proposition: Lemma functor_disp_cat_univalent : is_univalent_disp functor_disp_cat.
proof: Proof. apply dirprod_disp_cat_is_univalent. - apply disp_full_sub_univalent. intros [F₀ F₁]. apply impred. intros x. cbn[pr2]. apply homset_property. - apply disp_full_sub_univalent. intros [F₀ F₁]. repeat (apply impred; intros ?). cbn[pr2]. apply homset_property. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions