Let us say that a higher inductive type (aka HIT) H is 'non-recursive' if no constructor of H quantifies over elements of H. Examples are the spheres; a non-example is the propositional truncation (presented as usual). As a consequence, the elimination principle of the truncation only describes how to eliminate into propositional types. This raises two questions: First, can the truncation (or any given HIT H) be represented in a non-recursive way? And second, does this give a useful characterisation of maps into general types?

In this talk, I will present some results on this question, and compare the work by van Doorn with my own.