Consider the commutative squarewhere is a final functor and is a discrete fibration. For , choose an object of the nonempty comma category . Commutativity gives an arrowLift 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 .
Articles by others on the same topic
There are currently no matching articles.