search

rzk-lang / sHoTT

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

Formalise Theorem 8.8 of RS17 paper #12

Closed fizruk closed 1 year ago

fizruk commented 1 year ago

This one would particularly benefit from the literate style, providing the category-theoretic version of the proof from the paper in the text.

cesarbm03 commented 1 year ago

Feel free to modify the code I added if there is anything clashing with your proof.

TashiWalde commented 1 year ago

Let me also record here what I told @cesarbm03 .

After formalizing orthogonality and some of the statility properties thereof (see #81 and #76), it will be possible to formalize a very clean proof of this fact.

TashiWalde commented 1 year ago

@cesarbm03 Do you still plan to add anything to this issue or should we close it? If so, should we keep the helper methods apply-4-3 apply-4-3-again total-inner-horn-restriction map-to-total-inner-horn-restriction-fiber or can they be removed?

cesarbm03 commented 1 year ago

I am not sure if it has any value to have two proofs of the same result too. Plus, your proof is so elegant. At some point I felt the result was too involved for skills with the computer, I was hoping to resume the proof once I finish with the other PR I have open. I would vote for closing it since the result is proven now, if I get the "type theoretic proof" then we can decide whether is worth having two methods.