## Idea A type which represents the notion of truth value in homotopy type theory. ## Definition A __proposition__ is a type $A$ with a term $$p: \prod_{a:A} \prod_{b:A} a = b$$ ## See also * [[set]] category: not redirected to nlab yet