Representable isos

[cesarbm03]

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

[emilyriehl]

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]

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

[emilyriehl]

@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]

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]

@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]

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

[cesarbm03]

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

[emilyriehl]

@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]

@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.