nLab 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

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
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, model \infty -category



Universal constructions


Producing new model structures

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

Model structures

for \infty-groupoids

for ∞-groupoids

for equivariant \infty-groupoids

for rational \infty-groupoids

for rational equivariant \infty-groupoids

for nn-groupoids

for \infty-groups

for \infty-algebras

general \infty-algebras

specific \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 closed type which is to be interpreted this way as a fibrant type. More generally, an open type TT in context Γ\Gamma is called fibrant if [Γ.T][Γ][\Gamma.T] \to [\Gamma] is a fibration.

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 two-level type theory (2LTT). 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, 2LTT 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.

Last revised on February 23, 2024 at 22:19:05. See the history of this page for a list of all contributions to it.