proposition: Lemma is_univalent_sigma_disp (DD : is_univalent_disp D) (EE : is_univalent_disp E) : is_univalent_disp sigma_disp_cat.
proof: Proof. apply is_univalent_disp_from_fibers. intros x xx yy. use weqhomot. - induction xx as [xx xxx], yy as [yy yyy]. refine ( weqcomp (Y := (xx,, xxx : sigma_disp_cat x) ╝ yy,, yyy) _ (weqcomp (Y := ∑ ee : xx = yy, z_iso_disp (@total_z_iso _ D (_ ,, _) (_ ,, _) _ (idtoiso_disp (idpath _) ee)) xxx yyy) _ (weqcomp (Y := ∑ ff, (z_iso_disp (total_z_iso _ ff) xxx yyy)) _ _ ))). + apply total2_paths_equiv. + apply weqfibtototal. intro ee. induction (ee : xx = yy). refine (weqcomp (Y := z_iso_disp (idtoiso (C := total_category _) (total2_paths2_f (idpath x) (idpath _))) xxx yyy) _ _). * exact (make_weq (λ ee, idtoiso_disp (idpath _) ee) (EE _ _ _ _ _)). * now refine (make_weq _ (isweqtransportf (λ I, z_iso_disp I _ _) (z_iso_eq _ _ _))). + exact (weqfp (make_weq _ (DD _ _ (idpath _) _ _)) _). + exact (invweq (sigma_disp_z_iso_equiv (xxx := (_ ,, _)) (yyy := (_ ,, _)) _)). - assert (lemma1 : ∏ i i' (e : i = i') ii, pr1 (transportf (λ _, z_iso_disp _ (pr2 xx) (pr2 yy)) e ii) = transportf _ (maponpaths pr1 e) (pr1 ii)). { intros i i' e. now induction e. } intro ee. apply eq_z_iso_disp. induction ee. cbn. refine (maponpaths _ (lemma1 _ (total_z_iso _ (identity_z_iso_disp _)) _ _ @ _)). refine (maponpaths_2 (y' := idpath _) _ _ _). apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Limits