nLab tribe

Idea

A tribe in the sense of Joyal 2017, Def. 3.1.6 is a kind of fibration category providing some fragment of categorical semantics of dependent type theory and in particular of homotopy type theory.

Definitions

…

Related concepts

• clan

References

The particular terminology “tribe” is due to:

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

following

• André Joyal, What is categorical type theory, various talks in 2013 [pdf]

but the underlying notion of categorical semantics of dependent types is classical, going back at least to Seely 1984 & Hofmann 1997, as is the general idea of categorical semantics of homotopy type theory, going back to

• Steve Awodey, Michael Warren, Homotopy theoretic models of identity type, Mathematical Proceedings of the Cambridge Philosophical Society 146 1 (2009) [arXiv:0709.0248, doi:10.1017/S0305004108001783]

reviewed for instance in

• Mike Shulman, Categorical models of homotopy type theory (2012) [pdf]

See also:

• Michael Shulman, Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science, Volume 25, Issue 5 ( From type theory and homotopy theory to Univalent Foundations of Mathematics ) June 2015 (arXiv:1203.3253, doi:/10.1017/S0960129514000565)

• Chris Kapulkin and Karol Szumilo, Internal Language of Finitely Complete (∞,1)-categories, arxiv:1709.09519

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. […]

A tribe in the sense of Joyal is a display map category which models $\Sigma$-types and Paulin-Mohring Id-types.

• 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]