Niels van der Weide

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...

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...

In hindsight it wasn't necessary. When I first thought of the construction, I separated them in order to prevent duplicates of the nonrecursive constructors. But in hindsight I needed to...

I agree. But if we don't put the parameter in the name, how can we distinguish between `H_Con \> P` and `H_Con Q`? Same way as now or a different...

`H_Con P` makes constructor terms of `P`. `H_rec P` is terms of depth 1 using the constructor `c` from the HIT and arguments from `T`. For `H_Con` we look at...

It is not, but I did not recall it in the paper. We proved that in Proposition 13 in the paper 'Higher Inductive Types in Programming'. http://www.jucs.org/jucs_23_1/higher_inductive_types_in/jucs_23_01_0063_0088_basold.pdf

We use this assumption in Lemma 10. We need it, because otherwise we make a map from the constructor terms. We refer to lemma 11 on page 6 in 'From...

But we need to apply Lemma 10 to every constructor term, because for all constructor terms we need the induced map. On page 6 we apply Lemma 10 to every...

That is correct. I should have written down what I meant with them. We construct `F n`. Then `P` is `F(n-1)`, `Q` is `F(n-2)`, `R` is `F(n-3)`. `j_Q` and `j_R`...

That is indeed what I mean. That would be clearer I think.