proposition: Lemma foldr_var X (fvar : HSET_over_sort2⟦1,X⟧) (fapp : ∏ s t, HSET_over_sort2⟦app_source s t X,X⟧) (flam : ∏ s t, HSET_over_sort2⟦lam_source s t X,X⟧) : var_map · foldr_map X fvar fapp flam = fvar.
proof: Proof. assert (F := maponpaths (λ x, BinCoproductIn1 (BinCoproducts_functor_precat _ _ _ _ _) · x) (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))). rewrite assoc in F. eapply pathscomp0; [apply F|]. rewrite assoc. eapply pathscomp0; [eapply cancel_postcomposition, BinCoproductOfArrowsIn1|]. rewrite <- assoc. eapply pathscomp0; [eapply maponpaths, BinCoproductIn1Commutes|]. apply id_left. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Slice UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.slicecat UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.LiftingInitial_alt UniMath.SubstitutionSystems.Notation UniMath.SubstitutionSystems.MonadsMultiSorted UniMath.SubstitutionSystems.MultiSorted UniMath.SubstitutionSystems.MultiSortedMonadConstruction