proposition: Lemma foldr_app X (fvar : sortToSet2⟦Id,X⟧) (fapp : ∏ s t, sortToSet2⟦app_source s t X,X⟧) (flam : ∏ s t, sortToSet2⟦lam_source s t X,X⟧) (s t : sort) : app_map s t · foldr_map X fvar fapp flam = # (pr1 (app_source s t)) (foldr_map X fvar fapp flam) · fapp s t.
proof: Proof. etrans; [ apply cancel_postcomposition; unfold app_map; apply assoc |]. rewrite <- assoc. etrans; [apply maponpaths, (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))|]. rewrite assoc. etrans; [eapply cancel_postcomposition; rewrite <- assoc; apply maponpaths, BinCoproductOfArrowsIn2|]. rewrite <- !assoc. etrans; [apply maponpaths, maponpaths, BinCoproductIn2Commutes|]. rewrite assoc. etrans; [apply cancel_postcomposition; use (CoproductOfArrowsIn _ _ (Coproducts_functor_precat _ _ _ _ (λ _, _)))|]. rewrite <- assoc. apply maponpaths. exact (CoproductInCommutes _ _ _ _ _ _ (inl (s,,t))). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SumOfSignatures UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems UniMath.SubstitutionSystems.SignatureExamples UniMath.SubstitutionSystems.MultiSorted_alt UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction_alt UniMath.SubstitutionSystems.MonadsMultiSorted_alt