arXiv · 2005.14240
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.
Explore related subjects
Keep this discovery
Andrew Swan. 2020-05-28. A class of higher inductive types in Zermelo-Fraenkel set theory. https://doi.org/10.1002/malq.202100040
Cite the original work for its findings. Save a collection to share your selection of sources.