@InProceedings{kaposi_et_al:LIPIcs.FSCD.2018.20, author = {Kaposi, Ambrus and Kov\'{a}cs, Andr\'{a}s}, title = {{A Syntax for Higher Inductive-Inductive Types}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {20:1--20:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.20}, URN = {urn:nbn:de:0030-drops-91906}, doi = {10.4230/LIPIcs.FSCD.2018.20}, annote = {Keywords: homotopy type theory, inductive-inductive types, higher inductive types, quotient inductive types, logical relations} }