A class of higher inductive types in Zermelo-Fraenkel set theory

Abstract

We define a class of higher inductive types that can be constructed in the category of sets under the assumptions of Zermelo-Fraenkel set theory without the axiom of choice or the existence of uncountable regular cardinals. This class includes the example of unordered trees of any arity.

References in corpus (2)

• Quotients, inductive types, and quotient inductive types
• Constructing Infinitary Quotient-Inductive Types