Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
type_equivalence [2014/11/17 19:01] nikolaj |
type_equivalence [2015/12/07 18:39] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Type equivalence ===== | ===== Type equivalence ===== | ||
==== Type ==== | ==== Type ==== | ||
- | | $(A\simeq B) \equiv \Sigma_{f:A\to B}isequiv(f)$ | | + | | $(A\simeq B) \equiv \Sigma_{f:A\to B}\ isequiv(f)$ | |
where | where | ||
Line 18: | Line 18: | ||
We see how equivalence of types $(A\simeq B)$ eventually comes down to equality of terms. | 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, can should construct an equivalence on of these 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. | This is in analogy to how [[my equivalence of categories|equivalences of categories]] (defined via natural isomorphisms) comes down to isomorphisms of objects. | ||
==== Parents ==== | ==== Parents ==== | ||
- | === Related === | + | === Requirements === |
- | [[Dependent type theory]] | + | [[Identity type]] |