A pair of assignations (α, ω) each in {(Arrow(W)|:Arrow(W))} is said to identify an arrow world, W, with composition o, iff, for every arrow f of W, α(f) and ω(f) are identities with α(f) in Prior(f) and ω(f) in Post(f). We describe α(f) and ω(f) as the beginning and end of f respectively. An arrow world is said to be identifiable precisely if there exist such α and ω: ie the Post and Prior of each arrow contain identities.
For any arrow, f, of an identified arrow world, f o α(f)= f =ω(f) o f whence Prior(f) subsumes Prior(α(f)) and Post(f) subsumes Post(ω(f)). Identities are preserved by α and ω (since, if f is an identity, f o α(f) = α(f) and ω(f) = ω(f) o f). The end of a terminal arrow is terminal and the beginning of an initial arrow is initial.
For any composable pair, (f, g), in an identified arrow world, we have (f o α(f), g) and (f, ω(g) o g) composable with composites equal to that of (f, g).
What are the conditions under which, whenever h is initial or terminal, the following paragraph holds ? It certainly does in a category or if, for every f, Prior(f) = Prior(α(f)) and Post(f) = Post(ω(f)).
Whenever an arrow h is either initial or terminal, any a in Prior(h) and any w in Post(h) satisfy Hom(a, w) = {h}. Thus if an arrow world includes an initial arrow, i, and a terminal arrow, t, then it must also contain a null arrow; namely, given a in Prior(i) and w in Post(t), the unique member of Hom(a, w). [Note that h is initial iff, for any a in Prior(h), every member of Post(a) is initial; and terminal iff, for any w in Post(h), every member of Prior(w) is terminal. This makes the language easier later on.]
Written by Eddy.