Library UniMath.AlgebraicTheories.FundamentalTheorem.AlgebraToTheory

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Algebra.Monoids.
Require Import UniMath.CategoryTheory.Categories.HSET.Core.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Exponentials.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.Tuples.
Require Import UniMath.Combinatorics.Vectors.

Require Import UniMath.AlgebraicTheories.AlgebraicTheories.
Require Import UniMath.AlgebraicTheories.AlgebraMorphisms.
Require Import UniMath.AlgebraicTheories.Algebras.
Require Import UniMath.AlgebraicTheories.Combinators.
Require Import UniMath.AlgebraicTheories.Examples.EndomorphismTheory.
Require Import UniMath.AlgebraicTheories.Examples.LambdaCalculus.
Require Import UniMath.AlgebraicTheories.FundamentalTheorem.CommonUtilities.MonoidActions.
Require Import UniMath.AlgebraicTheories.LambdaTheories.
Require Import UniMath.AlgebraicTheories.LambdaTheoryCategory.
Require Import UniMath.AlgebraicTheories.CategoryOfRetracts.

Local Open Scope cat.
Local Open Scope vec.
Local Open Scope algebraic_theories.
Local Open Scope lambda_calculus.
Local Open Scope stn.

1. The construction of the monoid


Section AlgebraToTheory.

  Context (L : lambda_theory).
  Context (Lβ : has_β L).
  Context (A : algebra L).

  Let maction {M : monoid} {X : monoid_action M}
    : (∏ x m, MonoidActions.action_ax M X x m)
    := MonoidActions.action.
  Let aaction {n : nat}
    : (∏ f a, AlgebraCategoryCore.action_ax L A n f a)
    := Algebras.action (n := n).

  Definition compose
    (a b : A)
    : A
    := aaction (compose (var (● 0 : stn 2)) (var (● 1 : stn 2))) (weqvecfun _ [(a ; b)]).

  Lemma compose_assoc
    (a b c : A)
    : compose a (compose b c) = compose (compose a b) c.
  Show proof.
    unfold compose, aaction.
    pose (v := weqvecfun _ [(a ; b ; c)]).
    pose (Hv := λ i, !(var_action _ (i : stn 3) v)).
    rewrite (Hv (● 0) : a = _).
    rewrite (Hv (● 1) : b = _).
    rewrite (Hv (● 2) : c = _).
    do 4 (rewrite (move_action_through_vector_2 A _ _ _), <- subst_action).
    apply (maponpaths (λ x, aaction x v)).
    do 4 rewrite subst_compose.
    do 8 rewrite (var_subst L).
    apply compose_assoc.
    exact Lβ.

  Definition I1
    : A
    := aaction (U_term L) (weqvecfun _ vnil).

  Lemma I1_idempotent
    : compose I1 I1 = I1.
  Show proof.
    unfold compose, I1, aaction.
    rewrite (move_action_through_vector_2 A _ _ _).
    rewrite <- subst_action.
    apply (maponpaths (λ x, aaction x _)).
    rewrite subst_compose.
    do 2 rewrite (var_subst L).
    apply (U_compose _ Lβ).

  Definition make_functional_1 (a : A)
    : A
    := compose I1 a.

  Definition is_functional_1 (a: A)
    : UU
    := a = make_functional_1 a.

  Lemma isaprop_is_functional_1 (a : A) : isaprop (is_functional_1 a).
  Show proof.
    apply setproperty.

  Lemma is_functional_1_action_abs
    {n : nat}
    (f : (L (S n) : hSet))
    (v : stn n → A)
    : is_functional_1 (aaction (abs f : ((L n) : hSet)) v).
  Show proof.
    unfold is_functional_1, make_functional_1, compose, I1, aaction.
    rewrite <- (lift_constant_action _ _ v).
    rewrite (move_action_through_vector_2 A _ _ v).
    rewrite <- subst_action.
    apply (maponpaths (λ x, aaction x _)).
    rewrite subst_compose.
    do 2 rewrite (var_subst L).
    refine (_ @ !maponpaths (λ x, x ∘ _) (subst_U_term _ _)).
    apply (!U_compose L Lβ _).

  Definition functional_1_set
    : hSet.
  Show proof.
    use (total2_hSet (X := A)).
    intro a.
    exists (is_functional_1 a).
    abstract exact (isasetaprop (isaprop_is_functional_1 _)).

  Definition functional_1_eq
    (a a' : functional_1_set)
    (H : pr1 a = pr1 a')
    : a = a'.
  Show proof.
    apply subtypePairEquality.
    {
      intro.
      apply isaprop_is_functional_1.
    }
    exact H.

  Section Monoid.

    Lemma is_functional_1_compose
      (a b : A)
      : is_functional_1 (compose a b).
    Show proof.
      unfold is_functional_1.
      unfold make_functional_1.
      unfold I1.
      unfold compose.
      set (v := weqvecfun _ [(a ; b)]).
      rewrite <- (lift_constant_action _ _ v).
      rewrite (move_action_through_vector_2 A _ _ v).
      rewrite <- (subst_action A).
      apply (maponpaths (λ x, aaction x _)).
      rewrite subst_compose.
      do 2 rewrite (var_subst L).
      refine (_ @ !maponpaths (λ x, x ∘ _) (subst_U_term _ _)).
      exact (!U_compose _ Lβ _).

    Definition is_functional_1_I1
      : is_functional_1 I1
      := !I1_idempotent.

    Lemma is_runit_I1
      (a : A)
      : compose a (I1) = make_functional_1 a.
    Show proof.
      pose (Ha := (var_action _ (● 0 : stn 1) (weqvecfun 1 [(a)]))).
      refine (!_ @ maponpaths _ Ha).
      refine (!_ @ maponpaths (λ x, _ x _) Ha).
      unfold make_functional_1, compose, I1, aaction.
      rewrite <- (lift_constant_action 1 _ (weqvecfun 1 [(a)])).
      rewrite (move_action_through_vector_2 A (var _) _ _).
      rewrite (move_action_through_vector_2 A _ (var _) _).
      do 2 rewrite <- subst_action.
      apply (maponpaths (λ x, aaction x _)).
      refine (subst_compose _ _ _ _ @ _).
      refine (maponpaths (λ x, x ∘ _) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ x) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ x) (subst_U_term _ _) @ _).
      refine (_ @ !subst_compose _ _ _ (weqvecfun _ [(_ ; var _)])).
      refine (_ @ !maponpaths (λ x, x ∘ _) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, _ ∘ x) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, x ∘ _) (subst_U_term _ _)).
      cbn.
      unfold U_term.
      rewrite (compose_abs _ Lβ).
      rewrite (abs_compose _ Lβ).
      rewrite (var_subst L).
      now rewrite extend_tuple_inr.

    Lemma is_unit_I1
      : isunit
        (λ a b, compose (pr1 a) (pr1 b) ,, is_functional_1_compose (pr1 a) (pr1 b))
        (I1 ,, is_functional_1_I1).
    Show proof.
      split;
        intro a;
        apply functional_1_eq;
        refine (_ @ !pr2 a).
      - apply idpath.
      - apply is_runit_I1.

    Definition lambda_algebra_monoid : monoid.
    Show proof.
      use tpair.
      - use tpair.
        + exact functional_1_set.
        + intros a b.
          exact (compose (pr1 a) (pr1 b) ,, is_functional_1_compose (pr1 a) (pr1 b)).
      - split.
        + abstract (
            intros a b c;
            apply functional_1_eq;
            apply (!compose_assoc _ _ _)
          ).
        + exact (_ ,, is_unit_I1).

  End Monoid.

