proposition: Lemma binproduct_presheaf_induced_morphism_unique (t : ∑ k : presheaf_cat T ⟦ Q, binproduct_presheaf ⟧, k · binproduct_presheaf_pr1 = F × k · binproduct_presheaf_pr2 = F') : t = binproduct_presheaf_induced_morphism ,, binproduct_presheaf_induced_morphism_commutes.
proof: Proof. use subtypePairEquality. { intro. apply isapropdirprod; apply homset_property. } apply displayed_presheaf_morphism_eq. apply funextsec. intro n. apply funextfun. intro s. apply pathsdirprod. - refine (!_ @ maponpaths (λ x, pr1 x _ _) (pr12 t)). exact (maponpaths (λ x, x _) (presheaf_mor_comp _ _ _)). - refine (!_ @ maponpaths (λ x, pr1 x _ _) (pr22 t)). exact (maponpaths (λ x, x _) (presheaf_mor_comp _ _ _)). 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.Examples.Cartesian UniMath.CategoryTheory.DisplayedCats.Examples.Sigma UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Limits UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.Combinatorics.StandardFiniteSets UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryCategory UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.IndexedSetCategory UniMath.AlgebraicTheories.PresheafCategoryCore UniMath.AlgebraicTheories.PresheafMorphisms UniMath.AlgebraicTheories.Presheaves