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
A clan in the sense of Joyal 2017, Def. 1.1.1 (previously: category with display maps [Taylor 1987, §4.3.2], or display category [Taylor 1999, §8.3], a non-strict notion of contextual categories) is a minimum notion of fibration category providing categorical semantics for dependent types modelling (just) context extension and dependent pair type-formation (but not necessarily, say, function types or identity types):
A clan is a category with a terminal object equipped with a sub-class $Fib \subset Mor$ of its morphisms, to be called the fibrations and serving the role of display maps, such that:
every isomorphism is in $Fib$,
for every object $X$ the terminal map $X \to \ast$ is in $Fib$ (hence all objects are fibrant, cf. category of fibrant objects),
for $f \in Fib$ and $h$ any coincident morphism, the base change (pullback) $h^\ast f$ exits and is in $Fib$ (this interprets context extension)
for composable $f,g \in Fib$ also their composition $g \circ f \in Fib$ (this interprets dependent pair type-type formation)
The definition of categories with display maps and their role as categorical semantics for dependent types is due to
being a non-strict version of contextual categories:
The terminology “clan” for this notion is due to:
but the general notion of categorical semantics of dependent types is classical, going back at least to Seely 1984 and Hofmann 1997.
The type-theory-literature traditionally refers to such categories generically as display map/fibration categories with such-and-such types, eg.
The definitions in this section are relatively standard in the literature. A display map category which models $\Sigma$-types coincides with Joyal’s notion of clan, and a display map category which models $\sum$-types and $\prod$-types coincides with his notion of $\pi$-clan.
Last revised on January 15, 2024 at 02:58:15. See the history of this page for a list of all contributions to it.