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 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.
…
The particular terminology “tribe” is due to:
following
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
reviewed for instance in
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.
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.
Last revised on August 24, 2023 at 08:53:33. See the history of this page for a list of all contributions to it.