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).

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

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

Revised on May 12, 2017 03:50:33 by Mike Shulman (76.167.222.204)