Definition sigma_transportf_right {x₁ x₂ : C₁} {f₁ f₂ : x₁ --> x₂} (p : f₂ = f₁) {y₁ y₂ : C₂} {g : y₁ --> y₂} {xy₁ : sigma_twosided_disp_cat_data x₁ y₁} {xy₂ : sigma_twosided_disp_cat_data x₂ y₂} (fg : xy₁ -->[ f₂ ][ g ] xy₂) : transportf (λ z, xy₁ -->[ z ][ g ] xy₂) p fg = transportf (λ z, _ -->[ z ][ g ] _) p (pr1 fg) ,, transportf (λ z, @mor_disp _ D₂ _ _ (pr2 xy₁) (pr2 xy₂) z) (sigma_transportf_right_path p fg) (pr2 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. 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. Section FromSigmaIso. End FromSigmaIso.