proposition: Lemma is_univalent_disp_lambda_theory_data_disp_cat : is_univalent_disp lambda_theory_data_disp_cat.
proof: Proof. apply is_univalent_disp_iff_fibers_are_univalent. refine (λ (T : algebraic_theory) _ _, _). use isweq_iso. - intro f. use pathsdirprod; do 2 (apply funextsec; intro); apply f. - intro e. refine (maponpaths (λ x, _ x _) _ @ maponpaths _ _ @ !(pathsdirprod_eta e)); refine (pr1 ((_ : isaset _) _ _ _ _)); do 2 (apply (impred 2); intro); apply setproperty. - intro. apply z_iso_eq. refine (pr1 ((_ : isaprop _) _ _)). apply isapropdirprod; do 2 (apply impred; intro); apply setproperty. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategory UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples