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.
This is mostly a housekeeping PR cleaning up 03-extension-types.
weakextext-naiveextext. Maybe @emilyriehl wants to weigh in on this?eq-ext-htpy, which is the same asnaiveextext-extext.In terms of new formalizations:
curry-uncurry,uncurry-opcurry,fubini.htpy-ext-prop-extextthat extension extensionality implies the homotopy extension property.