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 category with finite limits 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, also the base change (pullback) $h^\ast f \,\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 August 24, 2023 at 10:31:07. See the history of this page for a list of all contributions to it.