I am confused

[andrejbauer]

Correct me if I am wrong, but aren't we doing the case of HIT which can be factored out into an ordinary inductive type followed by a coequalizer? If not, what's a counter-example? Our signature is finitary, so it ought to be the case that we can just do it this way.

Which begs the question: what is the paper about then?

(I probably asked you this question already in Ljubljana. For forgetful people like me, we should provide a counter-example in the paper.)

[nmvdw]

I think the truncation would be a counterexample. I will check that.

[nmvdw]

In Ljubljana we looked at set quotients. In this case we can write every finitary HIT, which is a set, as a quotient. However, in the paper, not every HIT is necessarily a set. I tried to prove that the coequalizer of the maps \pi_1, \pi_2 : A \times A -> A is a mere proposition, but for that I needed some coherencies on the paths in the coequalizer. I also tried to prove: if you have a path \prod x : B \> H, t \> x = r \> x in H, then the coequalizer C of t, r : B \> T \rightarrow T has a path \prod x : B \> C, \overline{t} \> x = \overline{r} \> x. For the extensions \overline{t}, \overline{r} : B \> C \rightarrow C and the overall proof I again needed some coherencies which I was unable to prove in general.

I think the statement that a HIT can be factored out as an inductive type followed by a coequalizer only holds for finitary HITs which are sets.

[andrejbauer]

Right. In fact, already the truncation of the unit type does not work. The coequalizer of the two projections unit × unit → unit is the circle, not the truncation of unit (which is unit). It would be instructive to see how we get the truncation of unit using our construction. So what happens if we construct the HIT:

Inductive T :=
| t : T
| p : ∏ (x y : T), x = y

First we have just t_0. Then we throw in a path p_0 : t_0 = t_0. Then what?

[nmvdw]

The construction happens in multiple steps. In this case H_Con does nothing, because we only have nonrecursive point constructors. We don't have to make identifications for them either. So, we get the following Inductive T_1 := | i : T_0 -> T_1 | p_1 : Π (x y : T_0), x = y This is a bit harder to draw, but I think it basically fills the circle with many paths. For each x and y in T_0 = S^1 we add a path x = y in T_1. We do have to identify paths. We have to identify ap i p_0 and p_1 (i t_0) (i t_0). We wantp_1to be some kind of extension ofp_0. So, if we putp_0inT_1, then we get the path ofp_1betweent_0andt_0. This continues. The only differences in the higher cases is thatp_0would explicitly need arguments as now it is just a path betweent_0andt_0`.