proposition: Lemma displayed_presheaf_morphism_eq {T T' : algebraic_theory} {F : algebraic_theory_morphism T T'} {P : presheaf_disp_cat T} {P' : presheaf_disp_cat T'} (G G' : (P : presheaf_disp_cat _) -->[F] P') (H : pr1 G = pr1 G') : G = G'.
proof: Proof. refine (subtypePath _ H). intro. use (isapropdirprod _ _ _ isapropunit). do 4 (apply impred_isaprop; intro). apply setproperty. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Examples.Cartesian UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Total UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.IndexedSetCategory