proposition: Lemma disp_over_unit_fiber_equals_cat (C : category) (u : unit) : (disp_over_unit C)[{u}] = C.
proof: Proof. apply (subtypePath (λ _, isaprop_has_homsets _)). refine (subtypePairEquality' _ (isaprop_is_precategory _ (homset_property C))). induction C as [C Hhomsets]. induction C as [Cdata Hisprecategory]. exact (maponpaths (λ x, (pr1 Cdata) ,, x) (pathsdirprod (idpath _) (idpath _))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Examples UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Fiber