Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotients?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
No, it is not.
One can do a lot with just homotopy pushouts/coequalizers (I assume this is what you mean by "non-truncated quotients"). For instance, Egbert Rijke showed in The join construction that from this together with the natural numbers you can construct truncations.
However, in section 9 of Semantics of higher inductive types, Peter Lumsdaine and I gave an example of a higher inductive type that cannot be proven to exist in ZF set theory without the axiom of choice (assuming the consistency of certain large cardinals), whereas GADTs and homotopy colimits do exist in ZF. The idea follows a proof by Blass about free algebras for infinitary algebraic theories, that the "free ordinal with countable suprema" is an uncountable regular ordinal, whereas ZF cannot construct any uncountable regular ordinals.
answered Jun 25, 2022 at 16:04