Proposition transportb_disp_mor2_hor_op {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D x₁ y₁} {xy₂ : D x₂ y₂} {f f' : x₁ --> x₂} (p : f' = f) {g g' : y₁ --> y₂} (q : g' = g) (fg : xy₁ -->[ f ][ g ] xy₂) : transportb_disp_mor2 (D := hor_op_twosided_disp_cat_data) q p fg = transportb_disp_mor2 (D := D) p q fg. Proof. induction p, q ; cbn. apply idpath. Qed.
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.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.