h-Prop

An h-prop or subsingleton is a type whose inhabitants are all equal. #m/def/type That is, a type $Γ ⊢ 𝑋$ is an h-prop iff the fibration

Γ, 𝑥 𝑦 : 𝑋 ⊢ 𝑥 \equiv 𝑦

has a section. Under propositions as some types, these are the types identified with propositions.

#state/develop | #lang/en | #SemBr