Theory EquivalenceOfCategories

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

chapter "Equivalence of Categories"

text ‹
  In this chapter we define the notions of equivalence and adjoint equivalence of categories
  and establish some properties of functors that are part of an equivalence.
›

theory EquivalenceOfCategories
imports Adjunction
begin

  locale equivalence_of_categories =
    C: category C +
    D: category D +
    F: "functor" D C F +
    G: "functor" C D G +
    η: natural_isomorphism D D D.map "G o F" η +
    ε: natural_isomorphism C C "F o G" C.map ε
  for C :: "'c comp"     (infixr C 55)
  and D :: "'d comp"     (infixr D 55)
  and F :: "'d  'c"
  and G :: "'c  'd"
  and η :: "'d  'd"
  and ε :: "'c  'c"
  begin

    notation C.in_hom    («_ : _ C _»)
    notation D.in_hom    («_ : _ D _»)

    lemma C_arr_expansion:
    assumes "C.arr f"
    shows "ε (C.cod f) C F (G f) C C.inv (ε (C.dom f)) = f"
    and "C.inv (ε (C.cod f)) C f C ε (C.dom f) = F (G f)"
    proof -
      have ε_dom: "C.inverse_arrows (ε (C.dom f)) (C.inv (ε (C.dom f)))"
        using assms C.inv_is_inverse by auto
      have ε_cod: "C.inverse_arrows (ε (C.cod f)) (C.inv (ε (C.cod f)))"
        using assms C.inv_is_inverse by auto
      have "ε (C.cod f) C F (G f) C C.inv (ε (C.dom f)) =
            (ε (C.cod f) C F (G f)) C C.inv (ε (C.dom f))"
        using C.comp_assoc by force
      also have 1: "... = (f C ε (C.dom f)) C C.inv (ε (C.dom f))"
        using assms ε.naturality by simp
      also have 2: "... = f"
        using assms ε_dom C.comp_arr_inv C.comp_arr_dom C.comp_assoc by force
      finally show "ε (C.cod f) C F (G f) C C.inv (ε (C.dom f)) = f" by blast
      show "C.inv (ε (C.cod f)) C f C ε (C.dom f) = F (G f)"
        using assms 1 2 ε_dom ε_cod C.invert_side_of_triangle C.isoI C.iso_inv_iso
        by metis
    qed

    lemma G_is_faithful:
    shows "faithful_functor C D G"
    proof
      fix f f'
      assume par: "C.par f f'" and eq: "G f = G f'"
      show "f = f'"
      proof -
        have "C.inv (ε (C.cod f))  C.hom (C.cod f) (F (G (C.cod f))) 
              C.iso (C.inv (ε (C.cod f)))"
          using par by auto
        moreover have 1: "ε (C.dom f)  C.hom (F (G (C.dom f))) (C.dom f) 
                          C.iso (ε (C.dom f))"
          using par by auto
        ultimately have 2: "f C ε (C.dom f) = f' C ε (C.dom f)"
          using par C_arr_expansion eq C.iso_is_section C.section_is_mono
          by (metis C_arr_expansion(1) eq)
        show ?thesis
        proof -
          have "C.epi (ε (C.dom f))"
            using 1 par C.iso_is_retraction C.retraction_is_epi by blast
          thus ?thesis using 2 par by auto
        qed
      qed
    qed

    lemma G_is_essentially_surjective:
    shows "essentially_surjective_functor C D G"
    proof
      fix b
      assume b: "D.ide b"
      have "C.ide (F b)  D.isomorphic (G (F b)) b"
      proof
        show "C.ide (F b)" using b by simp
        show "D.isomorphic (G (F b)) b"
        proof (unfold D.isomorphic_def)
          have "«D.inv (η b) : G (F b) D b»  D.iso (D.inv (η b))"
            using b by auto
          thus "f. «f : G (F b) D b»  D.iso f" by blast
        qed
      qed
      thus "a. C.ide a  D.isomorphic (G a) b"
        by blast
    qed

    interpretation ε_inv: inverse_transformation C C F o G C.map ε ..
    interpretation η_inv: inverse_transformation D D D.map G o F η ..
    interpretation GF: equivalence_of_categories D C G F ε_inv.map η_inv.map ..

    lemma F_is_faithful:
    shows "faithful_functor D C F"
      using GF.G_is_faithful by simp

    lemma F_is_essentially_surjective:
    shows "essentially_surjective_functor D C F"
      using GF.G_is_essentially_surjective by simp

    lemma G_is_full:
    shows "full_functor C D G"
    proof
      fix a a' g
      assume a: "C.ide a" and a': "C.ide a'"
      assume g: "«g : G a D G a'»"
      show "f. «f : a C a'»  G f = g"
      proof
        have εa: "C.inverse_arrows (ε a) (C.inv (ε a))"
          using a C.inv_is_inverse by auto
        have εa': "C.inverse_arrows (ε a') (C.inv (ε a'))"
          using a' C.inv_is_inverse by auto
        let ?f = "ε a' C F g C C.inv (ε a)"
        have f: "«?f : a C a'»"
          using a a' g εa εa' ε.preserves_hom [of a' a' a'] ε_inv.preserves_hom [of a a a]
          by fastforce
        moreover have "G ?f = g"
        proof -
          interpret F: faithful_functor D C F
            using F_is_faithful by auto
          have "F (G ?f) = F g"
          proof -
            have "F (G ?f) = C.inv (ε a') C ?f C ε a"
              using f C_arr_expansion(2) [of "?f"] by auto
            also have "... = (C.inv (ε a') C ε a') C F g C C.inv (ε a) C ε a"
              using a a' f g C.comp_assoc by fastforce
            also have "... = F g"
              using a a' g εa εa' C.comp_inv_arr C.comp_arr_dom C.comp_cod_arr by auto
            finally show ?thesis by blast
          qed
          moreover have "D.par (G (ε a' C F g C C.inv (ε a))) g"
            using f g by fastforce
          ultimately show ?thesis using f g F.is_faithful by blast
        qed
        ultimately show "«?f : a C a'»  G ?f = g" by blast
      qed
    qed

  end

  (* I'm not sure why I had to close and re-open the context here in order to
   * get the G_is_full fact in the interpretation GF. *)

  context equivalence_of_categories
  begin

    interpretation ε_inv: inverse_transformation C C F o G C.map ε ..
    interpretation η_inv: inverse_transformation D D D.map G o F η ..
    interpretation GF: equivalence_of_categories D C G F ε_inv.map η_inv.map ..

    lemma F_is_full:
    shows "full_functor D C F"
      using GF.G_is_full by simp

  end

  text ‹
    Traditionally the term "equivalence of categories" is also used for a functor
    that is part of an equivalence of categories.  However, it seems best to use
    that term for a situation in which all of the structure of an equivalence is
    explicitly given, and to have a different term for one of the functors involved.
›

  locale equivalence_functor =
    C: category C +
    D: category D +
    "functor" C D G
  for C :: "'c comp"     (infixr C 55)
  and D :: "'d comp"     (infixr D 55)
  and G :: "'c  'd" +
  assumes induces_equivalence: "F η ε. equivalence_of_categories C D F G η ε"
  begin

    notation C.in_hom    («_ : _ C _»)
    notation D.in_hom    («_ : _ D _»)

  end

  sublocale equivalence_of_categories  equivalence_functor C D G
    using equivalence_of_categories_axioms by (unfold_locales, blast)

  text ‹
    An equivalence functor is fully faithful and essentially surjective.
›

  sublocale equivalence_functor  fully_faithful_functor C D G
  proof -
    obtain F η ε where 1: "equivalence_of_categories C D F G η ε"
      using induces_equivalence by blast
    interpret equivalence_of_categories C D F G η ε
      using 1 by auto
    show "fully_faithful_functor C D G"
      using G_is_full G_is_faithful fully_faithful_functor.intro by auto
  qed

  sublocale equivalence_functor  essentially_surjective_functor C D G
  proof -
    obtain F η ε where 1: "equivalence_of_categories C D F G η ε"
      using induces_equivalence by blast
    interpret equivalence_of_categories C D F G η ε
      using 1 by auto
    show "essentially_surjective_functor C D G"
      using G_is_essentially_surjective by auto
  qed

  lemma (in inverse_functors) induce_equivalence:
  shows "equivalence_of_categories A B F G B.map A.map"
    using inv inv' A.is_extensional B.is_extensional B.comp_arr_dom B.comp_cod_arr
          A.comp_arr_dom A.comp_cod_arr
    by unfold_locales auto

  lemma (in invertible_functor) is_equivalence:
  shows "equivalence_functor A B G"
    using equivalence_functor_axioms.intro equivalence_functor_def equivalence_of_categories_def
          induce_equivalence
    by blast

  lemma (in identity_functor) is_equivalence:
  shows "equivalence_functor C C map"
  proof -
    interpret inverse_functors C C map map
      using map_def by unfold_locales auto
    interpret invertible_functor C C map
      using inverse_functors_axioms
      by unfold_locales blast
    show ?thesis
      using is_equivalence by blast
  qed

  text ‹
    A special case of an equivalence functor is an endofunctor F› equipped with
    a natural isomorphism from F› to the identity functor.
›

  context endofunctor
  begin

    lemma isomorphic_to_identity_is_equivalence:
    assumes "natural_isomorphism A A F A.map φ"
    shows "equivalence_functor A A F"
    proof -
      interpret φ: natural_isomorphism A A F A.map φ
         using assms by auto
      interpret φ': inverse_transformation A A F A.map φ ..
      interpret Fφ': natural_isomorphism A A F F o F F o φ'.map
      proof -
        interpret Fφ': natural_transformation A A F F o F F o φ'.map
          using φ'.natural_transformation_axioms functor_axioms
                horizontal_composite [of A A A.map F φ'.map A F F F]
          by simp
        show "natural_isomorphism A A F (F o F) (F o φ'.map)"
          apply unfold_locales
          using φ'.components_are_iso by fastforce
      qed
      interpret Fφ'oφ': vertical_composite A A A.map F F o F φ'.map F o φ'.map ..
      interpret Fφ'oφ': natural_isomorphism A A A.map F o F Fφ'oφ'.map
        using φ'.natural_isomorphism_axioms Fφ'.natural_isomorphism_axioms
              natural_isomorphisms_compose
        by fast
      interpret inv_Fφ'oφ': inverse_transformation A A A.map F o F Fφ'oφ'.map ..
      interpret F: equivalence_of_categories A A F F Fφ'oφ'.map inv_Fφ'oφ'.map ..
      show ?thesis ..
    qed

  end

  locale dual_equivalence_of_categories =
    E: equivalence_of_categories
  begin

    interpretation Cop: dual_category C ..
    interpretation Dop: dual_category D ..
    interpretation Fop: dual_functor D C F ..
    interpretation Gop: dual_functor C D G ..
    interpretation Gop_o_Fop: composite_functor Dop.comp Cop.comp Dop.comp Fop.map Gop.map ..
    interpretation Fop_o_Gop: composite_functor Cop.comp Dop.comp Cop.comp Gop.map Fop.map ..
    sublocale η': inverse_transformation D D E.D.map G  F η ..
    interpretation ηop: natural_transformation Dop.comp Dop.comp Dop.map Gop_o_Fop.map η'.map
      using η'.is_extensional η'.is_natural_1 η'.is_natural_2
      by unfold_locales auto
    interpretation ηop: natural_isomorphism Dop.comp Dop.comp Dop.map Gop_o_Fop.map η'.map
      by unfold_locales auto
    sublocale ε': inverse_transformation C C F  G E.C.map ε ..
    interpretation εop: natural_transformation Cop.comp Cop.comp Fop_o_Gop.map Cop.map ε'.map
      using ε'.is_extensional ε'.is_natural_1 ε'.is_natural_2
      by unfold_locales auto
    interpretation εop: natural_isomorphism Cop.comp Cop.comp Fop_o_Gop.map Cop.map ε'.map
      by unfold_locales auto
    sublocale equivalence_of_categories Cop.comp Dop.comp Fop.map Gop.map η'.map ε'.map
      ..

    lemma is_equivalence_of_categories:
    shows "equivalence_of_categories Cop.comp Dop.comp Fop.map Gop.map η'.map ε'.map"
      ..

  end

  locale dual_equivalence_functor =
    G: equivalence_functor
  begin

    interpretation Cop: dual_category C ..
    interpretation Dop: dual_category D ..
    interpretation Gop: dual_functor C D G ..

    sublocale equivalence_functor Cop.comp Dop.comp Gop.map
    proof -
      obtain F η ε where F: "equivalence_of_categories C D F G η ε"
        using G.equivalence_functor_axioms equivalence_functor_def
              equivalence_functor_axioms_def
        by blast
      interpret E: equivalence_of_categories C D F G η ε
        using F by blast
      interpret dual_equivalence_of_categories C D F G η ε ..
      show "equivalence_functor Cop.comp Dop.comp Gop.map" ..
    qed

    lemma is_equivalence_functor:
    shows "equivalence_functor Cop.comp Dop.comp Gop.map"
      ..

  end

  text ‹
    An adjoint equivalence is an equivalence of categories that is also an adjunction.
›

  locale adjoint_equivalence =
    unit_counit_adjunction C D F G η ε +
    η: natural_isomorphism D D D.map "G o F" η +
    ε: natural_isomorphism C C "F o G" C.map ε
  for C :: "'c comp"     (infixr C 55)
  and D :: "'d comp"     (infixr D 55)
  and F :: "'d  'c"
  and G :: "'c  'd"
  and η :: "'d  'd"
  and ε :: "'c  'c"

  text ‹
    An adjoint equivalence is clearly an equivalence of categories.
›

  sublocale adjoint_equivalence  equivalence_of_categories ..

  context adjoint_equivalence
  begin

    text ‹
      The triangle identities for an adjunction reduce to inverse relations when
      η› and ε› are natural isomorphisms.
›

    lemma triangle_G':
    assumes "C.ide a"
    shows "D.inverse_arrows (η (G a)) (G (ε a))"
    proof
      show "D.ide (G (ε a) D η (G a))"
        using assms triangle_G GεoηG.map_simp_ide by fastforce
      thus "D.ide (η (G a) D G (ε a))"
        using assms D.section_retraction_of_iso [of "G (ε a)" "η (G a)"] by auto
    qed

    lemma triangle_F':
    assumes "D.ide b"
    shows "C.inverse_arrows (F (η b)) (ε (F b))"
    proof
     show "C.ide (ε (F b) C F (η b))"
        using assms triangle_F εFoFη.map_simp_ide by auto
      thus "C.ide (F (η b) C ε (F b))"
        using assms C.section_retraction_of_iso [of "ε (F b)" "F (η b)"] by auto
    qed

    text ‹
      An adjoint equivalence can be dualized by interchanging the two functors and inverting
      the natural isomorphisms.  This is somewhat awkward to prove, but probably useful to have
      done it once and for all.
›

    lemma dual_adjoint_equivalence:
    assumes "adjoint_equivalence C D F G η ε"
    shows "adjoint_equivalence D C G F (inverse_transformation.map C C (C.map) ε)
                                       (inverse_transformation.map D D (G o F) η)"
    proof -
      interpret adjoint_equivalence C D F G η ε using assms by auto
      interpret ε': inverse_transformation C C F o G C.map ε ..
      interpret η': inverse_transformation D D D.map G o F η ..
      interpret Gε': natural_transformation C D G G o F o G G o ε'.map
      proof -
        have "natural_transformation C D G (G o (F o G)) (G o ε'.map)"
          using G.as_nat_trans.natural_transformation_axioms ε'.natural_transformation_axioms
                horizontal_composite
          by fastforce
        thus "natural_transformation C D G (G o F o G) (G o ε'.map)"
          using o_assoc by metis
      qed
      interpret η'G: natural_transformation C D G o F o G G η'.map o G
        using η'.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms
              horizontal_composite
        by fastforce
      interpret ε'F: natural_transformation D C F F o G o F ε'.map o F
        using ε'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
              horizontal_composite
        by fastforce
      interpret Fη': natural_transformation D C F o G o F F F o η'.map
      proof -
        have "natural_transformation D C (F o (G o F)) F (F o η'.map)"
          using η'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
                horizontal_composite
          by fastforce
        thus "natural_transformation D C (F o G o F) F (F o η'.map)"
          using o_assoc by metis
      qed
      interpret Fη'oε'F: vertical_composite D C F (F o G) o F F ε'.map o F F o η'.map ..
      interpret η'GoGε': vertical_composite C D G G o F o G G G o ε'.map η'.map o G ..
      show ?thesis
      proof
        show "η'GoGε'.map = G"
        proof (intro NaturalTransformation.eqI)
          show "natural_transformation C D G G G"
            using G.as_nat_trans.natural_transformation_axioms by auto
          show "natural_transformation C D G G η'GoGε'.map"
            using η'GoGε'.natural_transformation_axioms by auto
          show "a. C.ide a  η'GoGε'.map a = G a"
          proof -
            fix a
            assume a: "C.ide a"
            show "η'GoGε'.map a = G a"
              using a η'GoGε'.map_simp_ide triangle_G' G.preserves_ide
                    η'.inverts_components ε'.inverts_components
                    D.inverse_unique G.preserves_inverse_arrows GεoηG.map_simp_ide
                    D.inverse_arrows_sym triangle_G
              by (metis o_apply)
          qed
        qed
        show "Fη'oε'F.map = F"
        proof (intro NaturalTransformation.eqI)
          show "natural_transformation D C F F F"
            using F.as_nat_trans.natural_transformation_axioms by auto
          show "natural_transformation D C F F Fη'oε'F.map"
            using Fη'oε'F.natural_transformation_axioms by auto
          show "b. D.ide b  Fη'oε'F.map b = F b"
          proof -
            fix b
            assume b: "D.ide b"
            show "Fη'oε'F.map b = F b"
              using b Fη'oε'F.map_simp_ide εFoFη.map_simp_ide triangle_F triangle_F'
                    η'.inverts_components ε'.inverts_components F.preserves_ide
                    C.inverse_unique F.preserves_inverse_arrows C.inverse_arrows_sym
              by (metis o_apply)
          qed
        qed
      qed
    qed

  end

  text ‹
    Every fully faithful and essentially surjective functor underlies an adjoint equivalence.
    To prove this without repeating things that were already proved in @{theory Category3.Adjunction},
    we first show that a fully faithful and essentially surjective functor is a left adjoint
    functor, and then we show that if the left adjoint in a unit-counit adjunction is
    fully faithful and essentially surjective, then the unit and counit are natural isomorphisms;
    hence the adjunction is in fact an adjoint equivalence.
›

  locale fully_faithful_and_essentially_surjective_functor =
    C: category C +
    D: category D +
    fully_faithful_functor C D F +
    essentially_surjective_functor C D F
    for C :: "'c comp"     (infixr C 55)
    and D :: "'d comp"     (infixr D 55)
    and F :: "'c  'd"
  begin

    notation C.in_hom      («_ : _ C _»)
    notation D.in_hom      («_ : _ D _»)

    lemma is_left_adjoint_functor:
    shows "left_adjoint_functor C D F"
    proof
      fix y
      assume y: "D.ide y"
      let ?x = "SOME x. C.ide x  (e. D.iso e  «e : F x D y»)"
      let ?e = "SOME e. D.iso e  «e : F ?x D y»"
      have "x e. D.iso e  terminal_arrow_from_functor C D F x y e"
      proof -
        have "x. D.iso ?e  terminal_arrow_from_functor C D F x y ?e"
        proof -
          have x: "C.ide ?x  (e. D.iso e  «e : F ?x D y»)"
            using y essentially_surjective
                  someI_ex [of "λx. C.ide x  (e. D.iso e  «e : F x D y»)"]
            by blast
          hence e: "D.iso ?e  «?e : F ?x D y»"
            using someI_ex [of "λe. D.iso e  «e : F ?x D y»"] by blast
          interpret arrow_from_functor C D F ?x y ?e
            using x e by (unfold_locales, simp)
          interpret terminal_arrow_from_functor C D F ?x y ?e
          proof
            fix x' f
            assume 1: "arrow_from_functor C D F x' y f"
            interpret f: arrow_from_functor C D F x' y f
              using 1 by simp
            have f: "«f: F x' D y»"
              by (meson f.arrow)
            show "∃!g. is_coext x' f g"
            proof
              let ?g = "SOME g. «g : x' C ?x»  F g = D.inv ?e D f"
              have g: "«?g : x' C ?x»  F ?g = D.inv ?e D f"
                using f e x f.arrow is_full D.comp_in_homI D.inv_in_hom
                      someI_ex [of "λg. «g : x' C ?x»  F g = D.inv ?e D f"]
                by auto
              show 1: "is_coext x' f ?g"
              proof -
                have "«?g : x' C ?x»"
                  using g by simp
                moreover have "?e D F ?g = f"
                proof -
                  have "?e D F ?g = ?e D D.inv ?e D f"
                    using g by simp
                  also have "... = (?e D D.inv ?e) D f"
                    using e f D.inv_in_hom by (metis D.comp_assoc)
                  also have "... = f"
                  proof -
                    have "?e D D.inv ?e = y"
                      using e D.comp_arr_inv D.inv_is_inverse by auto
                    thus ?thesis
                      using f D.comp_cod_arr by auto
                  qed
                  finally show ?thesis by blast
                qed
                ultimately show ?thesis
                  unfolding is_coext_def by simp
              qed
              show "g'. is_coext x' f g'  g' = ?g"
              proof -
                fix g'
                assume g': "is_coext x' f g'"
                have 2: "«g' : x' C ?x»  ?e D F g' = f" using g' is_coext_def by simp
                have 3: "«?g : x' C ?x»  ?e D F ?g = f" using 1 is_coext_def by simp
                have "F g' = F ?g"
                  using e f 2 3 D.iso_is_section D.section_is_mono D.monoE D.arrI
                  by (metis (no_types, lifting) D.arrI)
                moreover have "C.par g' ?g"
                  using 2 3 by fastforce
                ultimately show "g' = ?g"
                  using is_faithful [of g' ?g] by simp
              qed
            qed
          qed
          show ?thesis
            using e terminal_arrow_from_functor_axioms by auto
        qed
        thus ?thesis by auto
      qed
      thus "x e. terminal_arrow_from_functor C D F x y e" by blast
    qed

    lemma extends_to_adjoint_equivalence:
    shows "G η ε. adjoint_equivalence C D G F η ε"
    proof -
      interpret left_adjoint_functor C D F
        using is_left_adjoint_functor by blast
      interpret Adj: meta_adjunction D C F G φ ψ
        using induces_meta_adjunction by simp
      interpret S: replete_setcat .
      interpret Adj: adjunction D C S.comp S.setp
                       Adj.φC Adj.φD F G φ ψ Adj.η Adj.ε Adj.Φ Adj.Ψ
        using induces_adjunction by simp
      interpret equivalence_of_categories D C F G Adj.η Adj.ε
      proof
        show 1: "a. D.ide a  D.iso (Adj.ε a)"
        proof -
          fix a
          assume a: "D.ide a"
          interpret εa: terminal_arrow_from_functor C D F G a a Adj.ε a
            using a Adj.has_terminal_arrows_from_functor [of a] by blast
          have "D.retraction (Adj.ε a)"
          proof -
            obtain b φ where φ: "C.ide b  D.iso φ  «φ: F b D a»"
              using a essentially_surjective by blast
            interpret φ: arrow_from_functor C D F b a φ
              using φ by (unfold_locales, simp)
            let ?g = "εa.the_coext b φ"
            have 1: "«?g : b C G a»  Adj.ε a D F ?g = φ"
              using φ.arrow_from_functor_axioms εa.the_coext_prop [of b φ] by simp
            have "a = (Adj.ε a D F ?g) D D.inv φ"
              using a 1 φ D.comp_cod_arr Adj.ε.preserves_hom D.invert_side_of_triangle(2)
               by auto
            also have "... = Adj.ε a D F ?g D D.inv φ"
              using a 1 φ D.inv_in_hom Adj.ε.preserves_hom [of a a a] D.comp_assoc
              by blast
            finally have "f. D.ide (Adj.ε a D f)"
              using a by metis
            thus ?thesis
              unfolding D.retraction_def by blast
          qed
          moreover have "D.mono (Adj.ε a)"
          proof
            show "D.arr (Adj.ε a)"
              using a by simp
            show "f f'. D.seq (Adj.ε a) f; D.seq (Adj.ε a) f'; Adj.ε a D f = Adj.ε a D f'
                             f = f'"
            proof -
              fix f f'
              assume seq: "D.seq (Adj.ε a) f" and seq': "D.seq (Adj.ε a) f'"
              and eq: "Adj.ε a D f = Adj.ε a D f'"
              have f: "«f : D.dom f D F (G a)»"
                using a seq Adj.ε.preserves_hom [of a a a] by fastforce
              have f': "«f' : D.dom f' D F (G a)»"
                using a seq' Adj.ε.preserves_hom [of a a a] by fastforce
              have par: "D.par f f'"
                using f f' seq eq D.dom_comp [of "Adj.ε a" f] by force
              obtain b' φ where φ: "C.ide b'  D.iso φ  «φ: F b' D D.dom f»"
                using par essentially_surjective D.ide_dom [of f] by blast
              have 1: "Adj.ε a D f D φ = Adj.ε a D f' D φ"
                using eq φ par D.comp_assoc by metis
              obtain g where g: "«g : b' C G a»  F g = f D φ"
                using a f φ is_full [of "G a" b' "f D φ"] by auto
              obtain g' where g': "«g' : b' C G a»  F g' = f' D φ"
                using a f' par φ is_full [of "G a" b' "f' D φ"] by auto
              interpret: arrow_from_functor C D F b' a Adj.ε a D f D φ
                using a φ f Adj.ε.preserves_hom
                by (unfold_locales, fastforce)
              interpret f'φ: arrow_from_functor C D F b' a Adj.ε a D f' D φ
                using a φ f' par Adj.ε.preserves_hom
                by (unfold_locales, fastforce)
              have "εa.is_coext b' (Adj.ε a D f D φ) g"
                unfolding εa.is_coext_def using g 1 by auto
              moreover have "εa.is_coext b' (Adj.ε a D f' D φ) g'"
                unfolding εa.is_coext_def using g' 1 by auto
              ultimately have "g = g'"
                using 1 fφ.arrow_from_functor_axioms f'φ.arrow_from_functor_axioms
                      εa.the_coext_unique εa.the_coext_unique [of b' "Adj.ε a D f' D φ" g']
                by auto
              hence "f D φ = f' D φ"
                using g g' is_faithful by argo
              thus "f = f'"
                using φ f f' par D.iso_is_retraction D.retraction_is_epi D.epiE [of φ f f']
                by auto
            qed
          qed
          ultimately show "D.iso (Adj.ε a)"
            using D.iso_iff_mono_and_retraction by simp
        qed
        interpret ε: natural_isomorphism D D F o G D.map Adj.ε
          using 1 by (unfold_locales, auto)
        interpret εF: natural_isomorphism C D F o G o F F Adj.ε o F
          using ε.components_are_iso by (unfold_locales, simp)
        show "a. C.ide a  C.iso (Adj.η a)"
        proof -
          fix a
          assume a: "C.ide a"
          have "D.inverse_arrows ((Adj.ε o F) a) ((F o Adj.η) a)"
            using a ε.components_are_iso Adj.ηε.triangle_F Adj.εFoFη.map_simp_ide
                  D.section_retraction_of_iso
            by simp
          hence "D.iso ((F o Adj.η) a)"
            by blast
          thus "C.iso (Adj.η a)"
            using a reflects_iso [of "Adj.η a"] by fastforce
        qed
      qed
      (*
       * Uggh, I should have started with "right_adjoint_functor D C G" so that the
       * following would come out right.  Instead, another step is needed to dualize.
       * TODO: Maybe re-work this later.
       *)
      interpret adjoint_equivalence D C F G Adj.η Adj.ε ..
      interpret ε': inverse_transformation D D F o G D.map Adj.ε ..
      interpret η': inverse_transformation C C C.map G o F Adj.η ..
      interpret E: adjoint_equivalence C D G F ε'.map η'.map
        using adjoint_equivalence_axioms dual_adjoint_equivalence by blast
      show ?thesis
        using E.adjoint_equivalence_axioms by auto
    qed

    lemma is_right_adjoint_functor:
    shows "right_adjoint_functor C D F"
    proof -
      obtain G η ε where E: "adjoint_equivalence C D G F η ε"
        using extends_to_adjoint_equivalence by auto
      interpret E: adjoint_equivalence C D G F η ε
        using E by simp
      interpret Adj: meta_adjunction C D G F E.φ E.ψ
        using E.induces_meta_adjunction by simp
      show ?thesis
        using Adj.has_right_adjoint_functor by simp
    qed

    lemma is_equivalence_functor:
    shows "equivalence_functor C D F"
    proof
      obtain G η ε where E: "adjoint_equivalence C D G F η ε"
        using extends_to_adjoint_equivalence by auto
      interpret E: adjoint_equivalence C D G F η ε
        using E by simp
      have "equivalence_of_categories C D G F η ε" ..
      thus "G η ε. equivalence_of_categories C D G F η ε" by blast
    qed

    sublocale equivalence_functor C D F
      using is_equivalence_functor by blast

  end

  context equivalence_of_categories
  begin

    text ‹
      The following development shows that an equivalence of categories can
      be refined to an adjoint equivalence by replacing just the counit.
    ›

    abbreviation ε'
    where "ε' a  ε a C F (D.inv (η (G a))) C C.inv (ε (F (G a)))"

    interpretation ε': transformation_by_components C C F  G C.map ε'
    proof
      show "a. C.ide a  «ε' a : (F  G) a C C.map a»"
        using η.components_are_iso ε.components_are_iso by simp
      fix f
      assume f: "C.arr f"
      show "ε' (C.cod f) C (F  G) f = C.map f C ε' (C.dom f)"
      proof -
        have "ε' (C.cod f) C (F  G) f =
              ε (C.cod f) C F (D.inv (η (G (C.cod f)))) C C.inv (ε (F (G (C.cod f)))) C F (G f)"
          using f C.comp_assoc by simp
        also have "... = ε (C.cod f) C (F (D.inv (η (G (C.cod f)))) C
                           F (G (F (G f)))) C C.inv (ε (F (G (C.dom f))))"
          using f ε.inv_naturality [of "F (G f)"] C.comp_assoc by simp
        also have "... = (ε (C.cod f) C F (G f)) C F (D.inv (η (G (C.dom f)))) C
                           C.inv (ε (F (G (C.dom f))))"
        proof -
          have "F (D.inv (η (G (C.cod f)))) C F (G (F (G f))) =
                F (G f) C F (D.inv (η (G (C.dom f))))"
          proof -
            have "F (D.inv (η (G (C.cod f)))) C F (G (F (G f))) =
                  F (D.inv (η (G (C.cod f))) D G (F (G f)))"
              using f by simp
            also have "... = F (G f D D.inv (η (G (C.dom f))))"
              using f η.inv_naturality [of "G f"] by simp
            also have "... = F (G f) C F (D.inv (η (G (C.dom f))))"
              using f by simp
            finally show ?thesis by blast
          qed
          thus ?thesis
            using C.comp_assoc by simp
        qed
        also have "... = C.map f C ε (C.dom f) C F (D.inv (η (G (C.dom f)))) C
                           C.inv (ε (F (G (C.dom f))))"
          using f ε.naturality C.comp_assoc by simp
        finally show ?thesis by blast
      qed
    qed

    interpretation ε': natural_isomorphism C C F  G C.map ε'.map
    proof
      show "a. C.ide a  C.iso (ε'.map a)"
        unfolding ε'.map_def
        using η.components_are_iso ε.components_are_iso
        apply simp
        by (intro C.isos_compose) auto
    qed

    lemma Fη_inverse:
    assumes "D.ide b"
    shows "F (η (G (F b))) = F (G (F (η b)))"
    and "F (η b) C ε (F b) = ε (F (G (F b))) C F (η (G (F b)))"
    and "C.inverse_arrows (F (η b)) (ε' (F b))"
    and "F (η b) = C.inv (ε' (F b))"
    and "C.inv (F (η b)) = ε' (F b)"
    proof -
      let ?ε' = "λa. ε a C F (D.inv (η (G a))) C C.inv (ε (F (G a)))"
      show 1: "F (η (G (F b))) = F (G (F (η b)))"
      proof -
        have "F (η (G (F b))) C F (η b) = F (G (F (η b))) C F (η b)"
        proof -
          have "F (η (G (F b))) C F (η b) = F (η (G (F b)) D η b)"
            using assms by simp
          also have "... = F (G (F (η b)) D η b)"
            using assms η.naturality [of "η b"] by simp
          also have "... = F (G (F (η b))) C F (η b)"
            using assms by simp
          finally show ?thesis by blast
        qed
        thus ?thesis
          using assms η.components_are_iso C.iso_cancel_right by simp
      qed
      show "F (η b) C ε (F b) = ε (F (G (F b))) C F (η (G (F b)))"
        using assms 1 ε.naturality [of "F (η b)"] by simp
      show 2: "C.inverse_arrows (F (η b)) (?ε' (F b))"
      proof
        show 3: "C.ide (?ε' (F b) C F (η b))"
        proof -
          have "?ε' (F b) C F (η b) =
                ε (F b) C (F (D.inv (η (G (F b)))) C C.inv (ε (F (G (F b))))) C F (η b)"
            using C.comp_assoc by simp
          also have "... = ε (F b) C (F (D.inv (η (G (F b)))) C F (G (F (η b)))) C C.inv (ε (F b))"
            using assms ε.naturality [of "F (η b)"] ε.components_are_iso C.comp_assoc
                  C.invert_opposite_sides_of_square
                    [of "ε (F (G (F b)))" "F (G (F (η b)))" "F (η b)" "ε (F b)"]
            by simp
          also have "... = ε (F b) C C.inv (ε (F b))"
          proof -
            have "F (D.inv (η (G (F b)))) C F (G (F (η b))) = F (G (F b))"
              using assms 1 D.comp_inv_arr' η.components_are_iso
              by (metis D.ideD(1) D.ideD(2) F.preserves_comp
                  F.preserves_ide G.preserves_ide η.preserves_dom D.map_simp)
            moreover have "F (G (F b)) C C.inv (ε (F b)) = C.inv (ε (F b))"
              using assms D.comp_cod_arr ε.components_are_iso C.inv_in_hom [of "ε (F b)"]
              by (metis C.comp_ide_arr C_arr_expansion(1) D.ide_char F.preserves_arr
                  F.preserves_dom F.preserves_ide G.preserves_ide C.seqE)
            ultimately show ?thesis by simp
          qed
          also have "... = F b"
            using assms ε.components_are_iso C.comp_arr_inv' by simp
          finally have "(ε (F b) C F (D.inv (η (G (F b)))) C C.inv (ε (F (G (F b))))) C F (η b) = F b"
            by blast
          thus ?thesis
            using assms by simp
        qed
        show "C.ide (F (η b) C ?ε' (F b))"
        proof -
          have "(F (η b) C ?ε' (F b)) C F (η b) = F (G (F b)) C F (η b)"
          proof -
            have "(F (η b) C ?ε' (F b)) C F (η b) =
                  F (η b) C (ε (F b) C F (D.inv (η (G (F b)))) C C.inv (ε (F (G (F b))))) C F (η b)"
              using C.comp_assoc by simp
            also have "... = F (η b)"
              using assms 3
                    C.comp_arr_dom
                      [of "F (η b)" "(ε (F b) C F (D.inv (η (G (F b)))) C
                                       C.inv (ε (F (G (F b))))) C F (η b)"]
              by auto
            also have "... = F (G (F b)) C F (η b)"
              using assms C.comp_cod_arr by simp
            finally show ?thesis by blast
          qed
          hence "F (η b) C ?ε' (F b) = F (G (F b))"
            using assms C.iso_cancel_right by simp
          thus ?thesis
            using assms by simp
        qed
      qed
      show "C.inv (F (η b)) = ?ε' (F b)"
        using assms 2 C.inverse_unique by simp
      show "F (η b) = C.inv (?ε' (F b))"
      proof -
        have "C.inverse_arrows (?ε' (F b)) (F (η b))"
          using assms 2 by auto
        thus ?thesis
          using assms C.inverse_unique by simp
      qed
    qed

    interpretation FoGoF: composite_functor D C C F F o G ..
    interpretation GoFoG: composite_functor C D D G G o F ..

    interpretation natural_transformation D C F FoGoF.map F  η
    proof -
      have "F  D.map = F"
        using hcomp_ide_dom F.as_nat_trans.natural_transformation_axioms by blast
      moreover have "F o (G o F) = FoGoF.map"
        by auto
      ultimately show "natural_transformation D C F FoGoF.map (F  η)"
        using η.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
              horizontal_composite [of D D D.map "G o F" η C F F F]
        by simp
    qed

    interpretation natural_transformation C D G GoFoG.map η  G
      using η.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms
            horizontal_composite [of C D G G G ]
      by fastforce

    interpretation natural_transformation D C FoGoF.map F ε'.map  F
      using ε'.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
            horizontal_composite [of D C F F F]
      by fastforce

    interpretation natural_transformation C D GoFoG.map G G  ε'.map
    proof -
      have "G o C.map = G"
        using hcomp_ide_dom G.as_nat_trans.natural_transformation_axioms by blast
      moreover have "G o (F o G) = GoFoG.map"
        by auto
      ultimately show "natural_transformation C D GoFoG.map G (G  ε'.map)"
        using G.as_nat_trans.natural_transformation_axioms ε'.natural_transformation_axioms
              horizontal_composite [of C C "F o G" C.map ε'.map D G G G]
        by simp
    qed

    interpretation ε'F_Fη: vertical_composite D C F FoGoF.map F F  η ε'.map  F ..
    interpretation Gε'_ηG: vertical_composite C D G GoFoG.map G η o G G o ε'.map ..

    interpretation ηε': unit_counit_adjunction C D F G η ε'.map
    proof
      show 1: "ε'F_Fη.map = F"
      proof
        fix g
        show "ε'F_Fη.map g = F g"
        proof (cases "D.arr g")
          show "¬ D.arr g  ε'F_Fη.map g = F g"
            using ε'F_Fη.is_extensional F.is_extensional by simp
          assume g: "D.arr g"
          have "ε'F_Fη.map g = ε' (F (D.cod g)) C F (η g)"
            using g ε'F_Fη.map_def by simp
          also have "... = ε' (F (D.cod g)) C F (η (D.cod g) D g)"
            using g η.is_natural_2 by simp
          also have "... = (ε' (F (D.cod g)) C F (η (D.cod g))) C F g"
            using g C.comp_assoc by simp
          also have "... = F (D.cod g) C F g"
            using g Fη_inverse(3) [of "D.cod g"] by fastforce
          also have "... = F g"
            using g C.comp_cod_arr by simp
          finally show "ε'F_Fη.map g = F g" by blast
        qed
      qed
      show "Gε'_ηG.map = G"
      proof
        fix f
        show "Gε'_ηG.map f = G f"
        proof (cases "C.arr f")
          show "¬ C.arr f  Gε'_ηG.map f = G f"
            using Gε'_ηG.is_extensional G.is_extensional by simp
          assume f: "C.arr f"
          have "F (Gε'_ηG.map f) = F (G (ε' (C.cod f)) D η (G f))"
            using f Gε'_ηG.map_def D.comp_assoc by simp
          also have "... = F (G (ε' (C.cod f)) D η (G (C.cod f)) D G f)"
            using f η.is_natural_2 [of "G f"] by simp
          also have "... = F (G (ε' (C.cod f))) C F (η (G (C.cod f))) C F (G f)"
            using f by simp
          also have "... = (F (G (ε' (C.cod f))) C C.inv (ε' (F (G (C.cod f))))) C F (G f)"
            using f Fη_inverse(4) C.comp_assoc by simp
          also have "... = (C.inv (ε' (C.cod f)) C ε' (C.cod f)) C F (G f)"
            using f ε'.inv_naturality [of "ε' (C.cod f)"] by simp
          also have "... = F (G (C.cod f)) C F (G f)"
            using f C.comp_inv_arr' [of "ε' (C.cod f)"] ε'.components_are_iso by simp
          also have "... = F (G f)"
            using f C.comp_cod_arr by simp
          finally have "F (Gε'_ηG.map f) = F (G f)" by blast
          moreover have "D.par (Gε'_ηG.map f) (G f)"
            using f by simp
          ultimately show "Gε'_ηG.map f = G f"
            using f F_is_faithful
            by (simp add: faithful_functor_axioms_def faithful_functor_def)
        qed
      qed
    qed

    interpretation ηε': adjoint_equivalence C D F G η ε'.map ..

    lemma refines_to_adjoint_equivalence:
    shows "adjoint_equivalence C D F G η ε'.map"
      ..

  end

end