Theory CartesianClosedCategory

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

chapter "Cartesian Closed Category"

theory CartesianClosedCategory
imports CartesianCategory
begin

  text‹
    A \emph{cartesian closed category} is a cartesian category such that,
    for every object b›, the functor prod ‐ b› is a left adjoint functor.
    A right adjoint to this functor takes each object c› to the \emph{exponential}
    exp b c›.  The adjunction yields a natural bijection between hom (prod a b) c›
    and hom a (exp b c)›.
  ›

  locale cartesian_closed_category =
    cartesian_category +
  assumes left_adjoint_prod_ax: "b. ide b  left_adjoint_functor C C (λx. some_prod x b)"

  locale elementary_cartesian_closed_category =
    elementary_cartesian_category C pr0 pr1 one trm
  for C :: "'a  'a  'a"  (infixr  55)
  and pr0 :: "'a  'a  'a"  (𝔭0[_, _])
  and pr1 :: "'a  'a  'a"  (𝔭1[_, _])
  and one :: "'a"              (𝟭)
  and trm :: "'a  'a"        (𝗍[_])
  and exp :: "'a  'a  'a"
  and eval :: "'a  'a  'a"
  and curry :: "'a  'a  'a  'a  'a" +
  assumes eval_in_hom_ax: " ide b; ide c   «eval b c : prod (exp b c) b  c»"
  and ide_exp_ax [intro]: " ide b; ide c   ide (exp b c)"
  and curry_in_hom: " ide a; ide b; ide c; «g : prod a b  c» 
                           «curry a b c g : a  exp b c»"
  and uncurry_curry_ax: " ide a; ide b; ide c; «g : prod a b  c» 
                           eval b c  prod (curry a b c g) b = g"
  and curry_uncurry_ax: " ide a; ide b; ide c; «h : a  exp b c» 
                           curry a b c (eval b c  prod h b) = h"

  context cartesian_closed_category
  begin

    interpretation elementary_cartesian_category C some_pr0 some_pr1 𝟭? λa. 𝗍?[a]
      using extends_to_elementary_cartesian_category by blast

    lemma has_exponentials:
    assumes "ide b" and "ide c"
    shows "x e. ide x  «e : x ? b  c» 
                 (a g. ide a  «g : a ? b  c»  (∃!f. «f : a  x»  g = e  (f ? b)))"
    proof -
      interpret F: left_adjoint_functor C C λx. x ? b
        using assms(1) left_adjoint_prod_ax by simp
      obtain x e where e: "terminal_arrow_from_functor C C (λx. x ? b) x c e"
        using assms F.ex_terminal_arrow [of c] by auto
      interpret e: terminal_arrow_from_functor C C λx. x ? b x c e
        using e by simp
      have "a g.  ide a; «g : a ? b  c»   ∃!f. «f : a  x»  g = e  (f ? b)"
        using e.is_terminal category_axioms F.functor_axioms
        unfolding e.is_coext_def arrow_from_functor_def arrow_from_functor_axioms_def
        by simp
      thus ?thesis
        using e.arrow by metis
    qed

    definition some_exp  ("exp?")
    where "some_exp b c  SOME x. ide x 
                                    (e. «e : x ? b  c» 
                                      (a g. ide a  «g : a ? b  c»
                                               (∃!f. «f : a  x»  g = e  (f ? b))))"

    definition some_eval  ("eval?")
    where "some_eval b c  SOME e. «e : exp? b c ? b  c» 
                                     (a g. ide a  «g : a ? b  c»
                                               (∃!f. «f : a  exp? b c»  g = e (f ? b)))"

    definition some_Curry  ("Curry?")
    where "some_Curry a b c g  THE f. «f : a  exp? b c»  g = eval? b c  (f ? b)"

    lemma Curry_uniqueness:
    assumes "ide b" and "ide c"
    shows "ide (exp? b c)"
    and "«eval? b c : exp? b c ? b  c»"
    and " ide a; «g : a ? b  c»  
            ∃!f. «f : a  exp? b c»  g = eval? b c  (f ? b)"
      using assms some_exp_def some_eval_def has_exponentials
            someI_ex [of "λx. ide x  (e. «e : x ? b  c» 
                                           (a g. ide a  «g : a ? b  c»
                                               (∃!f. «f : a  x»  g = e  (f ? b))))"]
            someI_ex [of "λe. «e : exp? b c ? b  c» 
                              (a g. ide a  «g : a ? b  c»
                                            (∃!f. «f : a  exp? b c»  g = e  (f ? b)))"]
      by auto

    lemma ide_exp [intro, simp]:
    assumes "ide b" and "ide c"
    shows "ide (exp? b c)"
      using assms Curry_uniqueness(1) by force

    lemma eval_in_hom [intro]:
    assumes "ide b" and "ide c" and "x = exp? b c ? b"
    shows "«eval? b c : x  c»"
      using assms Curry_uniqueness by simp

    lemma Uncurry_Curry:
    assumes "ide a" and "ide b" and "«g : a ? b  c»"
    shows "«Curry? a b c g : a  exp? b c»  g = eval? b c  (Curry? a b c g ? b)"
    proof -
      have "ide c"
        using assms(3) by auto
      thus ?thesis
        using assms some_Curry_def Curry_uniqueness
              theI' [of "λf. «f : a  exp? b c»  g = eval? b c  (f ? b)"]
        by simp
    qed

    lemma Curry_Uncurry:
    assumes "ide b" and "ide c" and "«h : a  exp? b c»"
    shows "Curry? a b c (eval? b c  (h ? b)) = h"
    proof -
      have "∃!f. «f : a  exp? b c»  eval? b c  (h ? b) = eval? b c  (f ? b)"
      proof -
        have "ide a  «eval? b c  (h ? b) : (a ? b)  c»"
        proof (intro conjI)
          show "ide a"
            using assms(3) by auto
          show "«eval? b c  (h ? b) : a ? b  c»"
            using assms by (intro comp_in_homI) auto
        qed
        thus ?thesis
          using assms Curry_uniqueness by simp
      qed
      moreover have "«h : a  exp? b c»  eval? b c  (h ? b) = eval? b c  (h ? b)"
        using assms by simp
      ultimately show ?thesis
        using assms some_Curry_def Curry_uniqueness Uncurry_Curry
              the1_equality [of "λf. «f : a  exp? b c» 
                                     eval? b c  (h ? b) = eval? b c  (f ? b)"]
        by simp
    qed

    lemma Curry_in_hom [intro]:
    assumes "ide a" and "ide b" and "«g : a ? b  c»"
    shows "«Curry? a b c g : a  exp? b c»"
      using assms
      by (simp add: Uncurry_Curry)

    lemma Curry_simps [simp]:
    assumes "ide a" and "ide b" and "«g : a ? b  c»"
    shows "arr (Curry? a b c g)"
    and "dom (Curry? a b c g) = a"
    and "cod (Curry? a b c g) = exp? b c"
      using assms Curry_in_hom by blast+

    lemma eval_simps [simp]:
    assumes "ide b" and "ide c" and "x = (exp? b c) ? b"
    shows "arr (eval? b c)"
    and "dom (eval? b c) = x"
    and "cod (eval? b c) = c"
      using assms eval_in_hom by auto

    interpretation elementary_cartesian_closed_category C some_pr0 some_pr1
                     𝟭? λa. 𝗍?[a] some_exp some_eval some_Curry
      using Curry_uniqueness Uncurry_Curry Curry_Uncurry
      apply unfold_locales by auto

    lemma extends_to_elementary_cartesian_closed_category:
    shows "elementary_cartesian_closed_category C some_pr0 some_pr1
             𝟭? (λa. 𝗍?[a]) some_exp some_eval some_Curry"
      ..

    lemma has_as_exponential:
    assumes "ide b" and "ide c"
    shows "has_as_exponential b c (exp? b c) (eval? b c)"
    proof
      show "ide b" by fact
      show "ide (exp? b c)"
        using assms by simp
      show "«some_eval b c : exp? b c ? b  c»"
        using assms by auto
      show "a g. ide a; «g : a ? b  c» 
                     ∃!f. «f : a  exp? b c»  g = eval? b c  (f ? b)"
        by (simp add: assms Curry_uniqueness(3))
    qed

    lemma has_as_exponential_iff:
    shows "has_as_exponential b c x e 
           ide b  «e : x ? b  c» 
           (h. «h : x  exp? b c»  e = eval? b c  (h ? b)  iso h)"
    proof
      assume 1: "has_as_exponential b c x e"
      moreover have 2: "has_as_exponential b c (exp? b c) (eval? b c)"
        using 1 ide_cod has_as_exponential_def in_homE
        by (metis has_as_exponential)
      ultimately show "ide b  «e : x ? b  c» 
                       (h. «h : x  exp? b c»  e = eval? b c  (h ? b)  iso h)"
        by (metis exponentials_are_isomorphic(2) has_as_exponentialE)
      next
      assume 1: "ide b  «e : x ? b  c» 
                 (h. «h : x  exp? b c»  e = eval? b c  (h ? b)  iso h)"
      have c: "ide c"
        using 1 ide_cod in_homE by metis
      have 2: "has_as_exponential b c (exp? b c) (eval? b c)"
        by (simp add: 1 c eval_in_hom_ax Curry_uniqueness(3) has_as_exponential_def)
      obtain h where h: "«h : x  exp? b c»  e = eval? b c  (h ? b)  iso h"
        using 1 by blast
      show "has_as_exponential b c x e"
      proof (unfold has_as_exponential_def, intro conjI)
        show "ide b" and "ide x" and "«e : x ? b  c»"
          using 1 h ide_dom by blast+
        show "y g. ide y  «g : y ? b  c»  (∃!f. «f : y  x»  g = e  (f ? b))"
        proof (intro allI impI)
          fix y g
          assume 3: "ide y  «g : y ? b  c»"
          obtain k where k: "«k : y  exp? b c»  g = eval? b c  (k ? b)"
            by (metis 3 ide b c Curry_uniqueness(3))
          show "∃!f. «f : y  x»  g = e  (f ? b)"
          proof -
            let ?f = "inv h  k"
            have f: "«?f : y  x»"
              by (meson comp_in_homI inv_in_hom h k)
            moreover have "g = e  (?f ? b)"
            proof -
              have "e  some_prod ?f b = e  some_prod (inv h  k) (b  b)"
                by (simp add: 1)
              also have "... = e  (inv h ? b)  (k ? b)"
                by (metis ide b f arrI comp_ide_self interchange ide_compE)
              also have "... = (e  (inv h ? b))  (k ? b)"
                using comp_assoc by simp
              also have "... = eval? b c  (k ? b)"
                by (metis «e : x ? b  c» h ide b arrI inv_prod(1-2) ide_is_iso
                    inv_ide invert_side_of_triangle(2))
              also have "... = g"
                using k by blast
              finally show ?thesis by blast
            qed
            moreover have "f'. «f' : y  x»  g = e  (f' ? b)  f' = ?f"
            proof -
              fix f'
              assume f': "«f' : y  x»  g = e  (f' ? b)"
              have "«h  f' : y  exp? b c»  g = eval? b c  (h  f' ? b)"
                using f' h ide b comp_assoc interchange seqI' by fastforce
              hence "C h f' = C h ?f"
                by (metis ide b arrI c h k Curry_Uncurry invert_side_of_triangle(1))
              thus "f' = ?f"
                using f h iso_cancel_left by auto
            qed
            ultimately show ?thesis by blast
          qed
        qed
      qed
    qed

  end

  context elementary_cartesian_closed_category
  begin

    lemma left_adjoint_prod:
    assumes "ide b"
    shows "left_adjoint_functor C C (λx. x  b)"
    proof -
      interpret "functor" C C λx. x  b
        using assms interchange
        apply unfold_locales
            apply auto
        using prod_def tuple_def
        by auto
      interpret left_adjoint_functor C C λx. x  b
      proof
        show "c. ide c  x e. terminal_arrow_from_functor C C (λx. x  b) x c e"
        proof -
          fix c
          assume c: "ide c"
          show "x e. terminal_arrow_from_functor C C (λx. x  b) x c e"
          proof (intro exI)
            interpret arrow_from_functor C C λx. x  b exp b c c eval b c
              using assms c eval_in_hom_ax
              by (unfold_locales, auto)
            show "terminal_arrow_from_functor C C (λx. x  b) (exp b c) c (eval b c)"
            proof
              show "a f. arrow_from_functor C C (λx. x  b) a c f 
                            ∃!g. arrow_from_functor.is_coext C C
                                   (λx. x  b) (exp b c) (eval b c) a f g"
              proof -
                fix a f
                assume f: "arrow_from_functor C C (λx. x  b) a c f"
                interpret f: arrow_from_functor C C λx. x  b a c f
                  using f by simp
                show "∃!g. is_coext a f g"
                proof
                  have a: "ide a"
                    using f.arrow by simp
                  show "is_coext a f (curry a b c f)"
                    unfolding is_coext_def
                    using assms a c curry_in_hom uncurry_curry_ax f.arrow by simp
                  show "g. is_coext a f g  g = curry a b c f"
                    unfolding is_coext_def
                    using assms a c curry_uncurry_ax f.arrow by simp
                qed
              qed
            qed
          qed
        qed
      qed
      show ?thesis ..
    qed

    sublocale cartesian_category C
      using is_cartesian_category by simp

    sublocale cartesian_closed_category C
    proof -
      interpret CCC: elementary_cartesian_category
                       C some_pr0 some_pr1 some_terminal some_terminator
        using extends_to_elementary_cartesian_category by blast
      show "cartesian_closed_category C"
      proof     
        fix b
        assume b: "ide b"
        interpret left_adjoint_functor C C λx. CCC.prod x b
        proof -
          (*
           * We know that (λx. x ⊗ b) is a left adjoint functor, where ⊗ is the
           * product ultimately defined in terms of the projections that are parameters
           * to the elementary_category_with_binary_products locale that is the present context.
           * This is not necessarily the same as (λx. CCC.prod x b), which is defined in terms
           * of projections chosen arbitrarily in category_with_binary_products.
           * However, since they are both categorical products, they are naturally isomorphic,
           * so one is a left adjoint functor if and only if the other is.
           *)
          have "naturally_isomorphic C C (λx. x  b) (λx. CCC.prod x b)"
          proof -
            interpret CC: product_category C C ..
            interpret X: binary_functor C C C λfg. fst fg  snd fg
              using binary_functor_Prod(1) by auto
            interpret Xb: "functor" C C λx. x  b
              using b X.fixing_ide_gives_functor_2 by simp
            interpret prod: binary_functor C C C λfg. CCC.prod (fst fg) (snd fg)
              using CCC.binary_functor_Prod(1) by simp
            interpret prod_b: "functor" C C λx. CCC.prod x b
               using b prod.fixing_ide_gives_functor_2 by simp
            interpret φ: transformation_by_components C C λx. x  b λx. CCC.prod x b
                           λa. CCC.tuple 𝔭1[a, b] 𝔭0[a, b]
              using b CCC.prod_tuple by unfold_locales auto
            interpret φ: natural_isomorphism C C λx. x  b λx. CCC.prod x b φ.map
            proof
              fix a
              assume a: "ide a"
              show "iso (φ.map a)"
              proof
                show "inverse_arrows (φ.map a) some_pr1 a b, some_pr0 a b"
                  using a b by auto
              qed
            qed
            show ?thesis
              using naturally_isomorphic_def φ.natural_isomorphism_axioms by blast
          qed
          moreover have "left_adjoint_functor C C (λx. x  b)"
            using b left_adjoint_prod by simp
          ultimately show "left_adjoint_functor C C (λx. CCC.prod x b)"
            using left_adjoint_functor_respects_naturally_isomorphic by auto
        qed
        show "f. ¬ arr f  some_prod f b = null"
          using is_extensional by blast
        show "g f. seq g f  some_prod (g  f) b = some_prod g b  some_prod f b"
          by simp
        show "y. ide y  x e. terminal_arrow_from_functor (⋅) (⋅) (λx. some_prod x b) x y e"
          using ex_terminal_arrow by simp
      qed auto
    qed

    lemma is_cartesian_closed_category:
    shows "cartesian_closed_category C"
      ..

  end

end