Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
type_equivalence [2014/11/17 19:01] nikolaj |
type_equivalence [2014/11/17 19:15] 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 24: | Line 24: | ||
==== Parents ==== | ==== Parents ==== | ||
=== Related === | === Related === | ||
- | [[Dependent type theory]] | + | [[Identity type]] |