proposition: Lemma step1_disp_univalent : is_univalent_disp step1_disp.
proof: Proof. apply is_univalent_disp_from_fibers. hnf; cbn; intros x f g. apply isweqimplimpl. - intro i. unfold z_iso_disp in i. cbn in i. apply funextsec. intro. destruct i as (ff, Hff). apply funextsec. intro. apply funextsec. intro. etrans. { apply pathsinv0. apply id_right. } etrans. { apply ff. } apply id_left. - assert (KK : isaset (∏ a b : C, C ⟦ a, b ⟧ → D ⟦ x a, x b ⟧)). + repeat (apply (impred 2); intro). apply homset_property. + apply KK. - apply isaproptotal2. + unfold isPredicate. intro u. apply (isaprop_is_z_iso_disp (D := step1_disp)). + cbn. intros u v Hu Hv. apply funextsec. intro a. apply funextsec. intro b. apply funextsec. intro t. 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