# nLab Darin Morrison

Selected writings

## Selected writings

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

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.