Proposition transportf_disp_mor2_twosided_disp_cat_on_disp_cat {x₁ x₂ : E₁} {f f' : x₁ --> x₂} (p : f = f') {y₁ y₂ : E₂} {g g' : y₁ --> y₂} (q : g = g') {xy₁ : twosided_disp_cat_on_disp_cat_data x₁ y₁} {xy₂ : twosided_disp_cat_on_disp_cat_data x₂ y₂} (fg : xy₁ -->[ f ][ g ] xy₂) : transportf_disp_mor2 p q fg = transportf_disp_mor2 (maponpaths pr1 p) (maponpaths pr1 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.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total.