internal category in homotopy type theory

**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**

One may consider internal categories in homotopy type theory. Under the interpretation of HoTT in an (infinity,1)-topos, this corresponds to the concept of a category object in an (infinity,1)-category. The general idea is presented there at *Homotopy Type Theory Formulation*.

For internal 1-categories in HoTT (as opposed to more general internal (infinity,1)-categories) a comprehensive discussion was given in (Ahrens-Kapulkin-Shulman-13).

In some literature, the “Rezk-completeness” condition on such categories is omitted from the definition, and categories that satisfy it are called *saturated* or *univalent*.

- Particularly useful in the context of such categories are displayed categories.

The relation between Segal completeness (now often “Rezk completeness”) for internal categories in HoTT and the univalence axiom had been pointed out in

A comprehensive discussion for 1-categories is in

- Benedikt Ahrens, Chris Kapulkin, Michael Shulman,
*Univalent categories and the Rezk completion*, Mathematical Structures in Computer Science, Volume 25, Issue 5 (*From type theory and homotopy theory to Univalent Foundations of Mathematics*), June 2015, pp. 1010-1039 (arXiv:1303.0584)

Exposition of this includes

Discussion of implementation of this in Coq includes

- Jason Gross, Adam Chlipala, David Spivak,
*Experience Implementing a Performant Category-Theory Library in Coq*(arXiv:1401.7694)

Genealization to (n,1)-categories is discussed in

- Paolo Capriotti, Nicolai Kraus,
*Univalent Higher Categories via Complete Semi-Segal Types*(arXiv:1707.03693)

Revised on July 15, 2017 09:14:27
by Urs Schreiber
(178.6.113.200)