# 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
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

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

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.
›

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_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;
›

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 _»")

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

shows "∃G η ε. adjoint_equivalence C D G F η ε"
proof -
interpret S: replete_setcat .
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
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
proof
using a by simp
⟹ f = f'"
proof -
fix f f'
assume seq: "D.seq (Adj.ε a) f" and seq': "D.seq (Adj.ε a) 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 fφ: arrow_from_functor C D F b' a ‹Adj.ε a ⋅⇩D f ⋅⇩D φ›
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
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"
D.section_retraction_of_iso
by simp
hence "D.iso ((F o Adj.η) a)"
by blast
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 ε': 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
show ?thesis
qed

proof -
obtain G η ε where E: "adjoint_equivalence C D G F η ε"
interpret E: adjoint_equivalence C D G F η ε
using E by simp
show ?thesis
qed

lemma is_equivalence_functor:
shows "equivalence_functor C D F"
proof
obtain G η ε where E: "adjoint_equivalence C D G F η ε"
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
qed
qed
qed

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