Functoriality properties of extension types

[TashiWalde]

• Every equivalence of types induces an equivalence on extension types. This was previously only proved for extensions from BOT
• Every retract of types induces a retract on extension types.
• I have renamed the previous term that only work for extensions from BOT by putting BOT in the name.
• Deduce full left-cancel-with-section for right orthogonal calculus (previously only a weak version)