fibrant type

Definition

In type theory , a fiber of a function $f:A\to B$ for some value $b:B$ is simply the type of elements in the codomain that map to $b$.

Remarks

The term derives from homotopy theory, and was absorbed into type theory via HoTT.