proposition: Proposition identity_preserves_hor_id {C : category} {D : twosided_disp_cat C C} (I : hor_id D) : preserves_hor_id I I (twosided_disp_functor_identity D).
proof: Proof. use make_preserves_hor_id. - exact (identity_preserves_hor_id_data I). - exact (identity_preserves_hor_id_laws I). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Categories.CategoryOfSetCategories UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics