Formalise Theorem 8.8 of RS17 paper

[fizruk]

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

[cesarbm03]

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

[TashiWalde]

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]

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

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.