Definition twosided_prod_transport_alt {x₁ x₂ : C₁} {y₁ y₂ : C₂} {xy₁ : D (F x₁) (G y₁)} {xy₂ : D (F x₂) (G y₂)} {f₁ f₂ : x₁ --> x₂} {g₁ g₂ : y₁ --> y₂} (fg : xy₁ -->[ #F f₁ ][ #G g₁ ] xy₂) (p : f₁ = f₂) (q : g₁ = g₂) : transportf (λ z, _ -->[ _ ][ #G z ] _) q (transportf (λ z, _ -->[ #F z ][ _ ] _) p fg) = transportf (λ z, _ -->[ pr1 z ][ dirprod_pr2 z ] _) (pathsdirprod (maponpaths (λ z, #F z) p) (maponpaths (λ z, #G z) q)) 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Section FromReindexIso. End FromReindexIso.