Representable isos - Githubissues

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.

https://rzk-lang.github.io/sHoTT/

44 stars 12 forks source link

Representable isos #141

Closed cesarbm03 closed 10 months ago

cesarbm03 commented 11 months ago

This is the proof of RS17 Proposition 10.11. I am not sure if what I did is unnecessarily long.

emilyriehl commented 11 months ago

I'll look at the proofs more closely when I get a minute but a quick observation is that much of the proof text is overly indented. Have a look at https://rzk-lang.github.io/sHoTT/STYLEGUIDE/ for some guidance, or let me know if I can help by making specific suggestions.

cesarbm03 commented 11 months ago

Thank you for the observation. I have implemented the indentation, I hope is better this time.

emilyriehl commented 11 months ago

@cesarbm03 yes that's much better. (Please ignore the other file that's changed now with your PR; that was me doing a bit of clean up elsewhere while fixing a typo:

Another suggestion: to streamline the code you could open up a section at the start of your work on representable isomorphisms converting your common hypotheses

  ( A : U)
  ( is-segal-A : is-segal A)
  ( a a' : A)
  ( ψ : ( x : A) → ( Equiv ( hom A a x) ( hom A a' x)))

into variables. Then you'd remove these five arguments from everything that follows up until you close the section.

You could close it just before or after 10.11(a). If you close it just before then the hypotheses of that result will be declared there, which might be nice, but this choice is up to you.

I could implement this change for you if you like, or you could do it yourself, or you could argue to leave things as they are.

cesarbm03 commented 11 months ago

That'd be indeed much nicer! I will try doing it myself, if there is some issue I'll ask for help for sure.

cesarbm03 commented 10 months ago

@emilyriehl I have made the implementation you suggested, let me know if there is something else I could do to improve it. Thank you.

fizruk commented 10 months ago

@cesarbm03 I have applied autoformatting (using Rzk v0.7.2) to the file.

cesarbm03 commented 10 months ago

@fizruk Thank you so much. I just noticed the new version of Rzk, I have updated now

emilyriehl commented 10 months ago

@cesarbm03 I'm sorry this has taken me such an unreasonably long time to review this.

I just made a few cosmetic changes but want to see what you think before merging:

I renamed your "fiberwise" stuff to "representable." Here you are dealing with a fiberwise transformation between representable functors so I thought it would be better to save the more general name for other uses.
I rearranged your proofs slightly: (i) The paths that you concatenate now are defined in the order which they will ultimately be composed. (ii) When you ultimately compose the reversal of a path, I went ahead and reversed the definition of the original path. So the proofs of the sublemmas are a bit longer while the proof of the main result by composing them is shorter.

Let me know what you think of this and feel free to push back on the changes I made.

cesarbm03 commented 10 months ago

@emilyriehl Thank for the review, I agree with the changes you made. This so much better and cleaner! I had had consider where to reverse the paths and for some reason I did it in the theorem.