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

### General

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

A formalization in HoTT-Agda of general (n,r)-categories for $n,r \in \mathbb{N} \sqcup \{\infty\}$, defined as coinductive types of infinity-graphs, with operations defined by induction-coinduction, is implemented in