We prove the orthogonality of final functors and discrete fibrations. For , finality supplies an object of . Lift through the discrete fibration , obtainingIf in the comma category, then , and is a lift of with codomain . Uniqueness of that lift makes its domain equal to . Thus ; since the comma category is a connected category, equality propagates along every zigzag. Define to be this common object.
For , choose . Lift into , obtaining . Then lifts into , so its domain is by the preceding construction. Define . The unique lifting property of a discrete fibration proves and , and gives .
At , use ; its lift is , so . Both and are lifts of with the same codomain, hence agree. Therefore .
Articles by others on the same topic
There are currently no matching articles.