natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
model category, model $\infty$-category
Definitions
Morphisms
Universal constructions
Refinements
Producing new model structures
Presentation of $(\infty,1)$-categories
Model structures
for $\infty$-groupoids
on chain complexes/model structure on cosimplicial abelian groups
related by the Dold-Kan correspondence
for equivariant $\infty$-groupoids
for rational $\infty$-groupoids
for rational equivariant $\infty$-groupoids
for $n$-groupoids
for $\infty$-groups
for $\infty$-algebras
general $\infty$-algebras
specific $\infty$-algebras
for stable/spectrum objects
for $(\infty,1)$-categories
for stable $(\infty,1)$-categories
for $(\infty,1)$-operads
for $(n,r)$-categories
for $(\infty,1)$-sheaves / $\infty$-stacks
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
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
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 $X$ in the empty context is usually interpreted as an object $[X]$ in the given target category, such that the unique morphism $[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]$ for which $[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 $T$ in context $\Gamma$ is called fibrant if $[\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.