Definition transportb_twosided_disp_functor_left {C₁ C₁' C₂ C₂' : category} {F : C₁ ⟶ C₁'} {G : C₂ ⟶ C₂'} {D₁ : twosided_disp_cat C₁ C₂} {D₂ : twosided_disp_cat C₁' C₂'} (FG : twosided_disp_functor F G D₁ D₂) {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D₁ x₁ y₁} {xy₂ : D₁ x₂ y₂} {f f' : x₁ --> x₂} (p : f = f') {g : y₁ --> y₂} (fg : xy₁ -->[ f' ][ g ] xy₂) : #2 FG (transportb (λ z, xy₁ -->[ z ][ g ] xy₂) p fg) = transportb (λ z, FG _ _ xy₁ -->[ z ][ _ ] FG _ _ xy₂) (maponpaths (λ z, #F z) p) (#2 FG fg).
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromDispFunctor. End FromDispFunctor.