Constructions with Non-Recursive Higher Inductive Types

DOI10.1145/2933575.2933586zbMath1394.03010OpenAlexW2467476450MaRDI QIDQ4635920

Nicolai Kraus

Publication date: 23 April 2018

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

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/84904788/Constrructions_with_Non_Recursive.pdf

zbMATH Keywords

homotopy type theoryhigher inductive typessequential colimitstruncation eliminationvan Doorn construction

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Related Items (7)

The construction of set-truncated higher inductive types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Higher Structures in Homotopy Type Theory ⋮ A Syntax for Higher Inductive-Inductive Types ⋮ Brouwer's fixed-point theorem in real-cohesive homotopy type theory ⋮ Semantics of higher inductive types

This page was built for publication: Constructions with Non-Recursive Higher Inductive Types