===== 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 [[my equivalence of categories|equivalences of categories]] (defined via natural isomorphisms) comes down to isomorphisms of objects.

==== Parents ====
=== Requirements ===
[[Identity type]]