Homotopy Type Theory
isomorphism in a precategory (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

A morphism f:hom A(a,b)f:hom_A(a,b) of a precategory AA is an isomorphism if there is a morphism g:hom A(b,a)g:hom_A(b,a) such that gf=1 agf=1_a and fg=1 bfg=1_b. We write aba \cong b for the type of such isomorphisms.

If f:abf:a \cong b, then we write f 1f^{-1} for its inverse which is uniquely determined by Lemma 9.1.3.

Properties

Lemma 9.1.3

For any f:hom A(a,b)f : hom_A(a,b) the type “f is an isomorphism” is a mere proposition?. Therefore, for any a,b:Aa,b:A the type aba \cong b is a set. Proof. Suppose given g:hom A(b,a)g:hom_A(b,a) and η:1 a=gf\eta:1_a = g f and ϵ:fg=1 b\epsilon : f g=1_b, and similarly g,ηg',\eta', and ϵ\epsilon'. We must show (g,η,ϵ)=(g,η,ϵ)(g,\eta,\epsilon)=(g',\eta', \epsilon'). But since all hom-sets are sets , their identity types are mere propositions, so it suffices to show g=gg=g'. For this we have g=1 ag=(gf)g=g(fg)=g1 b=g g' = 1_{a} g'= (g f) g' = g (f g') = g 1_{b}= g \square

category: category theory

Revision on September 4, 2018 at 13:28:34 by Ali Caglayan. See the history of this page for a list of all contributions to it.