2. The construction of the λ-theory with β-equality


  Section Theory.

    Definition UU_term
      : L 0
      := exponential_term L (U_term L) (U_term L).

    Definition I2
      : A
      :=
      aaction UU_term (weqvecfun _ vnil).

    Lemma I2_idempotent
      : compose I2 I2 = I2.
    Show proof.
      unfold compose, I2, aaction.
      rewrite (move_action_through_vector_2 A _ _ _).
      rewrite <- subst_action.
      apply (maponpaths (λ x, aaction x _)).
      rewrite subst_compose.
      do 2 rewrite (var_subst L).
      exact (exponential_idempotent L Lβ (U L Lβ) (U L Lβ)).

    Definition make_functional_2 (a : A)
      : A
      := compose I2 a.

    Definition is_functional_2 (a: A)
      : UU
      := a = make_functional_2 a.

    Lemma is_functional_2_action_abs
      {n : nat}
      (f : (L (S (S n)) : hSet))
      (p : stn n → A)
      : is_functional_2 (aaction (abs (abs f) : ((L n) : hSet)) p).
    Show proof.
      unfold is_functional_2, make_functional_2, compose, I2, aaction.
      rewrite <- (lift_constant_action _ _ p).
      rewrite (move_action_through_vector_2 A _ _ _).
      rewrite <- subst_action.
      apply (maponpaths (λ x, aaction x _)).
      refine (_ @ !subst_compose _ _ _ _).
      refine (_ @ !maponpaths (λ x, (x ∘ _)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ x)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, x ∘ _) (subst_exponential_term _ _ _ _)).
      refine (_ @ !maponpaths (λ x, (exponential_term _ x x ∘ _)) (subst_U_term _ _)).
      refine (_ @ !maponpaths (λ x, x ∘ _) (exponential_term_is_compose L Lβ _ _)).
      refine (_ @ !compose_abs L Lβ _ _ ).
      refine (_ @ !maponpaths (λ x, (abs (app x _))) (inflate_abs _ _)).
      refine (_ @ !maponpaths (λ x, (abs x)) (beta_equality _ Lβ _ _)).
      refine (_ @ !maponpaths (λ x, (abs x)) (subst_subst _ _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs x)) (subst_compose _ _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs (x ∘ _))) (subst_compose _ _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs (_ ∘ x))) (subst_inflate _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs ((x ∘ _) ∘ _))) (subst_inflate _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs ((_ ∘ x) ∘ _))) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs ((_ ∘ (x • _)) ∘ _))) (extend_tuple_inr _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs ((_ ∘ x) ∘ _))) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs ((_ ∘ x) ∘ _))) (extend_tuple_inr _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs (x ∘ _ ∘ x))) (subst_U_term _ _)).
      refine (_ @ !maponpaths (λ x, (abs (x ∘ _))) (U_compose L Lβ _)).
      exact (!maponpaths (λ x, (abs x)) (compose_U L Lβ _)).

    Lemma isaprop_is_functional_2 (a : A) : isaprop (is_functional_2 a).
    Show proof.
      apply setproperty.

    Definition functional_2_set
      : hSet.
    Show proof.
      refine (∑ (a : A), make_hSet (is_functional_2 a) _)%set.
      abstract exact (isasetaprop (isaprop_is_functional_2 _)).

    Definition functional_2_eq
      (a a' : functional_2_set)
      (H : pr1 a = pr1 a')
      : a = a'.
    Show proof.
      apply subtypePairEquality.
      {
        intro.
        apply isaprop_is_functional_2.
      }
      exact H.

    Definition compose_I1_I2
      : compose I1 I2 = I2
      := !is_functional_1_action_abs _ _.

    Lemma is_functional_2_to_is_functional_1
      (a : A)
      (H : is_functional_2 a)
      : is_functional_1 a.
    Show proof.
      rewrite H.
      unfold is_functional_1, make_functional_1, make_functional_2.
      rewrite compose_assoc.
      now rewrite compose_I1_I2.

    Lemma is_functional_2_compose
      (a : functional_2_set)
      (m : A)
      : is_functional_2 (compose (pr1 a) m).
    Show proof.
      unfold is_functional_2, make_functional_2.
      rewrite compose_assoc.
      exact (maponpaths (λ x, _ x _) (pr2 a)).

    Definition functional_2_monoid_action_data
      : monoid_action_data lambda_algebra_monoid.
    Show proof.
      use make_monoid_action_data.
      - exact functional_2_set.
      - intros a m.
        exists (compose (pr1 a) (pr1 m)).
        apply is_functional_2_compose.

    Lemma functional_2_is_monoid_action
      : is_monoid_action functional_2_monoid_action_data.
    Show proof.
      split.
      - intro x.
        apply functional_2_eq.
        simpl.
        apply (maponpaths pr1
          (runax lambda_algebra_monoid (_ ,, is_functional_2_to_is_functional_1 _ (pr2 x)))
        ).
      - intros.
        apply functional_2_eq.
        exact (compose_assoc _ _ _).

    Definition functional_2_monoid_action
      : monoid_action lambda_algebra_monoid
      := make_monoid_action _ functional_2_is_monoid_action.

    Definition functional_2_to_monoid_action_morphism_data_term
      (d : functional_2_monoid_action)
      (a b : A)
      : A.
    Show proof.
      pose (p := (weqvecfun _ [(pr1 d ; a ; b)])).
      refine (aaction _ p).
      refine (uncurry (var (● 0 : stn 3)) ∘ pair_arrow (var (● 1 : stn 3)) (var (● 2 : stn 3))).

    Definition functional_2_to_monoid_action_morphism_data
      (d : functional_2_monoid_action)
      : (BinProductObject _ (binproducts_monoid_action_cat lambda_algebra_monoid
          (monoid_monoid_action _)
          (monoid_monoid_action _)
        ) : monoid_action _)
        →
        (monoid_monoid_action lambda_algebra_monoid)
      := λ x, (
        functional_2_to_monoid_action_morphism_data_term d (pr11 x) (pr12 x) ,,
        is_functional_1_action_abs _ _
      ).

    Lemma functional_2_to_monoid_action_is_morphism
      (d : functional_2_monoid_action)
      : ∏ x m, mor_action_ax (functional_2_to_monoid_action_morphism_data d) x m.
    Show proof.
      intros x m.
      apply functional_1_eq.
      unfold functional_2_to_monoid_action_morphism_data.
      unfold functional_2_to_monoid_action_morphism_data_term.
      cbn -[weqvecfun aaction].
      pose (p := weqvecfun _ [(pr1 m ; pr1 d ; pr11 x ; pr12 x)]).
      unfold compose, aaction.
      rewrite <- (var_action _ (● 0 : stn 4) p : _ = pr1 m).
      rewrite <- (var_action _ (● 1 : stn 4) p : _ = pr1 d).
      rewrite <- (var_action _ (● 2 : stn 4) p : _ = pr11 x).
      rewrite <- (var_action _ (● 3 : stn 4) p : _ = pr12 x).
      do 2 (rewrite (move_action_through_vector_2 A _ _ _)).
      do 2 (rewrite <- subst_action).
      do 2 (rewrite (move_action_through_vector_3 A _ _ _ _)).
      do 2 (rewrite <- subst_action).
      rewrite (move_action_through_vector_2 A _ _ _).
      rewrite <- subst_action.
      apply (maponpaths (λ x, aaction x p)).
      refine (subst_compose _ _ _ _ @ _).
      refine (maponpaths (λ x, (x ∘ _)) (subst_uncurry _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ x)) (subst_pair_arrow _ _ _ _) @ _).
      refine (maponpaths (λ x, uncurry x ∘ _) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow x _) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow x _) (subst_compose _ _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow (x ∘ _) _) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow (_ ∘ x) _) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow _ x) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow _ x) (subst_compose _ _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow _ (x ∘ _)) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, _ ∘ pair_arrow _ (_ ∘ x)) (var_subst _ _ _) @ _).
      refine (_ @ !subst_compose _ (var _) _ _).
      refine (_ @ !maponpaths (λ x, (x ∘ _)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ x)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (x ∘ _)) (subst_compose _ _ _ _)).
      refine (_ @ !maponpaths (λ x, ((x ∘ _) ∘ _)) (subst_uncurry _ _ _)).
      refine (_ @ !maponpaths (λ x, ((_ ∘ x) ∘ _)) (subst_pair_arrow _ _ _ _)).
      refine (_ @ !maponpaths (λ x, uncurry x ∘ _ ∘ _) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, _ ∘ pair_arrow x _ ∘ _) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, _ ∘ pair_arrow _ x ∘ _) (var_subst _ _ _)).
      refine (_ @ Combinators.compose_assoc _ Lβ _ _ _).
      exact (!maponpaths (λ x, _ ∘ x) (pair_arrow_compose _ Lβ _ _ _)).

    Definition functional_2_to_exponential_object_morphism_data
      : functional_2_monoid_action →
        (exponential_object (monoid_monoid_action _) (monoid_monoid_action _))
      := λ d, make_monoid_action_morphism _ (functional_2_to_monoid_action_is_morphism d).

    Definition exponential_object_to_functional_2_term
      (f : (
        exponential_object
          (monoid_monoid_action lambda_algebra_monoid)
          (monoid_monoid_action lambda_algebra_monoid)
      ))
      : A.
    Show proof.
      refine (aaction (curry (var (stnweq (inr tt)))) (weqvecfun _ [(_)])).
      apply (f : monoid_action_morphism _ _).
      split.
      - exact (aaction π1 (weqvecfun _ [()]) ,, is_functional_1_action_abs _ _).
      - exact (aaction π2 (weqvecfun _ [()]) ,, is_functional_1_action_abs _ _).

    Definition exponential_object_to_functional_2_morphism_data
      : (exponential_object (monoid_monoid_action _) (monoid_monoid_action _))
        →
        functional_2_monoid_action
      := λ x, (exponential_object_to_functional_2_term x ,, is_functional_2_action_abs _ _).

    Lemma functional_2_to_exponential_object_is_morphism
      : ∏ x m, mor_action_ax functional_2_to_exponential_object_morphism_data x m.
    Show proof.
      intros a m.
      apply monoid_action_morphism_eq.
      intro x.
      apply functional_1_eq.
      unfold functional_2_to_exponential_object_morphism_data.
      unfold functional_2_to_monoid_action_morphism_data.
      unfold functional_2_to_monoid_action_morphism_data_term.
      cbn -[weqvecfun aaction].
      set (p := weqvecfun _ [(pr1 a ; pr1 m ; pr11 x ; pr12 x)]).
      rewrite <- (var_action _ (● 0 : stn 4) p : _ = pr1 a).
      rewrite <- (var_action _ (● 1 : stn 4) p : _ = pr1 m).
      rewrite <- (var_action _ (● 2 : stn 4) p : _ = pr11 x).
      rewrite <- (var_action _ (● 3 : stn 4) p : _ = pr12 x).
      unfold compose, aaction.
      do 2 (rewrite (move_action_through_vector_2 A _ _ _)).
      do 2 (rewrite <- subst_action).
      do 2 (rewrite (move_action_through_vector_3 A _ _ _ _)).
      do 2 (rewrite <- subst_action).
      apply (maponpaths (λ x, aaction x p)).
      refine (subst_compose _ _ _ _ @ _).
      refine (maponpaths (λ x, (x ∘ _)) (subst_uncurry _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ x)) (subst_pair_arrow _ _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry x) ∘ _)) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ (pair_arrow x _))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ (pair_arrow _ x))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry x) ∘ _)) (subst_compose _ _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry (x ∘ _)) ∘ _)) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry (_ ∘ x)) ∘ _)) (var_subst _ _ _) @ _).
      refine (uncurry_compose_pair_arrow _ Lβ _ _ _ @ _).
      refine (maponpaths (λ x, (abs (app (app x _) _))) (inflate_compose _ _ _) @ _).
      refine (maponpaths (λ x, (abs (app x _))) (app_compose _ Lβ _ _ _) @ _).
      refine (_ @ !subst_compose L _ _ (weqvecfun 3 [( _ ; (_ ∘ _) • _ ; _)])).
      refine (_ @ !maponpaths (λ x, (x ∘ _)) (subst_uncurry _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ x)) (subst_pair_arrow _ _ _ _)).
      refine (_ @ !maponpaths (λ x, ((uncurry x) ∘ _)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ (pair_arrow x _))) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ (pair_arrow _ x))) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ (pair_arrow x _))) (subst_compose _ _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ (pair_arrow (x ∘ _) _))) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (_ ∘ (pair_arrow (_ ∘ x) _))) (var_subst _ _ _)).
      refine (_ @ !uncurry_compose_pair_arrow _ Lβ _ _ _).
      refine (_ @ !maponpaths (λ x, (abs (app (app _ (app x _)) _))) (inflate_compose _ _ _)).
      exact (!maponpaths (λ x, (abs (app (app _ x) _))) (app_compose _ Lβ _ _ _)).

    Definition term_2
      (a a' : A)
      := (aaction (pair_arrow (var (● 0 : stn 2)) (var (● 1 : stn 2))) (weqvecfun _ [(a ; a')]) ,, is_functional_1_action_abs _ _).

    Lemma compose_2_term_1
      (b : monoid_monoid_action lambda_algebra_monoid)
      (a a' : A)
      : functional_2_to_monoid_action_morphism_data_term
        (aaction (curry (var (● 0 : stn 1))) (weqvecfun 1 [(pr1 b)]) ,, is_functional_2_action_abs _ _)
        a
        a'
      = pr1 (maction b (term_2 a a')).
    Show proof.
      unfold functional_2_to_monoid_action_morphism_data_term.
      cbn -[weqvecfun aaction].
      set (p := weqvecfun _ [(pr1 b; a; a')]).
      unfold functional_2_to_monoid_action_morphism_data_term, compose, aaction.
      rewrite <- (var_action _ (● 0 : stn 3) p : _ = pr1 b).
      rewrite <- (var_action _ (● 1 : stn 3) p : _ = a).
      rewrite <- (var_action _ (● 2 : stn 3) p : _ = a').
      rewrite (move_action_through_vector_1 A _ _).
      rewrite (move_action_through_vector_2 A _ _ _).
      rewrite <- subst_action.
      rewrite <- subst_action.
      rewrite (move_action_through_vector_2 A _ _ _).
      rewrite (move_action_through_vector_3 A _ _ _ _).
      rewrite <- subst_action.
      rewrite <- subst_action.
      apply (maponpaths (λ x, aaction x p)).
      refine (subst_compose _ _ _ _ @ _).
      refine (maponpaths (λ x, (x ∘ _)) (subst_uncurry _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ x)) (subst_pair_arrow _ _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry x) ∘ _)) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ (pair_arrow x _))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (_ ∘ (pair_arrow _ x))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry x) ∘ _)) (subst_curry _ _ _) @ _).
      refine (maponpaths (λ x, ((uncurry (curry x)) ∘ _)) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (x ∘ _)) (uncurry_curry _ Lβ _) @ _).
      refine (!Combinators.compose_assoc _ Lβ _ _ _ @ _).
      refine (maponpaths (λ x, (_ ∘ x)) (pair_arrow_compose _ Lβ _ _ _) @ _).
      refine (_ @ !subst_compose _ (var _) _ _).
      refine (_ @ !maponpaths (λ x, (x ∘ _)) (var_subst _ _ _)).
      apply maponpaths.
      refine (maponpaths (λ x, (pair_arrow x _)) (π1_pair_arrow _ Lβ _ _) @ _).
      refine (maponpaths (λ x, (pair_arrow _ x)) (π2_pair_arrow _ Lβ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app x _), _⟩))) (inflate_abs _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (inflate_abs _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨x, _⟩))) (beta_equality _ Lβ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, x⟩))) (beta_equality _ Lβ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨x, _⟩))) (subst_subst _ _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, x⟩))) (subst_subst _ _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨x, _⟩))) (subst_app _ _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, x⟩))) (subst_app _ _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app x _), _⟩))) (subst_inflate _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app _ x), _⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (subst_inflate _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app _ x)⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app x _), _⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app _ (x • _)), _⟩))) (extend_tuple_inr _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app _ (x • _))⟩))) (extend_tuple_inr _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app (x • _) _), _⟩))) (extend_tuple_inl _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app _ x), _⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app (x • _) _)⟩))) (extend_tuple_inl _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app _ x)⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app x _), _⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app _ x), _⟩))) (extend_tuple_inr _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (var_subst _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨_, (app _ x)⟩))) (extend_tuple_inr _ _ _) @ _).
      refine (maponpaths (λ x, (abs (⟨(app x _), _⟩))) (extend_tuple_inl _ _ _) @ _).
      refine (_ @ !var_subst _ _ _).
      refine (_ @ !subst_pair_arrow _ _ _ _).
      refine (_ @ !maponpaths (λ x, (pair_arrow x _)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (pair_arrow _ x)) (var_subst _ _ _)).
      refine (_ @ !maponpaths (λ x, (abs (⟨(app x _), _⟩))) (inflate_var _ _)).
      refine (_ @ !maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (inflate_var _ _)).
      exact (maponpaths (λ x, (abs (⟨_, (app x _)⟩))) (extend_tuple_inl _ _ _)).

    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.
    Show proof.
      split.
      - apply funextfun.
        intro a.
        apply functional_2_eq.
        set (p := 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 <- (var_action _ (make_stn 1 0 (idpath true)) p : _ = pr1 a).
        unfold make_functional_2, compose, I2, aaction.
        do 3 (rewrite <- (lift_constant_action _ _ p)).
        rewrite (move_action_through_vector_2 A _ _ _).
        rewrite <- subst_action.
        rewrite (move_action_through_vector_3 A _ _ _ _).
        rewrite <- subst_action.
        rewrite (move_action_through_vector_1 A _ _).
        rewrite <- subst_action.
        apply (maponpaths (λ x, aaction x p)).
        refine (subst_curry _ _ _ @ _).
        refine (maponpaths (λ x, (curry x)) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry x)) (subst_compose _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry (x ∘ _))) (subst_uncurry _ _ _) @ _).
        refine (maponpaths (λ x, (curry (_ ∘ x))) (subst_pair_arrow _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry ((uncurry x) ∘ _))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry ((uncurry x) ∘ _))) (subst_compose _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry ((uncurry (x ∘ _)) ∘ _))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry ((uncurry (_ ∘ x)) ∘ _))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry (_ ∘ (pair_arrow x _)))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry (_ ∘ (pair_arrow x _)))) (subst_π1 _ _) @ _).
        refine (maponpaths (λ x, (curry (_ ∘ (pair_arrow _ x)))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry (_ ∘ (pair_arrow _ x)))) (subst_π2 _ _) @ _).
        refine (!maponpaths (λ x, (curry x)) (uncurry_curry _ Lβ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (x ∘ _)))))) (subst_exponential_term _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry ((exponential_term _ x x) ∘ _)))))) (subst_U_term _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (x ∘ _)))))) (exponential_term_is_compose _ Lβ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry ((abs (x ∘ _ ∘ x)) ∘ _)))))) (subst_U_term _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry x))))) (abs_compose _ Lβ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs x)))))) (subst_compose _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs (x ∘ _))))))) (subst_compose _ _ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs ((_ ∘ x) ∘ _))))))) (var_subst _ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs ((_ ∘ x) ∘ _))))))) (extend_tuple_inr _ _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs ((_ ∘ (app x _)) ∘ _))))))) (inflate_var _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry (curry (uncurry (abs (x ∘ _ ∘ x))))))) (subst_U_term _ _) @ _).
        refine (maponpaths (λ x, (curry (uncurry x))) (curry_uncurry _ Lβ _) @ _).
        refine (_ @ !subst_compose _ _ _ _).
        refine (_ @ !maponpaths (λ x, (x ∘ _)) (var_subst _ _ _)).
        refine (_ @ !maponpaths (λ x, (_ ∘ x)) (var_subst _ _ _)).
        refine (_ @ !maponpaths (λ x, (x ∘ _)) (subst_exponential_term _ _ _ _)).
        refine (_ @ !maponpaths (λ x, ((exponential_term _ x x) ∘ _)) (subst_U_term _ _)).
        refine (_ @ !maponpaths (λ x, (x ∘ _)) (exponential_term_is_compose _ Lβ _ _)).
        refine (_ @ !maponpaths (λ x, ((abs (x ∘ _ ∘ x)) ∘ _)) (subst_U_term _ _)).
        refine (_ @ !abs_compose _ Lβ _ _).
        refine (_ @ !maponpaths (λ x, (abs x)) (subst_compose _ _ _ _)).
        refine (_ @ !maponpaths (λ x, (abs (x ∘ _))) (subst_compose _ _ _ _)).
        refine (_ @ !maponpaths (λ x, (abs ((_ ∘ x) ∘ _))) (var_subst _ _ _)).
        refine (_ @ !maponpaths (λ x, (abs ((_ ∘ x) ∘ _))) (extend_tuple_inr _ _ _)).
        refine (_ @ !maponpaths (λ x, (abs ((_ ∘ (app x _)) ∘ _))) (inflate_var _ _)).
        refine (_ @ !maponpaths (λ x, (abs (x ∘ _ ∘ x))) (subst_U_term _ _)).
        apply (curry_uncurry _ Lβ).
      - 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 _ _) @ _).
        do 2 (apply maponpaths).
        set (p := 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 <- (var_action _ (● 0 : stn 2) p : _ = pr11 a);
          rewrite <- (var_action _ (● 1 : stn 2) p : _ = pr12 a);
          do 2 (rewrite <- (lift_constant_action _ _ p));
          do 2 (rewrite (move_action_through_vector_2 A _ _ _));
          do 2 (rewrite <- subst_action);
          rewrite (move_action_through_vector_2 A _ _ _);
          rewrite <- subst_action;
          apply (maponpaths (λ x, aaction x p));
          refine (subst_compose _ _ _ _ @ _);
          refine (maponpaths (λ x, (x ∘ _)) (var_subst _ _ _) @ _);
          refine (maponpaths (λ x, (_ ∘ x)) (var_subst _ _ _) @ _);
          refine (maponpaths (λ x, (_ ∘ x)) (subst_pair_arrow _ _ _ _) @ _);
          refine (maponpaths (λ x, (_ ∘ (pair_arrow x _))) (var_subst _ _ _) @ _);
          refine (maponpaths (λ x, (_ ∘ (pair_arrow _ x))) (var_subst _ _ _) @ _);
          refine (_ @ !subst_compose _ _ _ (weqvecfun _ [(_ ; var _)]));
          refine (_ @ !maponpaths (λ x, (x ∘ _)) (var_subst _ _ _));
          refine (_ @ !maponpaths (λ x, (_ ∘ x)) (var_subst _ _ _));
          refine (_ @ !maponpaths (λ x, (x ∘ _)) (subst_U_term _ _));
          refine (_ @ !abs_compose _ Lβ _ _);
          refine (_ @ !maponpaths (λ x, (abs x)) (var_subst _ _ _));
          refine (_ @ !maponpaths (λ x, (abs x)) (extend_tuple_inr _ _ _)).
        + refine (maponpaths (λ x, (x ∘ _)) (subst_π1 _ _) @ _).
          apply (π1_pair_arrow _ Lβ).
        + refine (maponpaths (λ x, (x ∘ _)) (subst_π2 _ _) @ _).
          apply (π2_pair_arrow _ Lβ).

    Definition universal_monoid_exponential_iso
      : z_iso (C := monoid_action_cat lambda_algebra_monoid)
        functional_2_monoid_action
        (exponential_object (monoid_monoid_action _) (monoid_monoid_action _)).
    Show proof.
      use make_monoid_action_z_iso.
      - use make_z_iso.
        + exact functional_2_to_exponential_object_morphism_data.
        + exact exponential_object_to_functional_2_morphism_data.
        + exact is_z_iso_functional_2_exponential_object.
      - exact functional_2_to_exponential_object_is_morphism.

    Definition functional_app
      : monoid_action_morphism (monoid_monoid_action _) functional_2_monoid_action.
    Show proof.
      use make_monoid_action_morphism.
      - intro a.
        exists (compose I2 (pr1 a)).
        abstract exact (
          !maponpaths (λ x, compose x _) (I2_idempotent) @
          !compose_assoc _ _ _
        ).
      - abstract (
          intros a m;
          apply functional_2_eq;
          exact (compose_assoc _ _ _)
        ).

    Definition functional_abs
      : monoid_action_morphism functional_2_monoid_action (monoid_monoid_action _).
    Show proof.
      use make_monoid_action_morphism.
      - intro a.
        exists (pr1 a).
        exact (is_functional_2_to_is_functional_1 _ (pr2 a)).
      - intros a m.
        now apply functional_1_eq.

    Definition lambda_algebra_theory
      : lambda_theory.
    Show proof.
      use endomorphism_lambda_theory.
      - exact (monoid_action_cat lambda_algebra_monoid).
      - apply terminal_monoid_action.
      - apply binproducts_monoid_action_cat.
      - apply monoid_monoid_action.
      - apply is_exponentiable_monoid_action.
      - exact (inv_from_z_iso universal_monoid_exponential_iso · functional_abs).
      - exact (
          (functional_app : monoid_action_cat _ ⟦_, _⟧) ·
          morphism_from_z_iso _ _ universal_monoid_exponential_iso
        ).

    Lemma lambda_algebra_theory_has_beta
      : has_β lambda_algebra_theory.
    Show proof.
      apply endomorphism_theory_has_β.
      assert ((functional_abs : monoid_action_cat _⟦_, _⟧) · functional_app = identity _).
      {
        apply monoid_action_morphism_eq.
        intro a.
        apply functional_2_eq.
        exact (!pr2 a).
      }
      refine (assoc' _ _ _ @ _).
      refine (maponpaths (λ x, _ · x) (assoc _ _ _ ) @ _).
      rewrite X.
      rewrite id_left.
      apply z_iso_after_z_iso_inv.

  End Theory.

End AlgebraToTheory.