A class of higher inductive types in Zermelo-Fraenkel set theory
Logic
2022-02-07 v2
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.
Keywords
Cite
@article{arxiv.2005.14240,
title = {A class of higher inductive types in Zermelo-Fraenkel set theory},
author = {Andrew Swan},
journal= {arXiv preprint arXiv:2005.14240},
year = {2022}
}