proposition: Lemma is_z_iso_functional_2_exponential_object : is_inverse_in_precat (C := HSET) functional_2_to_exponential_object_morphism_data exponential_object_to_functional_2_morphism_data.
proof: Proof. split. - apply funextfun. intro a. apply functional_2_eq. set (v := weqvecfun _ [(pr1 a)]). unfold exponential_object_to_functional_2_morphism_data. unfold functional_2_to_exponential_object_morphism_data. unfold functional_2_to_monoid_action_morphism_data. unfold exponential_object_to_functional_2_term. unfold functional_2_to_monoid_action_morphism_data_term. cbn -[weqvecfun aaction]. rewrite (pr2 a). rewrite <- (pr_action _ (make_stn 1 0 (idpath true)) v : _ = pr1 a). unfold make_functional_2, compose, I2, aaction. do 3 rewrite <- (lift_constant_action _ _ v). rewrite (move_action_through_vector_2 A _ _ _). rewrite <- comp_action. rewrite (move_action_through_vector_3 A _ _ _ _). rewrite <- comp_action. rewrite (move_action_through_vector_1 A _ _). rewrite <- comp_action. apply (maponpaths (λ x, aaction x v)). apply term_1_compose_2_λ. - apply funextfun. intro f. apply monoid_action_morphism_eq. intro a. apply functional_1_eq. refine (compose_2_term_1 _ _ _ @ _). refine (!base_paths _ _ (mor_action f _ _) @ _). apply maponpaths. apply maponpaths. set (v := weqvecfun _ [(pr11 a ; pr12 a)]). apply pathsdirprod; apply functional_1_eq; [ refine (_ @ !pr21 a) | refine (_ @ !pr22 a) ]; cbn -[weqvecfun aaction]; unfold make_functional_1, compose, I1, aaction; rewrite <- (pr_action _ (make_stn 2 0 (idpath true)) v : _ = pr11 a); rewrite <- (pr_action _ (make_stn 2 1 (idpath true)) v : _ = pr12 a); rewrite <- (lift_constant_action _ _ v); rewrite <- (lift_constant_action _ _ v); rewrite (move_action_through_vector_2 A _ _ _); rewrite (move_action_through_vector_2 A _ _ _); rewrite <- comp_action; rewrite <- comp_action; rewrite (move_action_through_vector_2 A _ _ _); rewrite <- comp_action; apply (maponpaths (λ x, aaction x v)). + apply compose_T_λ. + apply compose_F_λ. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Tuples UniMath.Combinatorics.Vectors UniMath.AlgebraicTheories.AlgebraicTheories UniMath.AlgebraicTheories.Algebras UniMath.AlgebraicTheories.AlgebraMorphisms UniMath.AlgebraicTheories.Examples.LambdaCalculus UniMath.AlgebraicTheories.Examples.EndomorphismTheory UniMath.AlgebraicTheories.FundamentalTheorem.SpecificUtilities.LambdaTerms UniMath.AlgebraicTheories.FundamentalTheorem.CommonUtilities.MonoidActions UniMath.AlgebraicTheories.LambdaTheories UniMath.AlgebraicTheories.LambdaCalculus UniMath.AlgebraicTheories.LambdaTheoryCategory