Definition twosided_commute (H₁ : twosided_opcleaving) (H₂ : twosided_cleaving) {x₁ x₂ : C₁} {y₁ y₂ : C₂} (xy : D x₂ y₁) (f : x₁ --> x₂) (g : y₁ --> y₂) : twosided_opcleaving_ob H₁ (twosided_cleaving_ob H₂ xy f) g -->[ identity _ ][ identity _ ] twosided_cleaving_ob H₂ (twosided_opcleaving_ob H₁ xy g) f. Proof. use (twosided_opcartesian_factorisation (twosided_opcleaving_opcartesian H₁ _ g)). use (twosided_cartesian_factorisation (twosided_cleaving_cartesian H₂ _ f)). refine (transportb (λ z, _ -->[ z ][ _ ] _) _ (transportb (λ z, _ -->[ _ ][ z ] _) _ (twosided_cleaving_mor H₂ xy f ;;2 twosided_opcleaving_mor H₁ xy g))). - abstract (rewrite !id_left, !id_right ; apply idpath). - abstract (rewrite !id_left, !id_right ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.