Idea
In type theory, a type is fibrant if it has enough path-filling to support homotopical identity types.
Definition
Definition
In type theory , a fiber of a function for some value is simply the type of elements in the codomain that map to .
Remarks
The term derives from homotopy theory, and was absorbed into type theory via HoTT.