Explaining the construction

[andrejbauer]

In Section 3, it is not explained anywhere what the purpose of all the data for the construction is. For instance, what are Q and R and j_Q about? These symbols are not connected to anything that came before, or I just don't see it.

I think it would help to see how the construction works in a particular simple example.

[nmvdw]

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 are the inclusions of the constructor terms. The paths p_Q and p_R are the paths of the HIT in stage F(n-2) and F(n-3).

[andrejbauer]

Could we do it like this:

1. Define a construction G which is F_0, F_1 and F_2 combined.
2. Compute the colimit of G, G^2, G^3?

This might be a bit clearer.

[nmvdw]

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

[andrejbauer]

Ok, then, let's try to explain what G is doing:

1. It throws in n levels of constructors (where n is the rank of the path constructors, i.e., how deeply the LHS and RHS nest the point constructors).
2. It adds the paths prescribed by the path constructors.
3. It adds some coherences? What coherences?

[andrejbauer]

A working example should help understand the coherence stuff. Consider the propositional truncation of bool (which should be the interval):

Inductive T:
| zero : T
| one : T
| eq : forall x y : T, x = y

What does G do precisely? (In the most general case applicable.) Here is my best guess. We should think of G as a functor. It takes a type X and returns the type constructed in steps as follows:

1. First we generate one stage of points from X using the point constructors, so that gives us a type T' with two points, call them zero' and one'.
2. Then we take the coequalizer which puts in the path constructors, so in this case we calculate the coequalizer of the two projectionsT' × T' → T'. The result is a type T'' which has two points and four paths. Two of these paths are loops lzero : zero' = zero' and lone : one' = one'
3. Now there is a problem: the loops lzero and lone are not supposed to be there, so we want to make them equal to reflexivity. But here I get lost, how does this relate to your construction? Anyhow, we put in some more paths between paths to obtain a type T''. This is then the result of G X?

[nmvdw]

We start with T_0 which is just Bool.
For T_1 we start with T_0. Since there are no recursive constructors, we don't add points. Then we add paths p_1 : true = true, p_2 : true = false, p_3 : false = false (note: the actual result is a fattening of the interval! Not precisely the interval).
For T_2 we start with T_1. Again we add no points, but we add paths. We make T_2 as follows
Inductive T_2 = | i : T_1 -> T_2 | p : \prod x y : T_1, i x = i y
Note that we have added duplicates in the paths. Note we have the paths ap i p_2 and p (i true) (i false). We want it to be free, so we need to prevent duplicates. To do so, we use to path coequalizer.

If we had the type
Inductive N/2 = | 0 : N/2 | S : N/2 -> N/2 | p : 0 = S(S 0)
Now we focus on the points for the point coherencies.
We start with 0. Then we add S_1 0. We now have T_1 with points 0 and S_1 0. For T_2 we add points S_2 0 and S_2(S_1 0). Now we have two instances of 1, and we identify these.

In the text I briefly discussed the example of N/2 in the start of The Approximatoe. I think it would be a good idea to extend this one to show the whole constructiob.

[nmvdw]

The paths lzero and lone are supposed to be there. We have the path p : \prod x y : A, x = y. They are the paths p zero zero and p one one.
So, there are supposed to be extra paths. But they are equal to refl, because we repeat the construction. We add more paths x=y, and that causes it to be a mere proposition.

[andrejbauer]

Can you prove that the reuslt is a mere proposition? When will p one one become equal to refl?

What I am worrited about is whether there are enough coherences thrown in.

[nmvdw]

I was able to prove the introduction, elimination and computation rules, so the result is a mere proposition if my proof is correct. The introduction rule required the coherencies, and those were added.
Let's look at what happen if we apply the construction to the circle. Then we see why p one one becomes equal to refl. In this case one is base and p one one is refl.
Inductive T = | i : S^1 -> T | p : Π x y : S^1, i x = i y
Then we have p base : Π y : S^1, i base = i y. Then apd (p base) loop is a path between loop_*(p base base) and p base base (transport over a family constant = x). But loop_*(p base base) = p base base o ap i loop. So, p base base = p base base o ap i loop, and thus ap i loop = refl.
So, in the next step we again add paths p : Πx, y : T, i x = i y, and after that the previous problems are solved. The paths like p one one in the previous stages satisfy the conditions. However, we might have created new problems, so we continue. Because we do ω steps, the result is correct.

[andrejbauer]

Should that be p : Πx, y : T, i x = i y or p : Πx, y : T, x = y?

[andrejbauer]

I am sorry, but now you used S^1 to establish a fact, but we're trying to construct S^1. Can we just go through the example I suggested, i.e., the propositional truncation of two points? Why will p_1 = refl there?

[nmvdw]

Similar argument. I used S^1 because if you restrict it, it is a circle.
We start with

Inductive T_1 =
| a_1 : T_1
| b_1 : T_1
| p_1 : a_1 = a_1
| p_2 : a_1 = b_1
| p_3 : b_1 = b_1
Inductive T_2 =
| i : T_1 -> T_2
| q : Π x y : T_1, i x = i y
| c_1 : ap i p_1 = q (i a_1) (i a_1)
| c_2 : ap i p_2 = q (i a_1) (i b_1)
| c_3 : ap i p_3 = q (i b_1) (i b_1)

The c_i are the added coherencies for the paths (to prevent duplicates).
Goal: q (i a_1) (i a_1) = refl
We have q a_1 : Π y : T_1, i a_1 = i y.
Then apd (q a_1) p_1 : (p_1)_* (q a_1 a_1) = q (a_1 a_1).
By 2.11.3 in the HoTT book: (p_1)_* (q a_1 a_1) = ap i (p_1) o (q a_1 a_1).
So, we have a path ap i (p_1) o (q a_1 a_1) = q a_1 a_1.
Now we rewrite with ap i p_1 = q (i a_1) (i a_1), and we get a path (q a_1 a_1) o (q a_1 a_1) = q a_1 a_1.
Cancelling now gives that q a_1 a_1 = refl.

[nmvdw]

At T_(n+1) we add paths p : Π x y : T_n, i x = i y. With these the path between p one one and refl are made.

[andrejbauer]

Thanks! Let me see if I can now make sense of what's written in the paper.