proposition: Lemma endomorphism_theory_is_lambda : is_lambda_theory endomorphism_lambda_theory_data.
proof: Proof. use make_is_lambda_theory. - intros m n f g. refine (maponpaths _ (assoc' _ _ _) @ _). refine (φ_adj_inv_natural_precomp (pr2 E) _ _ _ _ _ @ _). apply (maponpaths (λ x, x · _)). apply BinProductArrowsEq. + refine (bp_commutes_1 _ _ _ _ @ _). refine (id_right _ @ !_). refine (bp_commutes_1 _ _ _ _ @ _). refine (extend_tuple_inr _ _ @ _). exact (maponpaths _ (homotinvweqweq _ (inr tt))). + do 2 refine (bp_commutes_2 _ _ _ _ @ !_). apply ProductArrow_eq. intro i. refine (assoc' _ _ _ @ _). refine (maponpaths _ (pow_commutes _ _ _ _) @ !_). refine (pow_commutes _ _ _ _ @ _). refine (extend_tuple_inl _ _ _ @ _). apply (maponpaths (λ x, x · _)). apply ProductArrow_eq. intro j. refine (pow_commutes _ _ _ _ @ _). exact (maponpaths _ (homotinvweqweq _ (inl j))). - intros m n f g. refine (_ @ assoc' _ _ _). refine (_ @ maponpaths (λ x, x · _) (φ_adj_natural_precomp (pr2 E) _ _ _ _ _)). apply (maponpaths (λ x, φ_adj (pr2 E) (x · _) · _)). apply ProductArrow_eq. intro i. refine (pow_commutes _ _ _ _ @ !_). rewrite <- (homotweqinvweq stnweq i). induction (invmap stnweq i) as [i' | i']; refine (maponpaths (λ x, _ · (_ x)) (homotinvweqweq stnweq _) @ _). + refine (assoc _ _ _ @ _). refine (maponpaths (λ x, x · _) (bp_commutes_2 _ _ _ _) @ _). refine (assoc' _ _ _ @ _). refine (maponpaths (λ x, _ · x) (pow_commutes _ _ _ _) @ !_). refine (extend_tuple_inl _ _ _ @ _). apply (maponpaths (λ x, x · _)). apply ProductArrow_eq. intro j. refine (pow_commutes _ _ _ _ @ _). exact (maponpaths _ (homotinvweqweq _ (inl j))). + refine (bp_commutes_1 _ _ _ _ @ _). refine (id_right _ @ !_). refine (extend_tuple_inr _ _ @ _). exact (maponpaths _ (homotinvweqweq _ (inr tt))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaTheoryCategoryCore UniMath.AlgebraicTheories.LambdaTheoryMorphisms UniMath.Combinatorics.Tuples