# Differences

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

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