Definition sigma_twosided_disp_cat_mor_eq {x₁ x₂ : C₁} {y₁ y₂ : C₂} {f : x₁ --> x₂} {g : y₁ --> y₂} {xy₁ : sigma_twosided_disp_cat_data x₁ y₁} {xy₂ : sigma_twosided_disp_cat_data x₂ y₂} (fg₁ : xy₁ -->[ f ][ g ] xy₂) (fg₂ : xy₁ -->[ f ][ g ] xy₂) (p : pr1 fg₁ = pr1 fg₂) (q : transportf (λ z, pr2 xy₁ -->[ z ] pr2 xy₂) (maponpaths (λ z, f ,, g ,, z) p) (pr2 fg₁) = pr2 fg₂) : 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.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.