clean up 03-extension-types

[TashiWalde]

This is mostly a housekeeping PR cleaning up 03-extension-types.

• Formatting improvements
• Restructured the section about homotopy extension property a bit and added subheaders.
• The proof of RS-4.11 is now in its own subsection. We might consider removing this subsection, since it is kinda redundant given the direct implication weakextext-naiveextext. Maybe @emilyriehl wants to weigh in on this?
• Removed the redundant term eq-ext-htpy, which is the same as naiveextext-extext.
• Removed one copy of Prop 4.10. For some reason this formalization was duplicated.

In terms of new formalizations:

• Added functorial instances of curry-uncurry, uncurry-opcurry, fubini.
• Added a very short direct proof htpy-ext-prop-extext that extension extensionality implies the homotopy extension property.

[emilyriehl]

@TashiWalde this looks great.

I guess for completeness sake, let's leave the redundant 4.11 there for now. I like the compromise of putting it in its own section towards the end.

Maybe in the future we move some of the redundant formalizations elsewhere (eg to the Yoneda repository?) and work on improving the efficiency of the sHoTT repository overall. But this is clearly a broader discussion we all should weigh in on.