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

imports Yoneda
begin

text‹
This theory defines the notions of adjoint functor and adjunction in various
ways and establishes their equivalence.
The notions left adjoint functor'' and right adjoint functor'' are defined
in terms of universal arrows.
Meta-adjunctions'' are defined in terms of natural bijections between hom-sets,
where the notion of naturality is axiomatized directly.
Hom-adjunctions'' formalize the notion of adjunction in terms of natural
isomorphisms of hom-functors.
Unit-counit adjunctions'' define adjunctions in terms of functors equipped
with unit and counit natural transformations that satisfy the usual
triangle identities.''
The ‹adjunction› locale is defined as the grand unification of all the
definitions, and includes formulas that connect the data from each of them.
It is shown that each of the definitions induces an interpretation of the
‹adjunction› locale, so that all the definitions are essentially equivalent.
Finally, it is shown that right adjoint functors are unique up to natural
isomorphism.

The reference \<^cite>‹"Wikipedia-Adjoint-Functors"› was useful in constructing this theory.
›

text‹
@{term e} is an arrow from @{term "F x"} to @{term y}.''
›

locale arrow_from_functor =
C: category C +
D: category D +
F: "functor" D C F
for D :: "'d comp"     (infixr "⋅⇩D" 55)
and C :: "'c comp"     (infixr "⋅⇩C" 55)
and F :: "'d ⇒ 'c"
and x :: 'd
and y :: 'c
and e :: 'c +
assumes arrow: "D.ide x ∧ C.in_hom e (F x) y"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

text‹
@{term g} is a @{term[source=true] D}-coextension of @{term f} along @{term e}.''
›

definition is_coext :: "'d ⇒ 'c ⇒ 'd ⇒ bool"
where "is_coext x' f g ≡ «g : x' →⇩D x» ∧ f = e ⋅⇩C F g"

end

text‹
@{term e} is a terminal arrow from @{term "F x"} to @{term y}.''
›

locale terminal_arrow_from_functor =
arrow_from_functor D C F x y e
for D :: "'d comp"     (infixr "⋅⇩D" 55)
and C :: "'c comp"     (infixr "⋅⇩C" 55)
and F :: "'d ⇒ 'c"
and x :: 'd
and y :: 'c
and e :: 'c +
assumes is_terminal: "arrow_from_functor D C F x' y f ⟹ (∃!g. is_coext x' f g)"
begin

definition the_coext :: "'d ⇒ 'c ⇒ 'd"
where "the_coext x' f = (THE g. is_coext x' f g)"

lemma the_coext_prop:
assumes "arrow_from_functor D C F x' y f"
shows "«the_coext x' f : x' →⇩D x»" and "f = e ⋅⇩C F (the_coext x' f)"
by (metis assms is_coext_def is_terminal the_coext_def the_equality)+

lemma the_coext_unique:
assumes "arrow_from_functor D C F x' y f" and "is_coext x' f g"
shows "g = the_coext x' f"
using assms is_terminal the_coext_def the_equality by metis

end

