proposition: Lemma is_assoc_compose (a b c : A) : compose (compose a b) c = compose a (compose b c).
proof: Proof. unfold compose. pose (v := weqvecfun _ [(a ; b ; c)]). pose (Hv := λ i Hi, !(pr_action _ (make_stn 3 i Hi) v)). rewrite (Hv 0 (idpath true) : a = _), (Hv 1 (idpath true) : b = _), (Hv 2 (idpath true) : c = _). do 2 rewrite (move_action_through_vector_2 _ _ _). do 2 rewrite <- comp_action. cbn -[weqvecfun action]. do 2 rewrite subst_abs. do 4 rewrite subst_app. do 6 rewrite subst_var. do 6 extend_tuple_3. do 2 rewrite (move_action_through_vector_2 _ _ _). do 2 rewrite <- comp_action. cbn -[weqvecfun v]. do 2 rewrite subst_abs. do 4 rewrite subst_app. do 6 rewrite subst_var. do 6 extend_tuple_3. cbn -[v]. do 3 rewrite inflate_var. do 2 rewrite inflate_abs. do 2 rewrite beta_equality. do 8 rewrite subst_app. do 6 rewrite subst_subst. do 6 rewrite subst_var. do 3 rewrite extend_tuple_inl. rewrite (extend_tuple_inr _ _ : extend_tuple _ _ lastelement = _). do 2 rewrite subst_var. do 6 rewrite inflate_var. do 2 rewrite extend_tuple_inr. do 4 rewrite subst_var. now do 4 rewrite extend_tuple_inl. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.Combinatorics.Tuples UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Presheaf UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.Examples.LambdaCalculus UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaCalculus UniMath.AlgebraicTheories.LambdaTheoryCategory