Processing math: 100%

Mere proposition

Type

isProp(A):=Πx,y:AIdA(x,y)

Discussion

In HoTT, a type is a proposition iff all its terms are equal. Roughly, this means it has zero or one term.

Reference

Parents

Requirements

Link to graph
Log In
Improvements of the human condition