nLab clan

Idea

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):

Definition

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:

1. every isomorphism is in $Fib$,

2. for every object $X$ the terminal map $X \to \ast$ is in $Fib$ (hence all objects are fibrant, cf. category of fibrant objects),

3. 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)

4. for composable $f,g \in Fib$ also their composition $g \circ f \in Fib$ (this interprets dependent pair type-type formation)

Related concepts

• fibration category

• category of fibrant objects

• categorical semantics of dependent types

  • tribe

  • type-theoretic model category

References

The definition of categories with display maps and their role as categorical semantics for dependent types is due to

• Paul Taylor, §4.3.2 in: Recursive Domains, Indexed Category Theory and Polymorphism, Cambridge (1983-7) [pdf]

being a non-strict version of contextual categories:

• Paul Taylor, §8.3 in: Practical Foundations of Mathematics, Cambridge University Press (1999) [webpage]

The terminology “clan” for this notion is due to:

• André Joyal, Notes on Clans and Tribes [arxiv:1710.10238]

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.

North 2019, Rem. 2.4:

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.

• Paige Randall North, Identity types and weak factorization systems in Cauchy complete categories, Mathematical Structures in Computer Science 29 9 (2019) 1411-1427 [doi:10.1017/S0960129519000033, arXiv:1901.03567]