1) Added the definition of right orthogonal fibrations (also called j-orthogonal in BW23) with respect to a shape inclusion \phi \subset \psi.
2) Proved that left orthogonality is preserved when crossing \phi \subset \psi with a fixed shape \chi. This is one way of saying that right orthogonal fibrations are closed under exponentiation. This uses naive extension extensionality.
3) Proved that left orthogonality is closed under composition and left cancellation and right cancellation with a retraction.
I believe this material belongs in its own file/section. I have created a new file called 04a-right-orthogonal.rzk.md to avoid messing with the later files. Soon we should rename it (and the files after it).
1) Added the definition of right orthogonal fibrations (also called j-orthogonal in BW23) with respect to a shape inclusion
\phi \subset \psi.2) Proved that left orthogonality is preserved when crossing
\phi \subset \psiwith a fixed shape\chi. This is one way of saying that right orthogonal fibrations are closed under exponentiation. This uses naive extension extensionality.3) Proved that left orthogonality is closed under composition and left cancellation and right cancellation with a retraction.
I believe this material belongs in its own file/section. I have created a new file called
04a-right-orthogonal.rzk.mdto avoid messing with the later files. Soon we should rename it (and the files after it).Depends on #79