Proposition double_hor_comp_mor_transportf_disp_mor2_right {C : category} {D : twosided_disp_cat C C} (Cm : hor_comp D) {x₁ x₂ y₁ y₂ z₁ z₂ : C} {v₁ v₁' : x₁ --> x₂} (p : v₁' = v₁) {v₂ v₂' : y₁ --> y₂} (q : v₂ = v₂') {v₃ v₃' : z₁ --> z₂} (r : v₃ = v₃') {h₁ : D x₁ y₁} {h₂ : D y₁ z₁} {k₁ : D x₂ y₂} {k₂ : D y₂ z₂} (s₁ : h₁ -->[ v₁' ][ v₂' ] k₁) (s₂ : h₂ -->[ v₂ ][ v₃ ] k₂) : double_hor_comp_mor Cm s₁ (transportf_disp_mor2 q r s₂) = transportf_disp_mor2 (!p) r (double_hor_comp_mor Cm (transportf_disp_mor2 p (!q) s₁) s₂). Proof. induction p, q, r ; 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.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.