Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
mere_proposition [2014/11/10 20:00] nikolaj |
mere_proposition [2014/11/10 21:12] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Mere proposition ===== | ===== Mere proposition ===== | ||
==== Type ==== | ==== Type ==== | ||
- | $isProp(A):={\large\Pi}_{x,y: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. |