Large and Infinitary Quotient Inductive-Inductive Types

DOI10.1145/3373718.3394770zbMath1498.03032arXiv2006.11736OpenAlexW3028596397MaRDI QIDQ5145670

Ambrus Kaposi, András Kovács

Publication date: 21 January 2021

Published in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2006.11736

zbMATH Keywords

inductive typescategories with familiesinfinitary inductive typesquotient inductive-inductive types

Mathematics Subject Classification ID

Type theory (03B38)

Related Items (4)

On generalized algebraic theories and categories with families ⋮ Unnamed Item ⋮ For Finitary Induction-Induction, Induction is Enough ⋮ Unnamed Item

This page was built for publication: Large and Infinitary Quotient Inductive-Inductive Types