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

TL;DR

This paper introduces a new class of higher inductive types within Zermelo-Fraenkel set theory, enabling the construction of complex structures like unordered trees without relying on the axiom of choice.

Contribution

It defines a novel class of higher inductive types in ZF set theory, expanding the scope of constructible types without additional axioms.

Findings

Includes unordered trees of any arity as an example

Constructs higher inductive types without the axiom of choice

Operates within ZF set theory assumptions

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.