Weak ext ext

[jonalfcam]

Progress towards RS Prop 4.11. A helper function that defines $c(t) = refl$ from the proposition.

[jonalfcam]

More progress towards the end of section 4. This will require a refactor to get the logic of the section correct, but all of the necessary functions are now there.

[emilyriehl]

@jonalfcam it sounds like you're still working on this and don't want us to review yet?

[emilyriehl]

While I'm here a request: since function extensionality is called funext let's use weakextext and weakfunext (no hyphens).

[jonalfcam]

Great! I'll fix those. Yes, this is a draft for the moment. Everything is correcet and typechecks, but in order to finish off the proof of Prop 4.11 I need to refactor so that the homotopy extension property is its own property and doesn't depend on weakextext. Once that is done (and I've appropriately renamed helper lemmas), that should finish off section 4 (modulo 4.12, which I might wait until the natural numbers are available to do).

[jonalfcam]

I have finished the proof of Prop. 4.11. There is a robust debate to be had about my naming conventions.

[jonalfcam]

It would appear that someone defined NaiveExtExt which I also defined a version of. I'm happy to change things over to that terminology to fix that particular conflict. Otherwise, I'm not sure how to resolve these.

[emilyriehl]

Hi @jonalfcam and @TashiWalde. I attempted to fix the merge conflicts, but now my flight boarding so I have to go.

In the current draft there are two versions of 4.10. I wasn't sure which came later and which is preserved. Could you two resolve this?

Elsewhere we use concatenation extext and funext so I think we should use weakextext and naiveextext. I wasn't sure what to call the homotopy extension property though.

[emilyriehl]

It's quite possible I made a mistake in resolving the conflicts so please look at this closely. Also I didn't check the markdown sections carefully. We typically use #!rzk a instead of $a$ but I understand why @jonalfcam wanted to use LaTeX for the extension types.

[jonalfcam]

It looks like this merge failed, but I see why. Unfortunately I am also boarding a plane. I can take care of it tomorrow.

[jonalfcam]

It’s the changes on line 697 in 04 that are the culprit. It looks like they were resolved to an old version.

[jonalfcam]

This now passes checks.