# Differences

This shows you the differences between two versions of the page.

Both sides previous revision Previous revision | |||

type_equivalence [2014/11/17 19:15] nikolaj |
type_equivalence [2015/12/07 18:39] (current) nikolaj |
||
---|---|---|---|

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. |