nLab Ambrus Kaposi

• website

Selected writings

• Thorsten Altenkirch, Ambrus Kaposi, Type Theory in Type Theory using Quotient Inductive Types, POPL17 (2017) [pdf]

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]

Exposition:

• Ambrus Kaposi, Quotient inductive-inductive types and higher friends, Homotopy Type Theory Electronic Seminar Talks, 22 October 2020 (video, slides)

category: people