nLab
Darin Morrison

Selected writings

Selected writings

A formalization in HoTT-Agda of general (n,r)-categories for n,r{}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

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