Homotopy Type Theory proposition > history (Rev #6)

Idea

A type which represents the notion of truth value in homotopy type theory.

A proposition is a type $A$ with a term

p: \prod_{a:A} \prod_{b:A} a = b