A class of higher inductive types in Zermelo-Fraenkel set theory - Andrew Swan (2020)