Lemma step1_disp_univalent : is_univalent_disp step1_disp. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.