A schema for higher inductive types of level one and its interpretation

Abstract

Supervised by Peter Dybjer.
We present a general schema for (non-dependent) higher inductive types built using only point and path constructors (HITs of level 1). Moreover we only allow ordinary inductive premisses for the constructors. We prove that the setoid model supports this schema. This model uses set-theory as a meta-language.