search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
45 stars 12 forks source link

Weak ext ext #70

Closed jonalfcam closed 1 year ago

jonalfcam commented 1 year ago

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

jonalfcam commented 1 year ago

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 commented 1 year ago

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

emilyriehl commented 1 year ago

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

jonalfcam commented 1 year ago

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 commented 1 year ago

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

jonalfcam commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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

jonalfcam commented 1 year ago

This now passes checks.