text‹
A left adjoint functor is a functor ‹F: D → C›
that enjoys the following universal coextension property: for each object
@{term y} of @{term C} there exists an object @{term x} of @{term D} and an
arrow ‹e ∈ C.hom (F x) y› such that for any arrow
‹f ∈ C.hom (F x') y› there exists a unique ‹g ∈ D.hom x' x›
such that @{term "f = C e (F g)"}.
›

C: category C +
D: category D +
"functor" D C F
for D :: "'d comp"     (infixr "⋅⇩D" 55)
and C :: "'c comp"     (infixr "⋅⇩C" 55)
and F :: "'d ⇒ 'c" +
assumes ex_terminal_arrow: "C.ide y ⟹ (∃x e. terminal_arrow_from_functor D C F x y e)"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

end

text‹
@{term e} is an arrow from @{term x} to @{term "G y"}.''
›

locale arrow_to_functor =
C: category C +
D: category D +
G: "functor" C D G
for C :: "'c comp"     (infixr "⋅⇩C" 55)
and D :: "'d comp"     (infixr "⋅⇩D" 55)
and G :: "'c ⇒ 'd"
and x :: 'd
and y :: 'c
and e :: 'd +
assumes arrow: "C.ide y ∧ D.in_hom e x (G y)"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

text‹
@{term f} is a @{term[source=true] C}-extension of @{term g} along @{term e}.''
›

definition is_ext :: "'c ⇒ 'd ⇒ 'c ⇒ bool"
where "is_ext y' g f ≡ «f : y →⇩C y'» ∧ g = G f ⋅⇩D e"

end

text‹
@{term e} is an initial arrow from @{term x} to @{term "G y"}.''
›

locale initial_arrow_to_functor =
arrow_to_functor C D G x y e
for C :: "'c comp"     (infixr "⋅⇩C" 55)
and D :: "'d comp"     (infixr "⋅⇩D" 55)
and G :: "'c ⇒ 'd"
and x :: 'd
and y :: 'c
and e :: 'd +
assumes is_initial: "arrow_to_functor C D G x y' g ⟹ (∃!f. is_ext y' g f)"
begin

definition the_ext :: "'c ⇒ 'd ⇒ 'c"
where "the_ext y' g = (THE f. is_ext y' g f)"

lemma the_ext_prop:
assumes "arrow_to_functor C D G x y' g"
shows "«the_ext y' g : y →⇩C y'»" and "g = G (the_ext y' g) ⋅⇩D e"
by (metis assms is_initial is_ext_def the_equality the_ext_def)+

lemma the_ext_unique:
assumes "arrow_to_functor C D G x y' g" and "is_ext y' g f"
shows "f = the_ext y' g"
using assms is_initial the_ext_def the_equality by metis

end

text‹
A right adjoint functor is a functor ‹G: C → D›
that enjoys the following universal extension property:
for each object @{term x} of @{term D} there exists an object @{term y} of @{term C}
and an arrow ‹e ∈ D.hom x (G y)› such that for any arrow
‹g ∈ D.hom x (G y')› there exists a unique ‹f ∈ C.hom y y'›
such that @{term "h = D e (G f)"}.
›

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 ex_initial_arrow: "D.ide x ⟹ (∃y e. initial_arrow_to_functor C D G x y e)"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

end

text‹
A meta-adjunction'' consists of a functor ‹F: D → C›,
a functor ‹G: C → D›, and for each object @{term x}
of @{term C} and @{term y} of @{term D} a bijection between
‹C.hom (F y) x› to ‹D.hom y (G x)› which is natural in @{term x}
and @{term y}.  The naturality is easy to express at the meta-level without having
to resort to the formal baggage of set category,'' hom-functor,''
and natural isomorphism,'' hence the name.
›

C: category C +
D: category D +
F: "functor" D C F +
G: "functor" C D G
for C :: "'c comp"     (infixr "⋅⇩C" 55)
and D :: "'d comp"     (infixr "⋅⇩D" 55)
and F :: "'d ⇒ 'c"
and G :: "'c ⇒ 'd"
and φ :: "'d ⇒ 'c ⇒ 'd"
and ψ :: "'c ⇒ 'd ⇒ 'c" +
assumes φ_in_hom: "⟦ D.ide y; C.in_hom f (F y) x ⟧ ⟹ D.in_hom (φ y f) y (G x)"
and ψ_in_hom: "⟦ C.ide x; D.in_hom g y (G x) ⟧ ⟹ C.in_hom (ψ x g) (F y) x"
and ψ_φ: "⟦ D.ide y; C.in_hom f (F y) x ⟧ ⟹ ψ x (φ y f) = f"
and φ_ψ: "⟦ C.ide x; D.in_hom g y (G x) ⟧ ⟹ φ y (ψ x g) = g"
and φ_naturality: "⟦ C.in_hom f x x'; D.in_hom g y' y; C.in_hom h (F y) x ⟧ ⟹
φ y' (f ⋅⇩C h ⋅⇩C F g) = G f ⋅⇩D φ y h ⋅⇩D g"
begin

notation C.in_hom ("«_ : _ →⇩C _»")
notation D.in_hom ("«_ : _ →⇩D _»")

text‹
The naturality of @{term ψ} is a consequence of the naturality of @{term φ}
and the other assumptions.
›

lemma ψ_naturality:
assumes f: "«f : x →⇩C x'»" and g: "«g : y' →⇩D y»" and h: "«h : y →⇩D G x»"
shows "f ⋅⇩C ψ x h ⋅⇩C F g = ψ x' (G f ⋅⇩D h ⋅⇩D g)"
using f g h φ_naturality ψ_in_hom C.ide_dom D.ide_dom D.in_homE φ_ψ ψ_φ
by (metis C.comp_in_homI' F.preserves_hom C.in_homE D.in_homE)

lemma respects_natural_isomorphism:
assumes "natural_isomorphism D C F' F τ" and "natural_isomorphism C D G G' μ"
shows "meta_adjunction C D F' G'
(λy f. μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C inverse_transformation.map D C F τ y))
(λx g. ψ x ((inverse_transformation.map C D G' μ x) ⋅⇩D g) ⋅⇩C τ (D.dom g))"
proof -
interpret τ: natural_isomorphism D C F' F τ
using assms(1) by simp
interpret τ': inverse_transformation D C F' F τ
..
interpret μ: natural_isomorphism C D G G' μ
using assms(2) by simp
interpret μ': inverse_transformation C D G G' μ
..
let ?φ' = "λy f. μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y)"
let ?ψ' = "λx g. ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g)"
show "meta_adjunction C D F' G' ?φ' ?ψ'"
proof
show "⋀y f x. ⟦D.ide y; «f : F' y →⇩C x»⟧
⟹ «μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y) : y →⇩D G' x»"
proof -
fix x y f
assume y: "D.ide y" and f: "«f : F' y →⇩C x»"
show "«μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y) : y →⇩D G' x»"
proof (intro D.comp_in_homI)
show "«μ (C.cod f) : G x →⇩D G' x»"
using f by fastforce
show "«φ y (f ⋅⇩C τ'.map y) : y →⇩D G x»"
using f y φ_in_hom by auto
qed
qed
show "⋀x g y. ⟦C.ide x; «g : y →⇩D G' x»⟧
⟹ «ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g) : F' y →⇩C x»"
proof -
fix x y g
assume x: "C.ide x" and g: "«g : y →⇩D G' x»"
show "«ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g) : F' y →⇩C x»"
proof (intro C.comp_in_homI)
show "«τ (D.dom g) : F' y →⇩C F y»"
using g by fastforce
show "«ψ x (μ'.map x ⋅⇩D g) : F y →⇩C x»"
using x g ψ_in_hom by auto
qed
qed
show "⋀y f x. ⟦D.ide y; «f : F' y →⇩C x»⟧
⟹ ψ x (μ'.map x ⋅⇩D μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y)) ⋅⇩C
τ (D.dom (μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y))) =
f"
proof -
fix x y f
assume y: "D.ide y" and f: "«f : F' y →⇩C x»"
have 1: "«φ y (f ⋅⇩C τ'.map y) : y →⇩D G x»"
using f y φ_in_hom by auto
show "ψ x (μ'.map x ⋅⇩D μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y)) ⋅⇩C
τ (D.dom (μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y))) =
f"
proof -
have "ψ x (μ'.map x ⋅⇩D μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y)) ⋅⇩C
τ (D.dom (μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y))) =
ψ x ((μ'.map x ⋅⇩D μ (C.cod f)) ⋅⇩D φ y (f ⋅⇩C τ'.map y)) ⋅⇩C
τ (D.dom (μ (C.cod f) ⋅⇩D φ y (f ⋅⇩C τ'.map y)))"
using D.comp_assoc by simp
also have "... = ψ x (φ y (f ⋅⇩C τ'.map y)) ⋅⇩C τ y"
by (metis "1" C.arr_cod C.dom_cod C.ide_cod C.in_homE D.comp_ide_arr D.dom_comp
D.ide_compE D.in_homE D.inverse_arrowsE μ'.inverts_components μ.preserves_dom
also have "... = f"
using f y ψ_φ C.comp_assoc τ'.inverts_components [of y] C.comp_arr_dom
by fastforce
finally show ?thesis by blast
qed
qed
show "⋀x g y. ⟦C.ide x; «g : y →⇩D G' x»⟧
⟹ μ (C.cod (ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g))) ⋅⇩D
φ y ((ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g)) ⋅⇩C τ'.map y) =
g"
proof -
fix x y g
assume x: "C.ide x" and g: "«g : y →⇩D G' x»"
have 1: "«ψ x (μ'.map x ⋅⇩D g) : F y →⇩C x»"
using x g ψ_in_hom by auto
show "μ (C.cod (ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g))) ⋅⇩D
φ y ((ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g)) ⋅⇩C τ'.map y) =
g"
proof -
have "μ (C.cod (ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g))) ⋅⇩D
φ y ((ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g)) ⋅⇩C τ'.map y) =
μ (C.cod (ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g))) ⋅⇩D
φ y (ψ x (μ'.map x ⋅⇩D g) ⋅⇩C τ (D.dom g) ⋅⇩C τ'.map y)"
using C.comp_assoc by simp
also have "... = μ x ⋅⇩D φ y (ψ x (μ'.map x ⋅⇩D g))"
using 1 C.comp_arr_dom C.comp_arr_inv' g by fastforce
also have "... = (μ x ⋅⇩D μ'.map x) ⋅⇩D g"
using x g φ_ψ D.comp_assoc by auto
also have "... = g"
using x g μ'.inverts_components [of x] D.comp_cod_arr by fastforce
finally show ?thesis by blast
qed
qed
show "⋀f x x' g y' y h. ⟦«f : x →⇩C x'»; «g : y' →⇩D y»; «h : F' y →⇩C x»⟧
⟹ μ (C.cod (f ⋅⇩C h ⋅⇩C F' g)) ⋅⇩D φ y' ((f ⋅⇩C h ⋅⇩C F' g) ⋅⇩C τ'.map y') =
G' f ⋅⇩D (μ (C.cod h) ⋅⇩D φ y (h ⋅⇩C τ'.map y)) ⋅⇩D g"
proof -
fix x y x' y' f g h
assume f: "«f : x →⇩C x'»" and g: "«g : y' →⇩D y»" and h: "«h : F' y →⇩C x»"
show "μ (C.cod (f ⋅⇩C h ⋅⇩C F' g)) ⋅⇩D φ y' ((f ⋅⇩C h ⋅⇩C F' g) ⋅⇩C τ'.map y') =
G' f ⋅⇩D (μ (C.cod h) ⋅⇩D φ y (h ⋅⇩C τ'.map y)) ⋅⇩D g"
proof -
have "μ (C.cod (f ⋅⇩C h ⋅⇩C F' g)) ⋅⇩D φ y' ((f ⋅⇩C h ⋅⇩C F' g) ⋅⇩C τ'.map y') =
μ x' ⋅⇩D φ y' ((f ⋅⇩C h ⋅⇩C F' g) ⋅⇩C τ'.map y')"
using f g h by fastforce
also have "... = μ x' ⋅⇩D φ y' (f ⋅⇩C (h ⋅⇩C τ'.map y) ⋅⇩C F g)"
using g τ'.naturality C.comp_assoc by auto
also have "... = (μ x' ⋅⇩D G f) ⋅⇩D φ y (h ⋅⇩C τ'.map y) ⋅⇩D g"
using f g h φ_naturality [of f x x' g y' y "h ⋅⇩C τ'.map y"] D.comp_assoc
by fastforce
also have "... = (G' f ⋅⇩D μ x) ⋅⇩D φ y (h ⋅⇩C τ'.map y) ⋅⇩D g"
using f μ.naturality by auto
also have "... = G' f ⋅⇩D (μ (C.cod h) ⋅⇩D φ y (h ⋅⇩C τ'.map y)) ⋅⇩D g"
using h D.comp_assoc by auto
finally show ?thesis by blast
qed
qed
qed
qed

end

text‹
The bijection between hom-sets that defines an adjunction can be represented
formally as a natural isomorphism of hom-functors.  However, stating the definition
this way is more complex than was the case for ‹meta_adjunction›.
One reason is that we need to have a set category'' that is suitable as
a target category for the hom-functors, and since the arrows of the categories
@{term C} and @{term D} will in general have distinct types, we need a set category
that simultaneously embeds both.  Another reason is that we simply have to formally
construct the various categories and functors required to express the definition.

This is a good place to point out that I have often included more sublocales
in a locale than are strictly required.  The main reason for this is the fact that
the locale system in Isabelle only gives one name to each entity introduced by
a locale: the name that it has in the first locale in which it occurs.
This means that entities that make their first appearance deeply nested in sublocales
will have to be referred to by long qualified names that can be difficult to
understand, or even to discover.  To counteract this, I have typically introduced
sublocales before the superlocales that contain them to ensure that the entities
in the sublocales can be referred to by short meaningful (and predictable) names.
In my opinion, though, it would be better if the locale system would make entities
that occur in multiple locales accessible by \emph{all} possible qualified names,
so that the most perspicuous name could be used in any particular context.
›

C: category C +
D: category D +
S: set_category S setp +
Cop: dual_category C +
Dop: dual_category D +
CopxC: product_category Cop.comp C +
DopxD: product_category Dop.comp D +
DopxC: product_category Dop.comp C +
F: "functor" D C F +
G: "functor" C D G +
HomC: hom_functor C S setp φC +
HomD: hom_functor D S setp φD +
Fop: dual_functor Dop.comp Cop.comp F +
FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map +
DopxG: product_functor Dop.comp C Dop.comp D Dop.map G +
Hom_FopxC: composite_functor DopxC.comp CopxC.comp S FopxC.map HomC.map +
Hom_DopxG: composite_functor DopxC.comp DopxD.comp S DopxG.map HomD.map +
Hom_FopxC: set_valued_functor DopxC.comp S setp Hom_FopxC.map +
Hom_DopxG: set_valued_functor DopxC.comp S setp Hom_DopxG.map +
Φ: set_valued_transformation DopxC.comp S setp Hom_FopxC.map Hom_DopxG.map Φ +
Ψ: set_valued_transformation DopxC.comp S setp Hom_DopxG.map Hom_FopxC.map Ψ +
ΦΨ: inverse_transformations DopxC.comp S Hom_FopxC.map Hom_DopxG.map Φ Ψ
for C :: "'c comp"     (infixr "⋅⇩C" 55)
and D :: "'d comp"     (infixr "⋅⇩D" 55)
and S :: "'s comp"     (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φC :: "'c * 'c ⇒ 'c ⇒ 's"
and φD :: "'d * 'd ⇒ 'd ⇒ 's"
and F :: "'d ⇒ 'c"
and G :: "'c ⇒ 'd"
and Φ :: "'d * 'c ⇒ 's"
and Ψ :: "'d * 'c ⇒ 's"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

abbreviation ψC :: "'c * 'c ⇒ 's ⇒ 'c"
where "ψC ≡ HomC.ψ"

abbreviation ψD :: "'d * 'd ⇒ 's ⇒ 'd"
where "ψD ≡ HomD.ψ"

end

text‹
Expressed in unit/counit terms, an adjunction consists of functors
‹F: D → C› and ‹G: C → D›, equipped with natural transformations
‹η: 1 → GF› and ‹ε: FG → 1› satisfying certain triangle identities''.
›

C: category C +
D: category D +
F: "functor" D C F +
G: "functor" C D G +
GF: composite_functor D C D F G +
FG: composite_functor C D C G F +
FGF: composite_functor D C C F ‹F o G› +
GFG: composite_functor C D D G ‹G o F› +
η: natural_transformation D D D.map ‹G o F› η +
ε: natural_transformation C C ‹F o G› C.map ε +
Fη: natural_transformation D C F ‹F o G o F› ‹F o η› +
ηG: natural_transformation C D G ‹G o F o G› ‹η o G› +
εF: natural_transformation D C ‹F o G o F› F ‹ε o F› +
Gε: natural_transformation C D ‹G o F o G› G ‹G o ε› +
εFoFη: vertical_composite D C F ‹F o G o F› F ‹F o η› ‹ε o F› +
GεoηG: vertical_composite C D G ‹G o F o G› G ‹η o G› ‹G o ε›
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" +
assumes triangle_F: "εFoFη.map = F"
and triangle_G: "GεoηG.map = G"
begin

notation C.in_hom      ("«_ : _ →⇩C _»")
notation D.in_hom      ("«_ : _ →⇩D _»")

end

lemma unit_determines_counit:
assumes "unit_counit_adjunction C D F G η ε"
and "unit_counit_adjunction C D F G η ε'"
shows "ε = ε'"
proof -
(* IDEA:  ε' = ε'FG o (FGε o FηG) = ε'ε o FηG = εFG o (ε'FG o FηG) = ε *)
interpret Adj: unit_counit_adjunction C D F G η ε using assms(1) by auto
interpret Adj': unit_counit_adjunction C D F G η ε' using assms(2) by auto
interpret FGFG: composite_functor C D C G ‹F o G o F› ..
interpret FGε: natural_transformation C C ‹(F o G) o (F o G)› ‹F o G› ‹(F o G) o ε›
horizontal_composite
by fastforce
interpret FηG: natural_transformation C C ‹F o G› ‹F o G o F o G› ‹F o η o G›
by blast
interpret ε'ε: natural_transformation C C ‹F o G o F o G› Adj.C.map ‹ε' o ε›
proof -
have "natural_transformation C C ((F o G) o (F o G)) Adj.C.map (ε' o ε)"
by (metis (no_types, lifting))
thus "natural_transformation C C (F o G o F o G) Adj.C.map (ε' o ε)"
using o_assoc by metis
qed
interpret ε'εoFηG: vertical_composite
C C ‹F o G› ‹F o G o F o G› Adj.C.map ‹F o η o G› ‹ε' o ε› ..
have "ε' = vertical_composite.map C C (F o Adj.GεoηG.map) ε'"
also have "... = vertical_composite.map C C
(vertical_composite.map C C (F o η o G) (F o G o ε)) ε'"
by (metis (no_types, lifting))
also have "... = vertical_composite.map C C
(vertical_composite.map C C (F o η o G) (ε' o F o G)) ε"
proof -
have "vertical_composite.map C C
(vertical_composite.map C C (F o η o G) (F o G o ε)) ε'
= vertical_composite.map C C (F o η o G)
(vertical_composite.map C C (F o G o ε) ε')"
using vcomp_assoc
FGε.natural_transformation_axioms FηG.natural_transformation_axioms o_assoc)
also have "... = vertical_composite.map C C (F o η o G)
(vertical_composite.map C C (ε' o F o G) ε)"
interchange_spc [of C C "F o G" Adj.C.map ε C "F o G" Adj.C.map ε']
by (metis hcomp_ide_cod hcomp_ide_dom o_assoc)
also have "... = vertical_composite.map C C
(vertical_composite.map C C (F o η o G) (ε' o F o G)) ε"
using vcomp_assoc
horizontal_composite)
finally show ?thesis by simp
qed
also have "... = vertical_composite.map C C
(vertical_composite.map D C (F o η) (ε' o F) o G) ε"
by metis
also have "... = ε"
finally show ?thesis by simp
qed

lemma counit_determines_unit:
assumes "unit_counit_adjunction C D F G η ε"
and "unit_counit_adjunction C D F G η' ε"
shows "η = η'"
proof -
interpret Adj: unit_counit_adjunction C D F G η ε using assms(1) by auto
interpret Adj': unit_counit_adjunction C D F G η' ε using assms(2) by auto
interpret GFGF: composite_functor D C D F ‹G o F o G› ..
interpret GFη: natural_transformation D D ‹G o F› ‹(G o F) o (G o F)› ‹(G o F) o η›
horizontal_composite
by (metis (no_types, lifting))
interpret η'GF: natural_transformation D D ‹G o F› ‹(G o F) o (G o F)› ‹η' o (G o F)›
horizontal_composite
by (metis (no_types, lifting))
interpret GεF: natural_transformation D D ‹G o F o G o F› ‹G o F› ‹G o ε o F›
by blast
interpret η'η: natural_transformation D D Adj.D.map ‹G o F o G o F› ‹η' o η›
proof -
have "natural_transformation D D Adj.D.map ((G o F) o (G o F)) (η' o η)"
by fastforce
thus "natural_transformation D D Adj.D.map (G o F o G o F) (η' o η)"
using o_assoc by metis
qed
interpret GεFoη'η: vertical_composite
D D Adj.D.map ‹G o F o G o F› ‹G o F› ‹η' o η› ‹G o ε o F› ..
have "η' = vertical_composite.map D D η' (G o Adj.εFoFη.map)"
also have "... = vertical_composite.map D D η'
(vertical_composite.map D D (G o (F o η)) (G o (ε o F)))"
by fastforce
also have "... = vertical_composite.map D D
(vertical_composite.map D D η' (G o (F o η))) (G o ε o F)"
GFη.natural_transformation_axioms GεF.natural_transformation_axioms o_assoc
by (metis (no_types, lifting))
also have "... = vertical_composite.map D D
(vertical_composite.map D D η (η' o G o F)) (G o ε o F)"
using interchange_spc [of D D Adj.D.map "G o F" η D Adj.D.map "G o F" η']
by (metis hcomp_ide_cod hcomp_ide_dom o_assoc)
also have "... = vertical_composite.map D D η
(vertical_composite.map D D (η' o G o F) (G o ε o F))"
using vcomp_assoc
GεF.natural_transformation_axioms η'GF.natural_transformation_axioms o_assoc)
also have "... = vertical_composite.map D D η
(vertical_composite.map C D (η' o G) (G o ε) o F)"
by fastforce
also have "... = η"
by simp
finally show ?thesis by simp
qed

text‹
The grand unification of everything to do with an adjunction.
›

C: category C +
D: category D +
S: set_category S setp +
Cop: dual_category C +
Dop: dual_category D +
CopxC: product_category Cop.comp C +
DopxD: product_category Dop.comp D +
DopxC: product_category Dop.comp C +
idDop: identity_functor Dop.comp +
HomC: hom_functor C S setp φC +
HomD: hom_functor D S setp φD +
F: left_adjoint_functor D C F +
G: right_adjoint_functor C D G +
GF: composite_functor D C D F G +
FG: composite_functor C D C G F +
FGF: composite_functor D C C F FG.map +
GFG: composite_functor C D D G GF.map +
Fop: dual_functor Dop.comp Cop.comp F +
FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map +
DopxG: product_functor Dop.comp C Dop.comp D Dop.map G +
Hom_FopxC: composite_functor DopxC.comp CopxC.comp S FopxC.map HomC.map +
Hom_DopxG: composite_functor DopxC.comp DopxD.comp S DopxG.map HomD.map +
Hom_FopxC: set_valued_functor DopxC.comp S setp Hom_FopxC.map +
Hom_DopxG: set_valued_functor DopxC.comp S setp Hom_DopxG.map +
η: natural_transformation D D D.map GF.map η +
ε: natural_transformation C C FG.map C.map ε +
Fη: natural_transformation D C F ‹F o G o F› ‹F o η› +
ηG: natural_transformation C D G ‹G o F o G› ‹η o G› +
εF: natural_transformation D C ‹F o G o F› F ‹ε o F› +
Gε: natural_transformation C D ‹G o F o G› G ‹G o ε› +
εFoFη: vertical_composite D C F FGF.map F ‹F o η› ‹ε o F› +
GεoηG: vertical_composite C D G GFG.map G ‹η o G› ‹G o ε› +
φψ: meta_adjunction C D F G φ ψ +
ηε: unit_counit_adjunction C D F G η ε +
ΦΨ: hom_adjunction C D S setp φC φD F G Φ Ψ
for C :: "'c comp"     (infixr "⋅⇩C" 55)
and D :: "'d comp"     (infixr "⋅⇩D" 55)
and S :: "'s comp"     (infixr "⋅⇩S" 55)
and setp :: "'s set ⇒ bool"
and φC :: "'c * 'c ⇒ 'c ⇒ 's"
and φD :: "'d * 'd ⇒ 'd ⇒ 's"
and F :: "'d ⇒ 'c"
and G :: "'c ⇒ 'd"
and φ :: "'d ⇒ 'c ⇒ 'd"
and ψ :: "'c ⇒ 'd ⇒ 'c"
and η :: "'d ⇒ 'd"
and ε :: "'c ⇒ 'c"
and Φ :: "'d * 'c ⇒ 's"
and Ψ :: "'d * 'c ⇒ 's" +
assumes φ_in_terms_of_η: "⟦ D.ide y; «f : F y →⇩C x» ⟧ ⟹ φ y f = G f ⋅⇩D η y"
and ψ_in_terms_of_ε: "⟦ C.ide x; «g : y →⇩D G x» ⟧ ⟹ ψ x g = ε x ⋅⇩C F g"
and η_in_terms_of_φ: "D.ide y ⟹ η y = φ y (F y)"
and ε_in_terms_of_ψ: "C.ide x ⟹ ε x = ψ x (G x)"
and φ_in_terms_of_Φ: "⟦ D.ide y; «f : F y →⇩C x» ⟧ ⟹
φ y f = (ΦΨ.ψD (y, G x) o S.Fun (Φ (y, x)) o φC (F y, x)) f"
and ψ_in_terms_of_Ψ: "⟦ C.ide x; «g : y →⇩D G x» ⟧ ⟹
ψ x g = (ΦΨ.ψC (F y, x) o S.Fun (Ψ (y, x)) o φD (y, G x)) g"
and Φ_in_terms_of_φ:
"⟦ C.ide x; D.ide y ⟧ ⟹
Φ (y, x) = S.mkArr (HomC.set (F y, x)) (HomD.set (y, G x))
(φD (y, G x) o φ y o ΦΨ.ψC (F y, x))"
and Ψ_in_terms_of_ψ:
"⟦ C.ide x; D.ide y ⟧ ⟹
Ψ (y, x) = S.mkArr (HomD.set (y, G x)) (HomC.set (F y, x))
(φC (F y, x) o ψ x o ΦΨ.ψD (y, G x))"

begin

interpretation GF: composite_functor D C D F G ..
interpretation FG: composite_functor C D C G F ..
interpretation FGF: composite_functor D C C F FG.map ..
interpretation GFG: composite_functor C D D G GF.map ..

definition ηo :: "'d ⇒ 'd"
where "ηo y = φ y (F y)"

lemma ηo_in_hom:
assumes "D.ide y"
shows "«ηo y : y →⇩D G (F y)»"
using assms D.ide_in_hom ηo_def φ_in_hom by force

lemma φ_in_terms_of_ηo:
assumes "D.ide y" and "«f : F y →⇩C x»"
shows "φ y f = G f ⋅⇩D ηo y"
proof (unfold ηo_def)
have 1: "«F y : F y →⇩C F y»"
using assms(1) D.ide_in_hom by blast
hence "φ y (F y) = φ y (F y) ⋅⇩D y"
by (metis assms(1) D.in_homE φ_in_hom D.comp_arr_dom)
thus "φ y f = G f ⋅⇩D φ y (F y)"
using assms 1 D.ide_in_hom by (metis C.comp_arr_dom C.in_homE φ_naturality)
qed

lemma φ_F_char:
assumes "«g : y' →⇩D y»"
shows "φ y' (F g) = ηo y ⋅⇩D g"
using assms ηo_def φ_in_hom [of y "F y" "F y"]
D.comp_cod_arr [of "D (φ y (F y)) g" "G (F y)"]
φ_naturality [of "F y" "F y" "F y" g y' y "F y"]
by (metis C.ide_in_hom D.arr_cod_iff_arr D.arr_dom D.cod_cod D.cod_dom D.comp_ide_arr
D.comp_ide_self D.ide_cod D.in_homE F.as_nat_trans.is_natural_2 F.functor_axioms
F.preserves_section_retraction φ_in_hom functor.preserves_hom)

interpretation η: transformation_by_components D D D.map GF.map ηo
proof
show "⋀a. D.ide a ⟹ «ηo a : D.map a →⇩D GF.map a»"
using ηo_def φ_in_hom D.ide_in_hom by force
fix f
assume f: "D.arr f"
show "ηo (D.cod f) ⋅⇩D D.map f = GF.map f ⋅⇩D ηo (D.dom f)"
using f φ_F_char [of "D.map f" "D.dom f" "D.cod f"]
φ_in_terms_of_ηo [of "D.dom f" "F f" "F (D.cod f)"]
by force
qed

lemma η_map_simp:
assumes "D.ide y"
shows "η.map y = φ y (F y)"
using assms η.map_simp_ide ηo_def by simp

definition εo :: "'c ⇒ 'c"
where "εo x = ψ x (G x)"

lemma εo_in_hom:
assumes "C.ide x"
shows "«εo x : F (G x) →⇩C x»"
using assms C.ide_in_hom εo_def ψ_in_hom by force

lemma ψ_in_terms_of_εo:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "ψ x g = εo x ⋅⇩C F g"
proof -
have "εo x ⋅⇩C F g = x ⋅⇩C ψ x (G x) ⋅⇩C F g"
using assms εo_def ψ_in_hom [of x "G x" "G x"]
C.comp_cod_arr [of "ψ x (G x) ⋅⇩C F g" x]
by fastforce
also have "... = ψ x (G x ⋅⇩D G x ⋅⇩D g)"
using assms ψ_naturality [of x x x g y "G x" "G x"] by force
also have "... = ψ x g"
using assms D.comp_cod_arr by fastforce
finally show ?thesis by simp
qed

lemma ψ_G_char:
assumes "«f: x →⇩C x'»"
shows "ψ x' (G f) = f ⋅⇩C εo x"
proof (unfold εo_def)
have 0: "C.ide x ∧ C.ide x'" using assms by auto
thus "ψ x' (G f) = f ⋅⇩C ψ x (G x)"
using 0 assms ψ_naturality ψ_in_hom [of x "G x" "G x"] G.preserves_hom εo_def
ψ_in_terms_of_εo G.as_nat_trans.is_natural_1 C.ide_in_hom
by (metis C.arrI C.in_homE)
qed

interpretation ε: transformation_by_components C C FG.map C.map εo
apply unfold_locales
using εo_in_hom
apply simp
using ψ_G_char ψ_in_terms_of_εo
by (metis C.arr_iff_in_hom C.ide_cod C.map_simp G.preserves_hom comp_apply)

lemma ε_map_simp:
assumes "C.ide x"
shows "ε.map x = ψ x (G x)"
using assms εo_def by simp

interpretation FD: composite_functor D D C D.map F ..
interpretation CF: composite_functor D C C F C.map ..
interpretation GC: composite_functor C C D C.map G ..
interpretation DG: composite_functor C D D G D.map ..

interpretation Fη: natural_transformation D C F ‹F o G o F› ‹F o η.map›
by (metis (no_types, lifting) F.as_nat_trans.natural_transformation_axioms
F.functor_axioms η.natural_transformation_axioms comp_functor_identity
horizontal_composite o_assoc)

interpretation εF: natural_transformation D C ‹F o G o F› F ‹ε.map o F›
using ε.natural_transformation_axioms F.as_nat_trans.natural_transformation_axioms
horizontal_composite
by fastforce

interpretation ηG: natural_transformation C D G ‹G o F o G› ‹η.map o G›
using η.natural_transformation_axioms G.as_nat_trans.natural_transformation_axioms
horizontal_composite
by fastforce

interpretation Gε: natural_transformation C D ‹G o F o G› G ‹G o ε.map›
by (metis (no_types, lifting) G.as_nat_trans.natural_transformation_axioms
G.functor_axioms ε.natural_transformation_axioms comp_functor_identity
horizontal_composite o_assoc)

interpretation εFoFη: vertical_composite D C F ‹F o G o F› F ‹F o η.map› ‹ε.map o F›
..
interpretation GεoηG: vertical_composite C D G ‹G o F o G› G ‹η.map o G› ‹G o ε.map›
..

lemma unit_counit_F:
assumes "D.ide y"
shows "F y = εo (F y) ⋅⇩C F (ηo y)"
using assms ψ_in_terms_of_εo ηo_def ψ_φ ηo_in_hom F.preserves_ide C.ide_in_hom by metis

lemma unit_counit_G:
assumes "C.ide x"
shows "G x = G (εo x) ⋅⇩D ηo (G x)"
using assms φ_in_terms_of_ηo εo_def φ_ψ εo_in_hom G.preserves_ide D.ide_in_hom by metis

shows "unit_counit_adjunction C D F G η.map ε.map"
proof
show "εFoFη.map = F"
using εFoFη.is_natural_transformation εFoFη.map_simp_ide unit_counit_F
F.as_nat_trans.natural_transformation_axioms
by (intro NaturalTransformation.eqI) auto
show "GεoηG.map = G"
using GεoηG.is_natural_transformation GεoηG.map_simp_ide unit_counit_G
G.as_nat_trans.natural_transformation_axioms
by (intro NaturalTransformation.eqI) auto
qed

definition η :: "'d ⇒ 'd" where "η ≡ η.map"
definition ε :: "'c ⇒ 'c" where "ε ≡ ε.map"

shows "unit_counit_adjunction C D F G η ε"
unfolding η_def ε_def

lemma η_is_natural_transformation:
shows "natural_transformation D D D.map GF.map η"
unfolding η_def ..

lemma ε_is_natural_transformation:
shows "natural_transformation C C FG.map C.map ε"
unfolding ε_def ..

text‹
From the defined @{term η} and @{term ε} we can recover the original @{term φ} and @{term ψ}.
›

lemma φ_in_terms_of_η:
assumes "D.ide y" and "«f : F y →⇩C x»"
shows "φ y f = G f ⋅⇩D η y"
using assms η_def by (simp add: φ_in_terms_of_ηo)

lemma ψ_in_terms_of_ε:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "ψ x g = ε x ⋅⇩C F g"
using assms ε_def by (simp add: ψ_in_terms_of_εo)

end

begin

interpretation unit_counit_adjunction C D F G η ε
using induces_unit_counit_adjunction η_def ε_def by auto

lemma has_terminal_arrows_from_functor:
assumes x: "C.ide x"
shows "terminal_arrow_from_functor D C F (G x) x (ε x)"
and "⋀y' f. arrow_from_functor D C F y' x f
⟹ terminal_arrow_from_functor.the_coext D C F (G x) (ε x) y' f = φ y' f"
proof -
interpret εx: arrow_from_functor D C F ‹G x› x ‹ε x›
using x ε.preserves_hom G.preserves_ide by unfold_locales auto
have 1: "⋀y' f. arrow_from_functor D C F y' x f ⟹
εx.is_coext y' f (φ y' f) ∧ (∀g'. εx.is_coext y' f g' ⟶ g' = φ y' f)"
using x
by (metis (full_types) εx.is_coext_def φ_ψ ψ_in_terms_of_ε arrow_from_functor.arrow
φ_in_hom ψ_φ)
interpret εx: terminal_arrow_from_functor D C F ‹G x› x ‹ε x›
using 1 by unfold_locales blast
show "terminal_arrow_from_functor D C F (G x) x (ε x)" ..
show "⋀y' f. arrow_from_functor D C F y' x f ⟹ εx.the_coext y' f = φ y' f"
using 1 εx.the_coext_def by auto
qed

apply unfold_locales using has_terminal_arrows_from_functor by auto

lemma has_initial_arrows_to_functor:
assumes y: "D.ide y"
shows "initial_arrow_to_functor C D G y (F y) (η y)"
and "⋀x' g. arrow_to_functor C D G y x' g ⟹
initial_arrow_to_functor.the_ext C D G (F y) (η y) x' g = ψ x' g"
proof -
interpret ηy: arrow_to_functor C D G y ‹F y› ‹η y›
using y by unfold_locales auto
have 1: "⋀x' g. arrow_to_functor C D G y x' g ⟹
ηy.is_ext x' g (ψ x' g) ∧ (∀f'. ηy.is_ext x' g f' ⟶ f' = ψ x' g)"
using y
by (metis (full_types) ηy.is_ext_def ψ_φ φ_in_terms_of_η arrow_to_functor.arrow
ψ_in_hom φ_ψ)
interpret ηy: initial_arrow_to_functor C D G y ‹F y› ‹η y›
apply unfold_locales using 1 by blast
show "initial_arrow_to_functor C D G y (F y) (η y)" ..
show "⋀x' g. arrow_to_functor C D G y x' g ⟹ ηy.the_ext x' g = ψ x' g"
using 1 ηy.the_ext_def by auto
qed

apply unfold_locales using has_initial_arrows_to_functor by auto

end

begin

definition φ :: "'d ⇒ 'c ⇒ 'd"
where "φ y h = G h ⋅⇩D η y"

definition ψ :: "'c ⇒ 'd ⇒ 'c"
where "ψ x h = ε x ⋅⇩C F h"

interpretation meta_adjunction C D F G φ ψ
proof
fix x :: 'c and y :: 'd and f :: 'c
assume y: "D.ide y" and f: "«f : F y →⇩C x»"
show 0: "«φ y f : y →⇩D G x»"
using f y G.preserves_hom η.preserves_hom φ_def D.ide_in_hom by auto
show "ψ x (φ y f) = f"
proof -
have "ψ x (φ y f) = (ε x ⋅⇩C F (G f)) ⋅⇩C F (η y)"
using y f φ_def ψ_def C.comp_assoc by auto
also have "... = (f ⋅⇩C ε (F y)) ⋅⇩C F (η y)"
using y f ε.naturality by auto
also have "... = f"
using y f εFoFη.map_simp_2 triangle_F C.comp_arr_dom D.ide_in_hom C.comp_assoc
by fastforce
finally show ?thesis by auto
qed
next
fix x :: 'c and y :: 'd and g :: 'd
assume x: "C.ide x" and g: "«g : y →⇩D G x»"
show "«ψ x g : F y →⇩C x»" using g x ψ_def by fastforce
show "φ y (ψ x g) = g"
proof -
have "φ y (ψ x g) = (G (ε x) ⋅⇩D η (G x)) ⋅⇩D g"
using g x φ_def ψ_def η.naturality [of g] D.comp_assoc by auto
also have "... = g"
using x g triangle_G D.comp_ide_arr GεoηG.map_simp_ide by auto
finally show ?thesis by auto
qed
next
fix f :: 'c and g :: 'd and h :: 'c and x :: 'c and x' :: 'c and y :: 'd and y' :: 'd
assume f: "«f : x →⇩C x'»" and g: "«g : y' →⇩D y»" and h: "«h : F y →⇩C x»"
show "φ y' (f ⋅⇩C h ⋅⇩C F g) = G f ⋅⇩D φ y h ⋅⇩D g"
using φ_def f g h η.naturality D.comp_assoc by fastforce
qed

shows "meta_adjunction C D F G φ ψ" ..

text‹
From the defined @{term φ} and @{term ψ} we can recover the original @{term η} and @{term ε}.
›

lemma η_in_terms_of_φ:
assumes "D.ide y"
shows "η y = φ y (F y)"
using assms φ_def D.comp_cod_arr by auto

lemma ε_in_terms_of_ψ:
assumes "C.ide x"
shows "ε x = ψ x (G x)"
using assms ψ_def C.comp_arr_dom by auto

end

text‹
A left adjoint functor induces a meta-adjunction, modulo the choice of a
›

begin

definition Go :: "'c ⇒ 'd"
where "Go a = (SOME b. ∃e. terminal_arrow_from_functor D C F b a e)"

definition εo :: "'c ⇒ 'c"
where "εo a = (SOME e. terminal_arrow_from_functor D C F (Go a) a e)"

lemma Go_εo_terminal:
assumes "∃b e. terminal_arrow_from_functor D C F b a e"
shows "terminal_arrow_from_functor D C F (Go a) a (εo a)"
using assms Go_def εo_def
someI_ex [of "λb. ∃e. terminal_arrow_from_functor D C F b a e"]
someI_ex [of "λe. terminal_arrow_from_functor D C F (Go a) a e"]
by simp

text‹
The right adjoint @{term G} to @{term F} takes each arrow @{term f} of
@{term[source=true] C} to the unique @{term[source=true] D}-coextension of
@{term "C f (εo (C.dom f))"} along @{term "εo (C.cod f)"}.
›

definition G :: "'c ⇒ 'd"
where "G f = (if C.arr f then
terminal_arrow_from_functor.the_coext D C F (Go (C.cod f)) (εo (C.cod f))
(Go (C.dom f)) (f ⋅⇩C εo (C.dom f))
else D.null)"

lemma G_ide:
assumes "C.ide x"
shows "G x = Go x"
proof -
interpret terminal_arrow_from_functor D C F ‹Go x› x ‹εo x›
using assms ex_terminal_arrow Go_εo_terminal by blast
have 1: "arrow_from_functor D C F (Go x) x (εo x)" ..
have "is_coext (Go x) (εo x) (Go x)"
using arrow is_coext_def C.in_homE C.comp_arr_dom by auto
hence "Go x = the_coext (Go x) (εo x)" using 1 the_coext_unique by blast
moreover have "εo x = C x (εo (C.dom x))"
using assms arrow C.comp_ide_arr C.seqI' C.ide_in_hom C.in_homE by metis
ultimately show ?thesis using assms G_def C.cod_dom C.ide_in_hom C.in_homE by metis
qed

lemma G_is_functor:
shows "functor C D G"
proof
fix f :: 'c
assume "¬C.arr f"
thus "G f = D.null" using G_def by auto
next
fix f :: 'c
assume f: "C.arr f"
let ?x = "C.dom f"
let ?x' = "C.cod f"
interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ‹?x› ‹εo ?x›
using f ex_terminal_arrow Go_εo_terminal by simp
interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ‹?x'› ‹εo ?x'›
using f ex_terminal_arrow Go_εo_terminal by simp
have 1: "arrow_from_functor D C F (Go ?x) ?x' (C f (εo ?x))"
using f xε.arrow by (unfold_locales, auto)
have "G f = x'ε.the_coext (Go ?x) (C f (εo ?x))" using f G_def by simp
hence Gf: "«G f : Go ?x →⇩D Go ?x'» ∧ f ⋅⇩C εo ?x = εo ?x' ⋅⇩C F (G f)"
using 1 x'ε.the_coext_prop by simp
show "D.arr (G f)" using Gf by auto
show "D.dom (G f) = G ?x" using f Gf G_ide by auto
show "D.cod (G f) = G ?x'" using f Gf G_ide by auto
next
fix f f' :: 'c
assume ff': "C.arr (C f' f)"
have f: "C.arr f" using ff' by auto
let ?x = "C.dom f"
let ?x' = "C.cod f"
let ?x'' = "C.cod f'"
interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ‹?x› ‹εo ?x›
using f ex_terminal_arrow Go_εo_terminal by simp
interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ‹?x'› ‹εo ?x'›
using f ex_terminal_arrow Go_εo_terminal by simp
interpret x''ε: terminal_arrow_from_functor D C F ‹Go ?x''› ‹?x''› ‹εo ?x''›
using ff' ex_terminal_arrow Go_εo_terminal by auto
have 1: "arrow_from_functor D C F (Go ?x) ?x' (f ⋅⇩C εo ?x)"
using f xε.arrow by (unfold_locales, auto)
have 2: "arrow_from_functor D C F (Go ?x') ?x'' (f' ⋅⇩C εo ?x')"
using ff' x'ε.arrow by (unfold_locales, auto)
have "G f = x'ε.the_coext (Go ?x) (C f (εo ?x))"
using f G_def by simp
hence Gf: "D.in_hom (G f) (Go ?x) (Go ?x') ∧ f ⋅⇩C εo ?x = εo ?x' ⋅⇩C F (G f)"
using 1 x'ε.the_coext_prop by simp
have "G f' = x''ε.the_coext (Go ?x') (f' ⋅⇩C εo ?x')"
using ff' G_def by auto
hence Gf': "«G f' : Go (C.cod f) →⇩D Go (C.cod f')» ∧ f' ⋅⇩C εo ?x' = εo ?x'' ⋅⇩C F (G f')"
using 2 x''ε.the_coext_prop by simp
show "G (f' ⋅⇩C f) = G f' ⋅⇩D G f"
proof -
have "x''ε.is_coext (Go ?x) ((f' ⋅⇩C f) ⋅⇩C εo ?x) (G f' ⋅⇩D G f)"
proof -
have 3: "«G f' ⋅⇩D G f : Go (C.dom f) →⇩D Go (C.cod f')»" using 1 2 Gf Gf' by auto
moreover have "(f' ⋅⇩C f) ⋅⇩C εo ?x = εo ?x'' ⋅⇩C F (G f' ⋅⇩D G f)"
by (metis 3 C.comp_assoc D.in_homE Gf Gf' preserves_comp)
ultimately show ?thesis using x''ε.is_coext_def by auto
qed
moreover have "arrow_from_functor D C F (Go ?x) ?x'' ((f' ⋅⇩C f) ⋅⇩C εo ?x)"
using ff' xε.arrow by unfold_locales blast
ultimately show ?thesis
using ff' G_def x''ε.the_coext_unique C.seqE C.cod_comp C.dom_comp by auto
qed
qed

interpretation G: "functor" C D G using G_is_functor by auto

lemma G_simp:
assumes "C.arr f"
shows "G f = terminal_arrow_from_functor.the_coext D C F (Go (C.cod f)) (εo (C.cod f))
(Go (C.dom f)) (f ⋅⇩C εo (C.dom f))"
using assms G_def by simp

interpretation idC: identity_functor C ..
interpretation GF: composite_functor C D C G F ..

interpretation ε: transformation_by_components C C GF.map C.map εo
proof
fix x :: 'c
assume x: "C.ide x"
show "«εo x : GF.map x →⇩C C.map x»"
proof -
interpret terminal_arrow_from_functor D C F ‹Go x› x ‹εo x›
using x Go_εo_terminal ex_terminal_arrow by simp
show ?thesis using x G_ide arrow by auto
qed
next
fix f :: 'c
assume f: "C.arr f"
show "εo (C.cod f) ⋅⇩C GF.map f = C.map f ⋅⇩C εo (C.dom f)"
proof -
let ?x = "C.dom f"
let ?x' = "C.cod f"
interpret xε: terminal_arrow_from_functor D C F ‹Go ?x› ?x ‹εo ?x›
using f Go_εo_terminal ex_terminal_arrow by simp
interpret x'ε: terminal_arrow_from_functor D C F ‹Go ?x'› ?x' ‹εo ?x'›
using f Go_εo_terminal ex_terminal_arrow by simp
have 1: "arrow_from_functor D C F (Go ?x) ?x' (C f (εo ?x))"
using f xε.arrow by unfold_locales auto
have "G f = x'ε.the_coext (Go ?x) (f ⋅⇩C εo ?x)"
using f G_simp by blast
hence "x'ε.is_coext (Go ?x) (f ⋅⇩C εo ?x) (G f)"
using 1 x'ε.the_coext_prop x'ε.is_coext_def by auto
thus ?thesis
using f x'ε.is_coext_def by simp
qed
qed

definition ψ
where "ψ x h = C (ε.map x) (F h)"

lemma ψ_in_hom:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "«ψ x g : F y →⇩C x»"
unfolding ψ_def using assms ε.maps_ide_in_hom by auto

lemma ψ_natural:
assumes f: "«f : x →⇩C x'»" and g: "«g : y' →⇩D y»" and h: "«h : y →⇩D G x»"
shows "f ⋅⇩C ψ x h ⋅⇩C F g = ψ x' ((G f ⋅⇩D h) ⋅⇩D g)"
proof -
have "f ⋅⇩C ψ x h ⋅⇩C F g = f ⋅⇩C (ε.map x ⋅⇩C F h) ⋅⇩C F g"
unfolding ψ_def by auto
also have "... = (f ⋅⇩C ε.map x) ⋅⇩C F h ⋅⇩C F g"
using C.comp_assoc by fastforce
also have "... = (f ⋅⇩C ε.map x) ⋅⇩C F (h ⋅⇩D g)"
using g h by fastforce
also have "... = (ε.map x' ⋅⇩C F (G f)) ⋅⇩C F (h ⋅⇩D g)"
using f ε.naturality by auto
also have "... = ε.map x' ⋅⇩C F ((G f ⋅⇩D h) ⋅⇩D g)"
using f g h C.comp_assoc by fastforce
also have "... = ψ x' ((G f ⋅⇩D h) ⋅⇩D g)"
unfolding ψ_def by auto
finally show ?thesis by auto
qed

lemma ψ_inverts_coext:
assumes x: "C.ide x" and g: "«g : y →⇩D G x»"
shows "arrow_from_functor.is_coext D C F (G x) (ε.map x) y (ψ x g) g"
proof -
interpret xε: arrow_from_functor D C F ‹G x› x ‹ε.map x›
using x ε.maps_ide_in_hom by unfold_locales auto
show "xε.is_coext y (ψ x g) g"
using x g ψ_def xε.is_coext_def G_ide by blast
qed

lemma ψ_invertible:
assumes y: "D.ide y" and f: "«f : F y →⇩C x»"
shows "∃!g. «g : y →⇩D G x» ∧ ψ x g = f"
proof
have x: "C.ide x" using f by auto
interpret xε: terminal_arrow_from_functor D C F ‹Go x› x ‹εo x›
using x ex_terminal_arrow Go_εo_terminal by auto
have 1: "arrow_from_functor D C F y x f"
using y f by (unfold_locales, auto)
let ?g = "xε.the_coext y f"
have "ψ x ?g = f"
using 1 x y ψ_def xε.the_coext_prop G_ide ψ_inverts_coext xε.is_coext_def by simp
thus "«?g : y →⇩D G x» ∧ ψ x ?g = f"
using 1 x xε.the_coext_prop G_ide by simp
show "⋀g'. «g' : y →⇩D G x» ∧ ψ x g' = f ⟹ g' = ?g"
using 1 x y ψ_inverts_coext G_ide xε.the_coext_unique by force
qed

definition φ
where "φ y f = (THE g. «g : y →⇩D G (C.cod f)» ∧ ψ (C.cod f) g = f)"

lemma φ_in_hom:
assumes "D.ide y" and "«f : F y →⇩C x»"
shows "«φ y f : y →⇩D G x»"
using assms ψ_invertible φ_def theI' [of "λg. «g : y →⇩D G x» ∧ ψ x g = f"]
by auto

lemma φ_ψ:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "φ y (ψ x g) = g"
proof -
have "φ y (ψ x g) = (THE g'. «g' : y →⇩D G x» ∧ ψ x g' = ψ x g)"
proof -
have "C.cod (ψ x g) = x"
using assms ψ_in_hom by auto
thus ?thesis
using φ_def by auto
qed
moreover have "∃!g'. «g' : y →⇩D G x» ∧ ψ x g' = ψ x g"
using assms ψ_in_hom ψ_invertible D.ide_dom by blast
ultimately show "φ y (ψ x g) = g"
using assms(2) by auto
qed

lemma ψ_φ:
assumes "D.ide y" and "«f : F y →⇩C x»"
shows "ψ x (φ y f) = f"
using assms ψ_invertible φ_def theI' [of "λg. «g : y →⇩D G x» ∧ ψ x g = f"]
by auto

lemma φ_natural:
assumes "«f : x →⇩C x'»" and "«g : y' →⇩D y»" and "«h : F y →⇩C x»"
shows "φ y' (f ⋅⇩C h ⋅⇩C F g) = (G f ⋅⇩D φ y h) ⋅⇩D g"
proof -
have "C.ide x' ∧ D.ide y ∧ D.in_hom (φ y h) y (G x)"
using assms φ_in_hom by auto
thus ?thesis
using assms D.comp_in_homI G.preserves_hom ψ_natural [of f x x' g y' y "φ y h"] φ_ψ ψ_φ
by auto
qed

shows "meta_adjunction C D F G φ ψ"
using φ_in_hom ψ_in_hom φ_ψ ψ_φ φ_natural D.comp_assoc
by unfold_locales auto

end

text‹
A right adjoint functor induces a meta-adjunction, modulo the choice of a
›

begin

definition Fo :: "'d ⇒ 'c"
where "Fo y = (SOME x. ∃u. initial_arrow_to_functor C D G y x u)"

definition ηo :: "'d ⇒ 'd"
where "ηo y = (SOME u. initial_arrow_to_functor C D G y (Fo y) u)"

lemma Fo_ηo_initial:
assumes "∃x u. initial_arrow_to_functor C D G y x u"
shows "initial_arrow_to_functor C D G y (Fo y) (ηo y)"
using assms Fo_def ηo_def
someI_ex [of "λx. ∃u. initial_arrow_to_functor C D G y x u"]
someI_ex [of "λu. initial_arrow_to_functor C D G y (Fo y) u"]
by simp

text‹
The left adjoint @{term F} to @{term g} takes each arrow @{term g} of
@{term[source=true] D} to the unique @{term[source=true] C}-extension of
@{term "D (ηo (D.cod g)) g"} along @{term "ηo (D.dom g)"}.
›

definition F :: "'d ⇒ 'c"
where "F g = (if D.arr g then
initial_arrow_to_functor.the_ext C D G (Fo (D.dom g)) (ηo (D.dom g))
(Fo (D.cod g)) (ηo (D.cod g) ⋅⇩D g)
else C.null)"

lemma F_ide:
assumes "D.ide y"
shows "F y = Fo y"
proof -
interpret initial_arrow_to_functor C D G y ‹Fo y› ‹ηo y›
using assms ex_initial_arrow Fo_ηo_initial by blast
have 1: "arrow_to_functor C D G y (Fo y) (ηo y)" ..
have "is_ext (Fo y) (ηo y) (Fo y)"
unfolding is_ext_def using arrow D.comp_ide_arr [of "G (Fo y)" "ηo y"] by force
hence "Fo y = the_ext (Fo y) (ηo y)"
using 1 the_ext_unique by blast
moreover have "ηo y = D (ηo (D.cod y)) y"
using assms arrow D.comp_arr_ide D.comp_arr_dom by auto
ultimately show ?thesis
using assms F_def D.dom_cod D.in_homE D.ide_in_hom by metis
qed

lemma F_is_functor:
shows "functor D C F"
proof
fix g :: 'd
assume "¬D.arr g"
thus "F g = C.null" using F_def by auto
next
fix g :: 'd
assume g: "D.arr g"
let ?y = "D.dom g"
let ?y' = "D.cod g"
interpret yη: initial_arrow_to_functor C D G ?y ‹Fo ?y› ‹ηo ?y›
using g ex_initial_arrow Fo_ηo_initial by simp
interpret y'η: initial_arrow_to_functor C D G ?y' ‹Fo ?y'› ‹ηo ?y'›
using g ex_initial_arrow Fo_ηo_initial by simp
have 1: "arrow_to_functor C D G ?y (Fo ?y') (D (ηo ?y') g)"
using g y'η.arrow by unfold_locales auto
have "F g = yη.the_ext (Fo ?y') (D (ηo ?y') g)"
using g F_def by simp
hence Fg: "«F g : Fo ?y →⇩C Fo ?y'» ∧ ηo ?y' ⋅⇩D g = G (F g) ⋅⇩D ηo ?y"
using 1 yη.the_ext_prop by simp
show "C.arr (F g)" using Fg by auto
show "C.dom (F g) = F ?y" using Fg g F_ide by auto
show "C.cod (F g) = F ?y'" using Fg g F_ide by auto
next
fix g :: 'd
fix g' :: 'd
assume g': "D.arr (D g' g)"
have g: "D.arr g" using g' by auto
let ?y = "D.dom g"
let ?y' = "D.cod g"
let ?y'' = "D.cod g'"
interpret yη: initial_arrow_to_functor C D G ?y ‹Fo ?y› ‹ηo ?y›
using g ex_initial_arrow Fo_ηo_initial by simp
interpret y'η: initial_arrow_to_functor C D G ?y' ‹Fo ?y'› ‹ηo ?y'›
using g ex_initial_arrow Fo_ηo_initial by simp
interpret y''η: initial_arrow_to_functor C D G ?y'' ‹Fo ?y''› ‹ηo ?y''›
using g' ex_initial_arrow Fo_ηo_initial by auto
have 1: "arrow_to_functor C D G ?y (Fo ?y') (ηo ?y' ⋅⇩D g)"
using g y'η.arrow by unfold_locales auto
have "F g = yη.the_ext (Fo ?y') (ηo ?y' ⋅⇩D g)"
using g F_def by simp
hence Fg: "«F g : Fo ?y →⇩C Fo ?y'» ∧ ηo ?y' ⋅⇩D g = G (F g) ⋅⇩D ηo ?y"
using 1 yη.the_ext_prop by simp
have 2: "arrow_to_functor C D G ?y' (Fo ?y'') (ηo ?y'' ⋅⇩D g')"
using g' y''η.arrow by unfold_locales auto
have "F g' = y'η.the_ext (Fo ?y'') (ηo ?y'' ⋅⇩D g')"
using g' F_def by auto
hence Fg': "«F g' : Fo ?y' →⇩C Fo ?y''» ∧ ηo ?y'' ⋅⇩D g' = G (F g') ⋅⇩D ηo ?y'"
using 2 y'η.the_ext_prop by simp
show "F (g' ⋅⇩D g) = F g' ⋅⇩C F g"
proof -
have "yη.is_ext (Fo ?y'') (ηo ?y'' ⋅⇩D g' ⋅⇩D g) (F g' ⋅⇩C F g)"
proof -
have 3: "«F g' ⋅⇩C F g : Fo ?y →⇩C Fo ?y''»" using 1 2 Fg Fg' by auto
moreover have "ηo ?y'' ⋅⇩D g' ⋅⇩D g = G (F g' ⋅⇩C F g) ⋅⇩D ηo ?y"
using Fg Fg' g g' 3 y''η.arrow
by (metis C.arrI D.comp_assoc preserves_comp)
ultimately show ?thesis using yη.is_ext_def by auto
qed
moreover have "arrow_to_functor C D G ?y (Fo ?y'') (ηo ?y'' ⋅⇩D g' ⋅⇩D g)"
using g g' y''η.arrow by unfold_locales auto
ultimately show ?thesis
using g g' F_def yη.the_ext_unique D.dom_comp D.cod_comp by auto
qed
qed

interpretation F: "functor" D C F using F_is_functor by auto

lemma F_simp:
assumes "D.arr g"
shows "F g = initial_arrow_to_functor.the_ext C D G (Fo (D.dom g)) (ηo (D.dom g))
(Fo (D.cod g)) (ηo (D.cod g) ⋅⇩D g)"
using assms F_def by simp

interpretation FG: composite_functor D C D F G ..

interpretation η: transformation_by_components D D D.map FG.map ηo
proof
fix y :: 'd
assume y: "D.ide y"
show "«ηo y : D.map y →⇩D FG.map y»"
proof -
interpret initial_arrow_to_functor C D G y ‹Fo y› ‹ηo y›
using y Fo_ηo_initial ex_initial_arrow by simp
show ?thesis using y F_ide arrow by auto
qed
next
fix g :: 'd
assume g: "D.arr g"
show "ηo (D.cod g) ⋅⇩D D.map g = FG.map g ⋅⇩D ηo (D.dom g)"
proof -
let ?y = "D.dom g"
let ?y' = "D.cod g"
interpret yη: initial_arrow_to_functor C D G ?y ‹Fo ?y› ‹ηo ?y›
using g Fo_ηo_initial ex_initial_arrow by simp
interpret y'η: initial_arrow_to_functor C D G ?y' ‹Fo ?y'› ‹ηo ?y'›
using g Fo_ηo_initial ex_initial_arrow by simp
have "arrow_to_functor C D G ?y (Fo ?y') (ηo ?y' ⋅⇩D g)"
using g y'η.arrow by unfold_locales auto
moreover have "F g = yη.the_ext (Fo ?y') (ηo ?y' ⋅⇩D g)"
using g F_simp by blast
ultimately have "yη.is_ext (Fo ?y') (ηo ?y' ⋅⇩D g) (F g)"
using yη.the_ext_prop yη.is_ext_def by auto
thus ?thesis
using g yη.is_ext_def by simp
qed
qed

definition φ
where "φ y h = D (G h) (η.map y)"

lemma φ_in_hom:
assumes y: "D.ide y" and f: "«f : F y →⇩C x»"
shows "«φ y f : y →⇩D G x»"
unfolding φ_def using assms η.maps_ide_in_hom by auto

lemma φ_natural:
assumes f: "«f : x →⇩C x'»" and g: "«g : y' →⇩D y»" and h: "«h : F y →⇩C x»"
shows "φ y' (f ⋅⇩C h ⋅⇩C F g) = (G f ⋅⇩D φ y h) ⋅⇩D g"
proof -
have "(G f ⋅⇩D φ y h) ⋅⇩D g = (G f ⋅⇩D G h ⋅⇩D η.map y) ⋅⇩D g"
unfolding φ_def by auto
also have "... = (G f ⋅⇩D G h) ⋅⇩D η.map y ⋅⇩D g"
using D.comp_assoc by fastforce
also have "... = G (f ⋅⇩C h) ⋅⇩D G (F g) ⋅⇩D η.map y'"
using f g h η.naturality by fastforce
also have "... = (G (f ⋅⇩C h) ⋅⇩D G (F g)) ⋅⇩D η.map y'"
using D.comp_assoc by fastforce
also have "... = G (f ⋅⇩C h ⋅⇩C F g) ⋅⇩D η.map y'"
using f g h D.comp_assoc by fastforce
also have "... = φ y' (f ⋅⇩C h ⋅⇩C F g)"
unfolding φ_def by auto
finally show ?thesis by auto
qed

lemma φ_inverts_ext:
assumes y: "D.ide y" and f: "«f : F y →⇩C x»"
shows "arrow_to_functor.is_ext C D G (F y) (η.map y) x (φ y f) f"
proof -
interpret yη: arrow_to_functor C D G y ‹F y› ‹η.map y›
using y η.maps_ide_in_hom by unfold_locales auto
show "yη.is_ext x (φ y f) f"
using f y φ_def yη.is_ext_def F_ide by blast
qed

lemma φ_invertible:
assumes x: "C.ide x" and g: "«g : y →⇩D G x»"
shows "∃!f. «f : F y →⇩C x» ∧ φ y f = g"
proof
have y: "D.ide y" using g by auto
interpret yη: initial_arrow_to_functor C D G y ‹Fo y› ‹ηo y›
using y ex_initial_arrow Fo_ηo_initial by auto
have 1: "arrow_to_functor C D G y x g"
using x g by (unfold_locales, auto)
let ?f = "yη.the_ext x g"
have "φ y ?f = g"
using φ_def yη.the_ext_prop 1 F_ide x y φ_inverts_ext yη.is_ext_def by fastforce
moreover have "«?f : F y →⇩C x»"
using 1 y yη.the_ext_prop F_ide by simp
ultimately show "«?f : F y →⇩C x» ∧ φ y ?f = g" by auto
show "⋀f'. «f' : F y →⇩C x» ∧ φ y f' = g ⟹ f' = ?f"
using 1 y φ_inverts_ext yη.the_ext_unique F_ide by force
qed

definition ψ
where "ψ x g = (THE f. «f : F (D.dom g) →⇩C x» ∧ φ (D.dom g) f = g)"

lemma ψ_in_hom:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "C.in_hom (ψ x g) (F y) x"
using assms φ_invertible ψ_def theI' [of "λf. «f : F y →⇩C x» ∧ φ y f = g"]
by auto

lemma ψ_φ:
assumes "D.ide y" and "«f : F y →⇩C x»"
shows "ψ x (φ y f) = f"
proof -
have "D.dom (φ y f) = y" using assms φ_in_hom by blast
hence "ψ x (φ y f) = (THE f'. «f' : F y →⇩C x» ∧ φ y f' = φ y f)"
using ψ_def by auto
moreover have "∃!f'. «f' : F y →⇩C x» ∧ φ y f' = φ y f"
using assms φ_in_hom φ_invertible C.ide_cod by blast
ultimately show ?thesis using assms(2) by auto
qed

lemma φ_ψ:
assumes "C.ide x" and "«g : y →⇩D G x»"
shows "φ y (ψ x g) = g"
using assms φ_invertible ψ_def theI' [of "λf. «f : F y →⇩C x» ∧ φ y f = g"]
by auto

shows "meta_adjunction C D F G φ ψ"
using φ_in_hom ψ_in_hom φ_ψ ψ_φ φ_natural D.comp_assoc
by (unfold_locales, auto)

end

text‹
To obtain a hom-adjunction from a meta-adjunction, we need to exhibit hom-functors
from @{term C} and @{term D} to a common set category @{term S}, so it is necessary
to apply an actual concrete construction of such a category.
We use the replete set category generated by the disjoint sum
@{typ "('c+'d)"} of the arrow types of @{term C} and @{term D}.
›

begin

interpretation S: replete_setcat ‹TYPE('c+'d)› .

definition inC :: "'c ⇒ ('c+'d) setcat.arr"
where "inC ≡ S.UP o Inl"

definition inD :: "'d ⇒ ('c+'d) setcat.arr"
where "inD ≡ S.UP o Inr"

interpretation S: replete_setcat ‹TYPE('c+'d)› .
interpretation Cop: dual_category C ..
interpretation Dop: dual_category D ..
interpretation CopxC: product_category Cop.comp C ..
interpretation DopxD: product_category Dop.comp D ..
interpretation DopxC: product_category Dop.comp C ..
interpretation HomC: hom_functor C S.comp S.setp ‹λ_. inC›
proof
show "⋀f. C.arr f ⟹ inC f ∈ S.Univ"
unfolding inC_def using S.UP_mapsto by auto
thus "⋀b a. ⟦C.ide b; C.ide a⟧ ⟹ inC  C.hom b a ⊆ S.Univ"
by blast
show "⋀b a. ⟦C.ide b; C.ide a⟧ ⟹ inj_on inC (C.hom b a)"
unfolding inC_def
using S.inj_UP
by (metis injD inj_Inl inj_compose inj_on_def)
qed
interpretation HomD: hom_functor D S.comp S.setp ‹λ_. inD›
proof
show "⋀f. D.arr f ⟹ inD f ∈ S.Univ"
unfolding inD_def using S.UP_mapsto by auto
thus "⋀b a. ⟦D.ide b; D.ide a⟧ ⟹ inD  D.hom b a ⊆ S.Univ"
by blast
show "⋀b a. ⟦D.ide b; D.ide a⟧ ⟹ inj_on inD (D.hom b a)"
unfolding inD_def
using S.inj_UP
by (metis injD inj_Inr inj_compose inj_on_def)
qed
interpretation Fop: dual_functor D C F ..
interpretation FopxC: product_functor Dop.comp C Cop.comp C Fop.map C.map ..
interpretation DopxG: product_functor Dop.comp C Dop.comp D Dop.map G ..
interpretation Hom_FopxC: composite_functor DopxC.comp CopxC.comp S.comp
FopxC.map HomC.map ..
interpretation Hom_DopxG: composite_functor DopxC.comp DopxD.comp S.comp
DopxG.map HomD.map ..

lemma inC_ψ [simp]:
assumes "C.ide b" and "C.ide a" and "x ∈ inC  C.hom b a"
shows "inC (HomC.ψ (b, a) x) = x"
using assms by auto

lemma ψ_inC [simp]:
assumes "C.arr f"
shows "HomC.ψ (C.dom f, C.cod f) (inC f) = f"
using assms HomC.ψ_φ by blast

lemma inD_ψ [simp]:
assumes "D.ide b" and "D.ide a" and "x ∈ inD  D.hom b a"
shows "inD (HomD.ψ (b, a) x) = x"
using assms by auto

lemma ψ_inD [simp]:
assumes "D.arr f"
shows "HomD.ψ (D.dom f, D.cod f) (inD f) = f"
using assms HomD.ψ_φ by blast

lemma Hom_FopxC_simp:
assumes "DopxC.arr gf"
shows "Hom_FopxC.map gf =
S.mkArr (HomC.set (F (D.cod (fst gf)), C.dom (snd gf)))
(HomC.set (F (D.dom (fst gf)), C.cod (snd gf)))
(inC ∘ (λh. snd gf ⋅⇩C h ⋅⇩C F (fst gf))
∘ HomC.ψ (F (D.cod (fst gf)), C.dom (snd gf)))"
using assms HomC.map_def by simp

lemma Hom_DopxG_simp:
assumes "DopxC.arr gf"
shows "Hom_DopxG.map gf =
S.mkArr (HomD.set (D.cod (fst gf), G (C.dom (snd gf))))
(HomD.set (D.dom (fst gf), G (C.cod (snd gf))))
(inD ∘ (λh. G (snd gf) ⋅⇩D h ⋅⇩D fst gf)
∘ HomD.ψ (D.cod (fst gf), G (C.dom (snd gf))))"
using assms HomD.map_def by simp

definition Φo
where "Φo yx = S.mkArr (HomC.set (F (fst yx), snd yx))
(HomD.set (fst yx, G (snd yx)))
(inD o φ (fst yx) o HomC.ψ (F (fst yx), snd yx))"

lemma Φo_in_hom:
assumes yx: "DopxC.ide yx"
shows "«Φo yx : Hom_FopxC.map yx →⇩S Hom_DopxG.map yx»"
proof -
have "Hom_FopxC.map yx = S.mkIde (HomC.set (F (fst yx), snd yx))"
using yx HomC.map_ide by auto
moreover have "Hom_DopxG.map yx = S.mkIde (HomD.set (fst yx, G (snd yx)))"
using yx HomD.map_ide by auto
moreover have
"«S.mkArr (HomC.set (F (fst yx), snd yx)) (HomD.set (fst yx, G (snd yx)))
(inD ∘ φ (fst yx) ∘ HomC.ψ (F (fst yx), snd yx)) :
S.mkIde (HomC.set (F (fst yx), snd yx))
→⇩S S.mkIde (HomD.set (fst yx, G (snd yx)))»"
proof (intro S.mkArr_in_hom)
show "HomC.set (F (fst yx), snd yx) ⊆ S.Univ" using yx HomC.set_subset_Univ by simp
show "HomD.set (fst yx, G (snd yx)) ⊆ S.Univ" using yx HomD.set_subset_Univ by simp
show "inD o φ (fst yx) o HomC.ψ (F (fst yx), snd yx)
∈ HomC.set (F (fst yx), snd yx) → HomD.set (fst yx, G (snd yx))"
proof
fix x
assume x: "x ∈ HomC.set (F (fst yx), snd yx)"
show "(inD o φ (fst yx) o HomC.ψ (F (fst yx), snd yx)) x
∈ HomD.set (fst yx, G (snd yx))"
using x yx HomC.ψ_mapsto [of "F (fst yx)" "snd yx"]
φ_in_hom [of "fst yx"] HomD.φ_mapsto [of "fst yx" "G (snd yx)"]
by auto
qed
qed
ultimately show ?thesis using Φo_def by auto
qed

interpretation Φ: transformation_by_components
DopxC.comp S.comp Hom_FopxC.map Hom_DopxG.map Φo
proof
fix yx
assume yx: "DopxC.ide yx"
show "«Φo yx : Hom_FopxC.map yx →⇩S Hom_DopxG.map yx»"
using yx Φo_in_hom by auto
next
fix gf
assume gf: "DopxC.arr gf"
show "S.comp (Φo (DopxC.cod gf)) (Hom_FopxC.map gf)
= S.comp (Hom_DopxG.map gf) (Φo (DopxC.dom gf))"
proof -
let ?g = "fst gf"
let ?f = "snd gf"
let ?x = "C.dom ?f"
let ?x' = "C.cod ?f"
let ?y = "D.cod ?g"
let ?y' = "D.dom ?g"
let ?Fy = "F ?y"
let ?Fy' = "F ?y'"
let ?Fg = "F ?g"
let ?Gx = "G ?x"
let ?Gx' = "G ?x'"
let ?Gf = "G ?f"
have 1: "S.arr (Hom_FopxC.map gf) ∧
Hom_FopxC.map gf = S.mkArr (HomC.set (?Fy, ?x)) (HomC.set (?Fy', ?x'))
(inC o (λh. ?f ⋅⇩C h ⋅⇩C ?Fg) o HomC.ψ (?Fy, ?x))"
using gf Hom_FopxC.preserves_arr Hom_FopxC_simp