Theory CartesianClosedMonoidalCategory

(*  Title:       CartesianClosedMonoidalCategory
    Author:      Eugene W. Stark <stark@cs.stonybrook.edu>, 2024
    Maintainer:  Eugene W. Stark <stark@cs.stonybrook.edu>
*)

section "Cartesian Closed Monoidal Categories"

text‹
  A \emph{cartesian closed monoidal category} is a cartesian monoidal category that is a
  closed monoidal category with respect to a chosen product.  This is not quite the same
  thing as a cartesian closed category, because a cartesian monoidal category
  (being a monoidal category) has chosen structure (the tensor, associators, and unitors),
  whereas we have defined a cartesian closed category to be an abstract category satisfying
  certain properties that are expressed without assuming any chosen structure.

›

theory CartesianClosedMonoidalCategory
imports Category3.CartesianClosedCategory MonoidalCategory.CartesianMonoidalCategory
        ClosedMonoidalCategory
begin

  locale cartesian_closed_monoidal_category =
    cartesian_monoidal_category +
    closed_monoidal_category

  locale elementary_cartesian_closed_monoidal_category =
    cartesian_monoidal_category +
    elementary_closed_monoidal_category
  begin

    lemmas prod_eq_tensor [simp]

  end

  text‹
    The following is the main purpose for the current theory: to show that a
    cartesian closed category with chosen structure determines a cartesian closed
    monoidal category.
  ›

  context elementary_cartesian_closed_category
  begin

    interpretation CMC: cartesian_monoidal_category C Prod α ι
      using extends_to_cartesian_monoidal_categoryECC by blast

    interpretation CMC: closed_monoidal_category C Prod α ι
      using CMC.T.is_extensional interchange left_adjoint_prod
      by unfold_locales
         (auto simp add: left_adjoint_functor.ex_terminal_arrow)

    lemma extends_to_closed_monoidal_categoryECCC:
    shows "closed_monoidal_category C Prod α ι"
      ..

    lemma extends_to_cartesian_closed_monoidal_categoryECCC:
    shows "cartesian_closed_monoidal_category C Prod α ι"
      ..

    interpretation CMC: elementary_monoidal_category
                          C CMC.tensor CMC.unity CMC.lunit CMC.runit CMC.assoc
      using CMC.induces_elementary_monoidal_category by blast

    interpretation CMC: elementary_closed_monoidal_category
                         C Prod α ι exp eval curry
      using eval_in_hom_ax curry_in_hom uncurry_curry_ax curry_uncurry_ax
      by unfold_locales auto

    lemma extends_to_elementary_closed_monoidal_categoryECCC:
    shows "elementary_closed_monoidal_category C Prod α ι exp eval curry"
      ..

    lemma extends_to_elementary_cartesian_closed_monoidal_categoryECCC:
    shows "elementary_cartesian_closed_monoidal_category C Prod α ι exp eval curry"
      ..

  end

  context elementary_cartesian_closed_monoidal_category
  begin

    interpretation elementary_monoidal_category C tensor unity lunit runit assoc
      using induces_elementary_monoidal_category by blast

    text ‹
      The following fact is not used in the present article, but it is a natural
      and likely useful lemma for which I constructed a proof at one point.
      The proof requires cartesianness; I suspect this is essential, but I am not
      absolutely certain of it.
    ›

    lemma isomorphic_exp_prod:
    assumes "ide a" and "ide b" and "ide x"
    shows "«Curry[exp x (a  b), x, a] (𝔭1[a, b]  eval x (a  b)),
             Curry[exp x (a  b), x, b] (𝔭0[a, b]  eval x (a  b))
               : exp x (a  b)  exp x a  exp x b»"
        (is "«?C, ?D : exp x (a  b)  exp x a  exp x b»")
    and "«Curry[exp x a  exp x b, x, a  b]
               eval x a  𝔭1[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                           𝔭0[exp x a  exp x b, x],
                eval x b  𝔭0[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                           𝔭0[exp x a  exp x b, x]
             : exp x a  exp x b  exp x (a  b)»"
        (is "«Curry[exp x a  exp x b, x, a  b] ?A, ?B
                : exp x a  exp x b  exp x (a  b)»")
    and "inverse_arrows
           (Curry[exp x a  exp x b, x, a  b]
              eval x a  𝔭1[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                          𝔭0[exp x a  exp x b, x],
               eval x b  𝔭0[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                          𝔭0[exp x a  exp x b, x])
           Curry[exp x (a  b), x, a] (𝔭1[a, b]  eval x (a  b)),
            Curry[exp x (a  b), x, b] (𝔭0[a, b]  eval x (a  b))"
    and "isomorphic (exp x (a  b)) (exp x a  exp x b)"
    proof -
      have A: "«?A : (exp x a  exp x b)  x  a»"
        using assms by auto
      have B: "«?B : (exp x a  exp x b)  x  b»"
        using assms by auto
      have AB: "«?A, ?B : (exp x a  exp x b)  x  a  b»"
        by (metis A B ECC.tuple_in_hom prod_eq_tensor)
      have C: "«?C : exp x (a  b)  exp x a»"
        using assms by auto
      have D: "«?D : exp x (a  b)  exp x b»"
        using assms by auto
      show CD: "«?C, ?D : exp x (a  b)  exp x a  exp x b»"
        using C D by fastforce
      show 1: "«Curry[exp x a  exp x b, x, a  b] ?A, ?B
                  : (exp x a  exp x b)  exp x (a  b)»"
        by (simp add: AB assms(1-3) Curry_in_hom)
      show "inverse_arrows (Curry[exp x a  exp x b, x, a  b] ?A, ?B) ?C, ?D"
      proof
        show "ide (Curry[exp x a  exp x b, x, a  b] ?A, ?B  ?C, ?D)"
        proof -
          have "Curry[exp x a  exp x b, x, a  b] ?A, ?B  ?C, ?D =
                Curry[exp x (a  b), x, a  b] (?A, ?B  (?C, ?D  x))"
            using assms AB CD comp_Curry_arr by presburger
          also have "... = Curry[exp x (a  b), x, a  b]
                             ?A  (?C, ?D  x), ?B  (?C, ?D  x)"
          proof -
            have "span ?A ?B"
              using A B by fastforce
            moreover have "arr (?C, ?D  x)"
              using assms CD by auto
            moreover have "dom ?A = cod (?C, ?D  x)"
              by (metis A CD assms(3) cod_tensor ide_char in_homE)
            ultimately show ?thesis
              using assms ECC.comp_tuple_arr by metis
          qed
          also have "... = Curry[exp x (a  b), x, a  b]
                             Uncurry[x, a] ?C, eval x b  (?D  x)"
          proof -
            have "?A  (?C, ?D  x) = Uncurry[x, a] ?C"
            proof -
              have "?A  (?C, ?D  x) =
                    eval x a 
                      𝔭1[exp x a, exp x b]  𝔭1[exp x a  exp x b, x]  (?C, ?D  x),
                       𝔭0[exp x a  exp x b, x]  (?C, ?D  x)"
                using assms ECC.comp_tuple_arr comp_assoc by simp
              also have "... = eval x a 
                                 ?C  𝔭1[exp x (a  b), x], x  𝔭0[exp x (a  b), x]"
                using assms ECC.pr_naturality(1-2) by auto
              also have "... = eval x a  (?C  x) 
                                 𝔭1[exp x (a  b), x], 𝔭0[exp x (a  b), x]"
                using assms
                      ECC.prod_tuple
                        [of "𝔭1[exp x (a  b), x]" "𝔭0[exp x (a  b), x]" ?C x]
                by simp
              also have "... = Uncurry[x, a] ?C"
                using assms C ECC.tuple_pr comp_arr_ide comp_arr_dom by auto
              finally show ?thesis by blast
            qed
            moreover have "?B  (?C, ?D  x) = Uncurry[x, b] ?D"
            proof -
              have "?B  (?C, ?D  x) =
                    eval x b 
                      𝔭0[exp x a, exp x b]  𝔭1[exp x a  exp x b, x]  (?C, ?D  x),
                       𝔭0[exp x a  exp x b, x]  (?C, ?D  x)"
                using assms ECC.comp_tuple_arr comp_assoc by simp
              also have "... = eval x b 
                                 ?D  𝔭1[exp x (a  b), x], x  𝔭0[exp x (a  b), x]"
                using assms C ECC.pr_naturality(1-2) by auto
              also have "... = eval x b  (?D  x) 
                                 𝔭1[exp x (a  b), x], 𝔭0[exp x (a  b), x]"
                using assms
                      ECC.prod_tuple
                        [of "𝔭1[exp x (a  b), x]" "𝔭0[exp x (a  b), x]" ?D x]
                by simp
              also have "... = Uncurry[x, b] ?D"
                using assms C ECC.tuple_pr comp_arr_ide comp_arr_dom by auto
              finally show ?thesis by blast
            qed
            ultimately show ?thesis by simp
          qed
          also have "... = Curry[exp x (a  b), x, a  b]
                             (𝔭1[a, b]  eval x (a  b), 𝔭0[a, b]  eval x (a  b))"
            using assms Uncurry_Curry by auto
          also have "... = Curry[exp x (a  b), x, a  b]
                             (𝔭1[a, b], 𝔭0[a, b]  eval x (a  b))"
            using assms ECC.comp_tuple_arr [of "𝔭1[a, b]" "𝔭0[a, b]" "eval x (a  b)"]
            by simp
          also have "... = Curry[exp x (a  b), x, a  b] (eval x (a  b))"
            using assms comp_cod_arr by simp
          also have "... = exp x (a  b)"
            using assms Curry_Uncurry ide_exp ide_in_hom tensor_preserves_ide
                  Uncurry_exp
            by metis
          finally have "Curry[exp x a  exp x b, x, a  b] ?A, ?B  ?C, ?D =
                        exp x (a  b)"
            by blast
          thus ?thesis
            using assms ide_exp tensor_preserves_ide by presburger
        qed
        show "ide (?C, ?D  Curry[exp x a  exp x b, x, a  b] ?A, ?B)"
        proof -
          have 2: "span 𝔭1[exp x a  exp x b, x] 𝔭0[exp x a  exp x b, x]"
            using assms by simp
          have 3: "seq x 𝔭0[exp x a  exp x b, x]"
            using assms by simp
          have "?C, ?D  Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                ?C  Curry[exp x a  exp x b, x, a  b] ?A, ?B,
                 ?D  Curry[exp x a  exp x b, x, a  b] ?A, ?B"
            using assms C D 1 ECC.comp_tuple_arr by (metis in_homE)
          also have "... = 𝔭1[exp x a, exp x b], 𝔭0[exp x a, exp x b]"
          proof -
            have "Curry[exp x (a  b), x, a] (𝔭1[a, b]  eval x (a  b)) 
                    Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                  𝔭1[exp x a, exp x b]"
            proof -
              have "Curry[exp x (a  b), x, a] (𝔭1[a, b]  eval x (a  b)) 
                      Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                    Curry[exp x a  exp x b, x, a]
                      ((𝔭1[a, b]  eval x (a  b)) 
                         (Curry[exp x a  exp x b, x, a  b] ?A, ?B  x))"
                using assms 1 comp_Curry_arr by auto
              also have "... = Curry[exp x a  exp x b, x, a]
                                 (𝔭1[a, b]  eval x (a  b) 
                                    (Curry[exp x a  exp x b, x, a  b] ?A, ?B  x))"
                using comp_assoc by simp
              also have "... = Curry[exp x a  exp x b, x, a] (𝔭1[a, b]  ?A, ?B)"
                using assms AB Uncurry_Curry ide_exp tensor_preserves_ide by simp
              also have "... = Curry[exp x a  exp x b, x, a]
                                (eval x a 
                                   𝔭1[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                                    𝔭0[exp x a  exp x b, x])"
                using assms A B ECC.pr_tuple(1) by fastforce
              also have "... = Curry[exp x a  exp x b, x, a]
                                (eval x a  (𝔭1[exp x a, exp x b]  x) 
                                              𝔭1[exp x a  exp x b, x],
                                               𝔭0[exp x a  exp x b, x])"
              proof -
                have "seq 𝔭1[exp x a, exp x b] 𝔭1[exp x a  exp x b, x]"
                  using assms by auto
                thus ?thesis
                  using assms 2 3 prod_eq_tensor comp_ide_arr ECC.prod_tuple
                  by metis
              qed
              also have "... = Curry (exp x a  exp x b) x a
                                 (eval x a  (𝔭1[exp x a, exp x b]  x))"
                using assms comp_arr_dom by simp
              also have "... = 𝔭1[exp x a, exp x b]"
                using assms Curry_Uncurry by simp
              finally show ?thesis by blast
            qed
            moreover have "Curry[exp x (a  b), x, b] (𝔭0[a, b]  eval x (a  b)) 
                             Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                           𝔭0[exp x a, exp x b]"
            proof -
              have "Curry[exp x (a  b), x, b] (𝔭0[a, b]  eval x (a  b)) 
                      Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                    Curry[exp x a  exp x b, x, b]
                      ((𝔭0[a, b]  eval x (a  b)) 
                         (Curry[exp x a  exp x b, x, a  b] ?A, ?B  x))"
              proof -
                have "«Curry[exp x a  exp x b, x, a  b] ?A, ?B
                         : exp x a  exp x b  exp x (a  b)»"
                  using 1 by blast
                moreover have "«𝔭0[a, b]  eval x (a  b) : exp x (a  b)  x  b»"
                  using assms
                  by (metis (no_types, lifting) ECC.pr0_in_hom' ECC.pr_simps(2)
                      comp_in_homI eval_in_homECMC prod_eq_tensor tensor_preserves_ide)
                ultimately show ?thesis
                  using assms comp_Curry_arr by simp
              qed
              also have "... = Curry[exp x a  exp x b, x, b]
                                 (𝔭0[a, b] 
                                    Uncurry[x, a  b]
                                      (Curry[exp x a  exp x b, x, a  b] ?A, ?B))"
                using comp_assoc by simp
              also have "... = Curry (exp x a  exp x b) x b (𝔭0[a, b]  ?A, ?B)"
                using assms AB Uncurry_Curry ide_exp tensor_preserves_ide by simp
              also have "... = Curry[exp x a  exp x b, x, b]
                                 (eval x b 
                                   𝔭0[exp x a, exp x b]  𝔭1[exp x a  exp x b, x],
                                    𝔭0[exp x a  exp x b, x])"
                using assms A B by fastforce
              also have "... = Curry[exp x a  exp x b, x, b]
                                 (eval x b  (𝔭0[exp x a, exp x b]  x) 
                                              𝔭1[exp x a  exp x b, x],
                                               𝔭0[exp x a  exp x b, x])"
              proof -
                have "seq 𝔭0[exp x a, exp x b] 𝔭1[exp x a  exp x b, x]"
                  using assms by auto
                thus ?thesis
                  using assms 2 3 prod_eq_tensor comp_ide_arr ECC.prod_tuple
                  by metis
              qed
              also have "... = Curry (exp x a  exp x b) x b
                                 (Uncurry[x, b] 𝔭0[exp x a, exp x b])"
              proof -
                have "(𝔭0[exp x a, exp x b]  x) 
                        𝔭1[exp x a  exp x b, x], 𝔭0[exp x a  exp x b, x] =
                      𝔭0[exp x a, exp x b]  x"
                  using assms comp_arr_ide ECC.tuple_pr by auto
                thus ?thesis by simp
              qed
              also have "... = 𝔭0[exp x a, exp x b]"
                using assms Curry_Uncurry by simp
              finally show ?thesis by blast
            qed
            ultimately show ?thesis by simp
          qed
          also have "... = exp x a  exp x b"
            using assms ECC.tuple_pr by simp
          finally have "?C, ?D  Curry[exp x a  exp x b, x, a  b] ?A, ?B =
                        exp x a  exp x b"
            by blast
          thus ?thesis
            using assms tensor_preserves_ide by simp
        qed
      qed
      thus "isomorphic (exp x (a  b)) (exp x a  exp x b)"
        unfolding isomorphic_def
        using CD by blast
    qed

  end

end