Definition disp_cat_id_comp_of_strict_twosided_disp_cat : disp_cat_id_comp cat_of_setcategory disp_cat_ob_mor_of_strict_twosided_disp_cat. Proof. split. - exact (λ (C : setcategory) (D : strict_twosided_disp_cat C C), twosided_disp_functor_identity D). - exact (λ (C₁ C₂ C₃ : setcategory) (F : C₁ ⟶ C₂) (G : C₂ ⟶ C₃) (D₁ : strict_twosided_disp_cat C₁ C₁) (D₂ : strict_twosided_disp_cat C₂ C₂) (D₃ : strict_twosided_disp_cat C₃ C₃) (FF : twosided_disp_functor F F D₁ D₂) (GG : twosided_disp_functor G G D₂ D₃), comp_twosided_disp_functor FF GG). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.DispFunctorPair. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws. Section FromIso. End FromIso.