Differences

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

Link to this comparison view

Both sides previous revision Previous revision
mere_proposition [2014/11/10 20:05]
nikolaj
mere_proposition [2014/11/10 21:12] (current)
nikolaj
Line 1: Line 1:
 ===== Mere proposition ===== ===== Mere proposition =====
 ==== Type ==== ==== Type ====
-$isProp(A):​={\large\Pi}_{x,​y:​A}Path_A(x,y)$+$isProp(A):​={\large\Pi}_{x,​y:​A}\,Id_A(x,y)$
 ==== Discussion ==== ==== Discussion ====
 In HoTT, a type is a proposition iff all its terms are equal. Roughly, this means it has zero or one term. In HoTT, a type is a proposition iff all its terms are equal. Roughly, this means it has zero or one term.
Link to graph
Log In
Improvements of the human condition