Definition sigma_twosided_disp_cat_ob_mor : twosided_disp_cat_ob_mor C₁ C₂. Proof. simple refine (_ ,, _). - exact (λ x y, ∑ (xy : D₁ x y), D₂ (x ,, y ,, xy)). - exact (λ x₁ x₂ y₁ y₂ xy₁ xy₂ f g, ∑ (fg : pr1 xy₁ -->[ f ][ g ] pr1 xy₂), pr2 xy₁ -->[ f ,, g ,, fg ] pr2 xy₂). Defined.
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.