Formalise Propositions 3.6 and 3.7 from RS17 paper

[dvmcarpena]

Closes #3. Prop 3.6 works fine, but for prop 3.7 the check of Δ³-is-retract-Δ²×Δ¹-section does not terminate in my laptop. I'm not sure what's happening, but proof seems ok.

[fizruk]

I can reproduce the issue, I will trace it and report later. Thanks for letting us know!

[fizruk]

Initially, I thought there is a bug and an infinite loop somewhere. But it turns out, there's just a huge inefficiency (which can also be considered a bug, I guess). In particular, when checking Δ³-is-retract-Δ²×Δ¹-section, rzk has unnecessarily generated 21 LEM instances for points, many of which are ill typed (there was no typechecking in that part), leading to $2^{21}$ branches to check, which just took a lot of time.

I have fixed the issue locally, and now I see another issue in Δ³-is-retract-Δ²×Δ¹. The default proof by refl does not work, since $\eta$-expansion for pairs in the cube/tope layer does not fire appropriately, leading essentially to $\langle \langle \pi1 (t{12}), \pi2 (t{12}) \rangle, t3 \rangle \equiv \langle t{12}, t_3 \rangle$ in the goal, which does not simplify to reflexive equality tope (but should), so the typechecking is stuck and reports a type error.

I will fix this second issue as well soon, make a release, and then this PR will be good to merge!

Thanks for exposing weaknesses in the implementation :)

[dvmcarpena]

Great! Thanks for the quick response and fixes! Ready to merge for me :)

[emilyriehl]

Done.