Prove that the total category $\TotCat{\SelfIx{B}}$ of the canonical self-indexing (Section 2.1 [0003]) is the arrow category $B^{\to}$, and the projection is the codomain functor.
Prove that the total category $\TotCat{\SelfIx{B}}$ of the canonical self-indexing (Section 2.1 [0003]) is the arrow category $B^{\to}$, and the projection is the codomain functor.