- cpx h g G L V1 V2 → cpx h g G L T1 T2 →
- cpx h g G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-| cpx_zeta : ∀G,L,V,T1,T,T2. cpx h g G (L.ⓓV) T1 T →
- ⬆[0, 1] T2 ≡ T → cpx h g G L (+ⓓV.T1) T2
-| cpx_eps : ∀G,L,V,T1,T2. cpx h g G L T1 T2 → cpx h g G L (ⓝV.T1) T2
-| cpx_ct : ∀G,L,V1,V2,T. cpx h g G L V1 V2 → cpx h g G L (ⓝV1.T) V2
+ cpx h o G L V1 V2 → cpx h o G L T1 T2 →
+ cpx h o G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+| cpx_zeta : ∀G,L,V,T1,T,T2. cpx h o G (L.ⓓV) T1 T →
+ ⬆[0, 1] T2 ≡ T → cpx h o G L (+ⓓV.T1) T2
+| cpx_eps : ∀G,L,V,T1,T2. cpx h o G L T1 T2 → cpx h o G L (ⓝV.T1) T2
+| cpx_ct : ∀G,L,V1,V2,T. cpx h o G L V1 V2 → cpx h o G L (ⓝV1.T) V2