Homotopy Type Theory predicate > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

A predicate over a type $A$ is a type family $P$ such that for every $a:A$, $P(a)$ is a proposition:

See also

• relation

• proposition

• type family