Darin Morrison

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

- Darin Morrison,
*agda-nr-cats*,*agda-infinity-categories*

See also at *internal category in homotopy type theory*.

category: people

Last revised on August 27, 2019 at 03:15:15. See the history of this page for a list of all contributions to it.