Consider the commutative square
where is a final functor and is a discrete fibration. For , choose an object of the nonempty comma category . Commutativity gives an arrow
Lift it uniquely through with codomain , and define to be the domain of this lift.
This definition does not depend on the choice of . A morphism in the comma category satisfies . The composite of the lift of with is then a lift of with codomain , so uniqueness of discrete-fibration lifts says that it is the chosen lift and has the same domain. Since is connected, all choices give the same object .
For , define as the unique lift through of with codomain . Its domain is : choose , and observe that composing this lift with the lift of yields the lift associated with . Uniqueness of lifting also proves preservation of identities and composition, so is a functor and .
For , choose in . The lift of is , hence ; the same lifting argument on arrows gives . Finally, if is another filler, then for every , the arrow is a lift of . Unique lifting forces and then forces equality on arrows. Thus is unique, proving orthogonality of final functors and discrete fibrations.

Articles by others on the same topic (0)

There are currently no matching articles.