Contents

category theory

# Contents

## Idea

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.

## References

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

Exposition of this includes

Discussion of implementation of this in Coq includes

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

and, by different means, in

A formalization in HoTT-Agda of general (n,r)-categories for $n,r \in \mathbb{N} \sqcup \{\infty\}$ is claimed in

Last revised on January 20, 2019 at 01:40:42. See the history of this page for a list of all contributions to it.