proposition: Lemma plus_1_is_presheaf {T : algebraic_theory} (P : presheaf T) : is_presheaf (plus_1_presheaf_data P).
proof: Proof. use make_is_presheaf. - intros l m n x f g. refine (op_op P x _ _ @ _). apply (maponpaths (op (x : P _))). apply funextfun. intro i. induction (invmap stnweq i) as [i' | i']. + refine (comp_comp T (f i') _ _ @ !_). refine (comp_comp T (f i') g _ @ !_). apply maponpaths. apply funextfun. intro. refine (pr_comp _ _ _ @ _). exact (maponpaths _ (homotinvweqweq stnweq _)). + refine (pr_comp _ _ _ @ _). exact (maponpaths _ (homotinvweqweq stnweq _)). - intros n x. refine (_ @ op_pr _ _). apply (maponpaths (op (x : P _))). apply funextfun. intro i. refine (_ @ maponpaths _ (homotweqinvweq stnweq i)). induction (invmap stnweq i) as [i' | i']. + apply pr_comp. + apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Functors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.Presheaves UniMath.AlgebraicTheories.PresheafCategoryCore UniMath.Combinatorics.Tuples