A morphism of a precategory is an isomorphism if there is a morphism such that and . We write for the type of such isomorphisms.
If , then we write for its inverse which is uniquely determined by Lemma 9.1.3.
For any the type “f is an isomorphism” is a mere proposition?. Therefore, for any the type is a set. Proof. Suppose given and and , and similarly , and . We must show . But since all hom-sets are sets , their identity types are mere propositions, so it suffices to show . For this we have
Revision on September 4, 2018 at 22:26:22 by Ali Caglayan. See the history of this page for a list of all contributions to it.