Idea
In type theory, a type is fibrant if it has enough path-filling to support homotopical identity types.
In ordinary homotopy type theory, this refers to a Kan fibrations.
In cubical type theory (CCHM), a fibrant type is a type together with a composition structure.
In Higher Observational Type Theory is a fibrant type if there is a transport isomorphism defined coinductively on all identity types over .
Remarks
The term derives from homotopy theory, and was absorbed into type theory via HoTT.