A formalization in HoTT-Agda of general (n,r)-categories for , defined as coinductive types of infinity-graphs, with operations defined by induction-coinduction, is implemented in
See also at internal category in homotopy type theory.
Last revised on August 27, 2019 at 07:15:15. See the history of this page for a list of all contributions to it.