fibrant type



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type/path type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Model category theory

model category



Universal constructions


Producing new model structures

Presentation of (,1)(\infty,1)-categories

Model structures

for \infty-groupoids

for ∞-groupoids

for rational \infty-groupoids

for nn-groupoids

for \infty-groups

for \infty-algebras



for stable/spectrum objects

for (,1)(\infty,1)-categories

for stable (,1)(\infty,1)-categories

for (,1)(\infty,1)-operads

for (n,r)(n,r)-categories

for (,1)(\infty,1)-sheaves / \infty-stacks

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts




In the categorical semantics of dependent type theory in some suitable category 𝒞\mathcal{C} (see at relation between category theory and type theory) a type XX in the empty context is usually interpreted as an object [X][X] in the given target category, such that the unique morphism [X]*[X]\to \ast to the terminal object (which interprets the unit type) is a special morphism called a display map. Specifically in the context of homotopy type theory display maps are typically fibrations with respect to some homotopical category structure on 𝒞\mathcal{C} (for instance the structure of a category of fibrant objects or even that of a model category, in particular that of a type-theoretic model category). Since in 𝒞\mathcal{C} objects [X][X] for which [X]*[X] \to \ast is a fibration are called fibrant objects, one may then call a type which is to be interpreted this way as a fibrant type.

Usually all types are required to be interpreted this way, and hence often the term “fibrant type” is not used, since often non-fibrant types are never considered.

However in general one may want to consider flavors of dependent type theory with categorical semantics in suitable homotopical categories which explicitly distinguishes between fibrant and non-fibrant interpretation. One example of this is what has come to be called Homotopy Type System (HTS). Default homotopy type theory (HoTT) has interpretation in type-theoretic model categories which is such that, roughly, Quillen equivalence is respected in that the interpretation in a way only depends on the (infinity,1)-category which is presented by the model category. Since up to weak equivalence every object in the model category is fibrant, this means that in this sense there is no sensible distinction between fibrant and non-fibrant objects/types. On the other hand, HTS is more a language for the type-theoretic model category itself (or whatever homotopical category plays its role), not just for the (infinity,1)-category that it is going to present. In its interpretation one explicitly wants to be able to distinguish between any object and its fibrant replacement. Hence in this context one distinguishes between “fibrant types” that are required to be interpreted as fibrant objects and “non-fibrant types” which may be interpreted as more general objects.

Created on May 12, 2014 at 01:28:57. See the history of this page for a list of all contributions to it.