Constructions with non-recursive higher inductive types

DOI10.1145/2933575.2933586MaRDI QIDQ4635920zbMATH OpenOpenAlexFDO

Authors 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

higher inductive typeshomotopy type theorysequential colimitstruncation eliminationvan Doorn construction

Mathematics Subject Classification ID

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

Recommendations

• Constructing higher inductive types as groupoid quotients
• Constructing higher inductive types as groupoid quotients
• Semantics of higher inductive types
• Functions out of higher truncations
• On higher inductive types in cubical type theory

Cited in

(13)

• A construction method for induced types and its application to G₂
• Construction of tame types
• The construction of set-truncated higher inductive types
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Semantics of higher inductive types
• Constructing higher inductive types as groupoid quotients
• A syntax for higher inductive-inductive types
• Impredicative encodings of (higher) inductive types
• Signatures and induction principles for higher inductive-inductive types
• The general universal property of the propositional truncation
• Functions out of higher truncations
• Higher Structures in Homotopy Type Theory
• scientific article; zbMATH DE number 7756115 (Why is no real title available?)

This page was built for publication: Constructions with non-recursive higher inductive types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635920)