## Definition ## A __predicate__ over a type $A$ is a [[type family]] $P$ such that for every $a:A$, $P(a)$ is a proposition: $$a:A \vdash \pi(a):isProp(P(a))$$ ## See also ## * [[relation]] * [[proposition]] * [[type family]] category: not redirected to nlab yet