Andrej Bauer

Ok good, then we can turn Proposition 13 into a propositional equality in the formalization.

I don't think that's the place. Lemma 10 is about a *single* constructor term, and so obviously it's going to have an `n`. Somewhere we need to know that *all*...

As I said at the beginning, I am asking where else we need to know this, other than `H_Conn^n`. Somewhere it should show up, or else it ought to be...

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

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

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

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

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

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

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