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*

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

category: people

Created on July 11, 2019 at 03:32:15. See the history of this page for a list of all contributions to it.