On higher inductive-inductive types:
Ambrus Kaposi, András Kovács, A Syntax for Higher Inductive-Inductive Types, at 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (2018) 20:1-20:18 [pdf, doi:10.4230/LIPIcs.FSCD.2018.20]
Ambrus Kaposi, András Kovács, Signatures and Induction Principles for Higher Inductive-Inductive Types, Logical Methods in Computer Science 16 1 (2020) lmcs:6100 [arXiv:1902.00297, doi:10.23638/LMCS-16(1:10)2020]
András Kovács, Type-Theoretic Signatures for Algebraic Theories and Inductive Types, PhD thesis (2022) [pdf, slides:pdf]
On computing the first stable homotopy group of spheres via homotopy type theory (the “Brunerie number”) in cubical Agda:
Last revised on July 13, 2024 at 07:48:31. See the history of this page for a list of all contributions to it.