Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
mere_proposition [2014/11/10 20:00] nikolaj |
mere_proposition [2014/11/10 20:05] 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}Path_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. | ||
