Type equivalence
Type
| $(A\simeq B) \equiv \Sigma_{f:A\to B}\ isequiv(f)$ |
where
$isequiv(f) \equiv \left(\Sigma_{g:B\to A}(f\circ g\sim id_B)\right) \times \left(\Sigma_{g:B\to A}(h\circ f\sim id_A)\right)$
where
$(k\sim l)\equiv \Pi_{x:C} \left(k(x)=_{P(x)}l(x)\right)$
where
$P:C\to U$ and $k,l: \Pi_{x:C}P(x)$.
Discussion
We see how equivalence of types $(A\simeq B)$ eventually comes down to equality of terms.
(The univalence axiom then says that to find those term-equalities, one can construct an equivalence on of these terms.)
This is in analogy to how equivalences of categories (defined via natural isomorphisms) comes down to isomorphisms of objects.
Parents
Requirements
