On 03/03/14 05:02, Michael Shulman wrote:
> I find both of these proofs very difficult to read. Can anyone write
> out the argument in informal language?
My post showing that ||2|| has the universal property of the interval
(judgementally for the first order equations and propositional for the
second order equations) was in this thread, back in July:
The proof is easy and short. The only trick is to come up with a
suitable proposition to work with.
Assume a type two with points 0,1:2, and let ||-|| denote the
Define I = ||2||, and let seg : |0| = |1| the path arising from the
definition of ||-|| (I call it the "truncation path").
The end-points of I are taken to be |0| and |1|, of course.
Given points x0,x1:X and a path p:x0=x1, we wish to build g:I->X such
that g|0|=x0 and g|1|=x1 (judgementally), and ap g seg = p
The trouble is that X is not assumed to be a proposition, and hence
the recursion principle for ||-|| can't be used.
So work instead with paths-from x0, i.e. Sigma(x:X).x0=x, which is a
Now define f:2->paths-from x0 by
f 0 = (x0, refl)
f 1 = (x1, p)
By the recursion principle for ||-||, f "extends" to
Now define g:||2||->X to be g' composed with the first projection,
which I call "endpoint" in this discussion.
You can check that g|0|=x0 and g|1|=x1 judgementally, by simply
expanding the definitions (or with Agda, as the proof refl is accepted).
The proof that ap g seg = p is equally easy. It suffices to consider
x0,x1 the same, say x, and p=refl x, in a proof by induction.
We have, in this case,
ap g' seg = refl (x,refl x),
using the fact that ||2|| is an proposition and hence an set.
Applying the first projection (called "end-point") to this path, we
ap end-point (ap g' seg) = ap end-point (refl (x,refl x)),
Now the lhs is equal to
ap (end-point o g') seg
and in turn, by the definition of g, to
ap g seg.
And the rhs is refl by the definition of ap. Putting this together, we get
ap g seg = refl
and our proof by induction is complete. Q.E.D.
Moreover, it is known that recursion on I gives induction. However, as
far as I know, it doesn't give it judgementally. Hence in the Agda
file I also include a proof that the induction principle for the
interval does hold judgementally if we take I=||2||.
Additionally, the above proof technique can be used to show that if a
function f:X->Y factors through |-|:X->||X||, then we can find a
judgemental factorization. Also in that file. Nicolai then used this
to define his mysterious pseudo-inverse of |-|:X->||X||.
To conclude, here is an observation. We discussed constancy (many
times) in this list.
Mike's definition is that f:X->Y is constant iff we are in possession
of y:Y such that f=\lambda x.y. Let's adopt this terminology. (In the
Agda file I call this "constant-valued".)
It is easy to see that f:X->Y has a factor through |-|:X->||X|| iff