Differences

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

Link to this comparison view

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.
Link to graph
Log In
Improvements of the human condition