Homotopy Type Theory isomorphism in a precategory > history (Rev #9, changes)

Showing changes from revision #8 to #9: Added | Removed | Changed

Definition

A morphism $f:hom_A(a,b)$ of a precategory $A$ is an isomorphism if there is a morphism $g:hom_A(b,a)$ such that $\mathrm{<span><del\; class="diffmod">\; gf</del><ins\; class="diffmod">\; g</ins></span>}\circ f=1_a$ gf=1_a g \circ f = 1_a and $\mathrm{<span><del\; class="diffmod">\; fg</del><ins\; class="diffmod">\; f</ins></span>}\circ g=1_b$ fg=1_b f\circ g = 1_b. We write $a \cong b$ for the type of such isomorphisms.

If $f:a \cong b$, then we write $f^{-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)$ the type “f is an isomorphism” is a mere proposition?proposition. Therefore, for any $a,b:A$ the type $a \cong b$ is a set. Proof. Suppose given $g:hom_A(b,a)$ and $\eta :1_a=g\circ f$ \eta:1_a = g \circ f and $ϵ:f\circ g=1_b$ \epsilon : f g=1_b \circ g = 1_b, and similarly $g',\eta'$, and $\epsilon'$. We must show $(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=g'$. For this we have $g\prime =1_a\circ g\prime =(g\circ f)\circ g\prime =g\circ (f\circ g\prime )=g\circ 1_b=g\square$ g' = 1_{a} \circ g'= (g \circ f) \circ g' = g \circ (f \circ g') = g \circ 1_{b}= g \square

See also

Category theory

References

HoTT Book