Theory Modification
section "Modifications"
text ‹
Modifications are morphisms of pseudonatural transformations.
In this section, we give a definition of ``modification'', and we prove that
the mappings ‹η› and ‹ε›, which were chosen in the course of showing that a
pseudonatural equivalence ‹τ› has a converse pseudonatural equivalence ‹τ'›,
are invertible modifications that relate the composites ‹τ'τ› and ‹ττ'›
to the identity pseudonatural transformations on ‹F› and ‹G›.
This means that ‹τ› and ‹τ'› are quasi-inverses in a suitable bicategory
of pseudofunctors, pseudonatural transformations, and modifications, though
we do not go so far as to give a formal construction of such a bicategory.
›
theory Modification
imports PseudonaturalTransformation
begin
locale modification =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
τ: pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G τ⇩0 τ⇩1 +
τ': pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G τ⇩0' τ⇩1'
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ⇩F :: "'c * 'c ⇒ 'd"
and G :: "'c ⇒ 'd"
and Φ⇩G :: "'c * 'c ⇒ 'd"
and τ⇩0 :: "'c ⇒ 'd"
and τ⇩1 :: "'c ⇒ 'd"
and τ⇩0' :: "'c ⇒ 'd"
and τ⇩1' :: "'c ⇒ 'd"
and Γ :: "'c ⇒ 'd" +
assumes Γ_in_hom: "C.obj a ⟹ «Γ a : τ⇩0 a ⇒⇩D τ⇩0' a»"
and naturality: "⟦ «f : a →⇩C b»; C.ide f ⟧ ⟹ τ⇩1' f ⋅⇩D (G f ⋆⇩D Γ a) = (Γ b ⋆⇩D F f) ⋅⇩D τ⇩1 f"
locale invertible_modification =
modification +
assumes components_are_iso: "C.obj a ⟹ D.iso (Γ a)"
locale identity_modification =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
τ: pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G τ⇩0 τ⇩1
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ⇩F :: "'c * 'c ⇒ 'd"
and G :: "'c ⇒ 'd"
and Φ⇩G :: "'c * 'c ⇒ 'd"
and τ⇩0 :: "'c ⇒ 'd"
and τ⇩1 :: "'c ⇒ 'd"
begin
abbreviation map
where "map ≡ τ⇩0"
sublocale invertible_modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G τ⇩0 τ⇩1 τ⇩0 τ⇩1 map
using D.comp_arr_dom D.comp_cod_arr
by unfold_locales auto
end
locale composite_modification =
C: bicategory V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C +
D: bicategory V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D +
ρ: pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G ρ⇩0 ρ⇩1 +
σ: pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G σ⇩0 σ⇩1 +
τ: pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G τ⇩0 τ⇩1 +
Γ: modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G ρ⇩0 ρ⇩1 σ⇩0 σ⇩1 Γ +
Δ: modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G σ⇩0 σ⇩1 τ⇩0 τ⇩1 Δ
for V⇩C :: "'c comp" (infixr "⋅⇩C" 55)
and H⇩C :: "'c comp" (infixr "⋆⇩C" 53)
and 𝖺⇩C :: "'c ⇒ 'c ⇒ 'c ⇒ 'c" ("𝖺⇩C[_, _, _]")
and 𝗂⇩C :: "'c ⇒ 'c" ("𝗂⇩C[_]")
and src⇩C :: "'c ⇒ 'c"
and trg⇩C :: "'c ⇒ 'c"
and V⇩D :: "'d comp" (infixr "⋅⇩D" 55)
and H⇩D :: "'d comp" (infixr "⋆⇩D" 53)
and 𝖺⇩D :: "'d ⇒ 'd ⇒ 'd ⇒ 'd" ("𝖺⇩D[_, _, _]")
and 𝗂⇩D :: "'d ⇒ 'd" ("𝗂⇩D[_]")
and src⇩D :: "'d ⇒ 'd"
and trg⇩D :: "'d ⇒ 'd"
and F :: "'c ⇒ 'd"
and Φ⇩F :: "'c * 'c ⇒ 'd"
and G :: "'c ⇒ 'd"
and Φ⇩G :: "'c * 'c ⇒ 'd"
and ρ⇩0 :: "'c ⇒ 'd"
and ρ⇩1 :: "'c ⇒ 'd"
and σ⇩0 :: "'c ⇒ 'd"
and σ⇩1 :: "'c ⇒ 'd"
and τ⇩0 :: "'c ⇒ 'd"
and τ⇩1 :: "'c ⇒ 'd"
and Γ :: "'c ⇒ 'd"
and Δ :: "'c ⇒ 'd"
begin
abbreviation map
where "map a ≡ Δ a ⋅⇩D Γ a"
sublocale modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G ρ⇩0 ρ⇩1 τ⇩0 τ⇩1 map
using Δ.Γ_in_hom Γ.Γ_in_hom Δ.naturality Γ.naturality
apply unfold_locales
apply auto[1]
proof -
fix f a b
assume f: "«f : a →⇩C b»" and ide_f: "C.ide f"
have "τ⇩1 f ⋅⇩D (G f ⋆⇩D map a) = (τ⇩1 f ⋅⇩D (G f ⋆⇩D Δ a)) ⋅⇩D (G f ⋆⇩D Γ a)"
proof -
have "D.seq (Δ a) (Γ a)"
using f Δ.Γ_in_hom Γ.Γ_in_hom by blast
thus ?thesis
using f ide_f D.whisker_left [of "G f" "Δ a" "Γ a"] D.comp_assoc
by simp
qed
also have "... = (Δ b ⋆⇩D F f) ⋅⇩D σ⇩1 f ⋅⇩D (G f ⋆⇩D Γ a)"
using f ide_f Δ.naturality [of f a b] D.comp_assoc by simp
also have "... = ((Δ b ⋆⇩D F f) ⋅⇩D (Γ b ⋆⇩D F f)) ⋅⇩D ρ⇩1 f"
using f ide_f Γ.naturality [of f a b] D.comp_assoc by simp
also have "... = (map b ⋆⇩D F f) ⋅⇩D ρ⇩1 f"
proof -
have "D.seq (Δ b) (Γ b)"
using f Δ.Γ_in_hom Γ.Γ_in_hom by blast
thus ?thesis
using f ide_f D.whisker_right [of "F f" "Δ b" "Γ b"] by simp
qed
finally show "τ⇩1 f ⋅⇩D (G f ⋆⇩D map a) = (map b ⋆⇩D F f) ⋅⇩D ρ⇩1 f" by simp
qed
end
context converse_pseudonatural_equivalence
begin
interpretation EV: self_evaluation_map V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ..
notation EV.eval ("⦃_⦄")
interpretation ι⇩F: identity_pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F
..
interpretation ι⇩G: identity_pseudonatural_transformation
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G
..
interpretation τ'τ: composite_pseudonatural_equivalence
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F G Φ⇩G F Φ⇩F
τ⇩0 τ⇩1 map⇩0 map⇩1
..
interpretation ττ': composite_pseudonatural_equivalence
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G F Φ⇩F G Φ⇩G
map⇩0 map⇩1 τ⇩0 τ⇩1
..
interpretation η: invertible_modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F F Φ⇩F
ι⇩F.map⇩0 ι⇩F.map⇩1 τ'τ.map⇩0 τ'τ.map⇩1 η
proof
show "⋀a. C.obj a ⟹ «η a : F.map⇩0 a ⇒⇩D τ'τ.map⇩0 a»"
using unit_in_hom τ'τ.map⇩0_def by simp
show "⋀a. C.obj a ⟹ D.iso (η a)"
by simp
show "⋀f a b. ⟦ «f : a →⇩C b»; C.ide f⟧
⟹ τ'τ.map⇩1 f ⋅⇩D (F f ⋆⇩D η a) = (η b ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f] ⋅⇩D 𝗋⇩D[F f]"
proof -
fix f a b
assume f: "«f : a →⇩C b»" and ide_f: "C.ide f"
have a: "C.obj a" and b: "C.obj b"
using f by auto
have "τ'τ.map⇩1 f ⋅⇩D (F f ⋆⇩D η a) =
(𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a)
⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[F f, τ⇩0' a, τ⇩0 a]) ⋅⇩D
(F f ⋆⇩D η a)"
unfolding τ'τ.map⇩1_def map⇩1_def
using a b f D.comp_assoc by auto
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
(((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
(((𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[F f, τ⇩0' a, τ⇩0 a]) ⋅⇩D
(F f ⋆⇩D η a)"
proof -
have "(τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a)
⋆⇩D τ⇩0 a
= ((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
(((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a)"
proof -
have "D.arr ((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a))"
using a b f ide_f τ.iso_map⇩1_ide
by (metis (no_types, lifting) C.in_hhomE map⇩1_def map⇩1_simps(1))
thus ?thesis
using a b f D.whisker_right [of "τ⇩0 a"] by fastforce
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
(((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[F⇩0 b ⋆⇩D F f, τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(F f ⋆⇩D η a)"
proof -
have "((𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D 𝖺⇩D⇧-⇧1[F f, τ⇩0' a, τ⇩0 a] =
𝖺⇩D⇧-⇧1[F⇩0 b ⋆⇩D F f, τ⇩0' a, τ⇩0 a] ⋅⇩D (𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a)"
using a b f ide_f D.assoc'_naturality [of "𝗅⇩D⇧-⇧1[F f]" "τ⇩0' a" "τ⇩0 a"] by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[F⇩0 b ⋆⇩D F f, τ⇩0' a, τ⇩0 a]) ⋅⇩D
((F⇩0 b ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D (F f ⋆⇩D η a) = 𝗅⇩D⇧-⇧1[F f] ⋆⇩D η a"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "𝗅⇩D⇧-⇧1[F f]" "F f" "τ⇩0' a ⋆⇩D τ⇩0 a" "η a"]
by simp
also have "... = ((F⇩0 b ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D (𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "F⇩0 b ⋆⇩D F f" "𝗅⇩D⇧-⇧1[F f]" "η a" "F⇩0 a"]
by auto
finally have "(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D (F f ⋆⇩D η a) =
((F⇩0 b ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D (𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f, τ⇩0' a, τ⇩0 a] ⋅⇩D
(((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
((F⇩0 b ⋆⇩D F f) ⋆⇩D η a)) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D 𝖺⇩D⇧-⇧1[F⇩0 b ⋆⇩D F f, τ⇩0' a, τ⇩0 a] =
𝖺⇩D⇧-⇧1[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f, τ⇩0' a, τ⇩0 a] ⋅⇩D ((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a)"
using a b f ide_f D.assoc'_naturality [of "η b ⋆⇩D F f" "τ⇩0' a" "τ⇩0 a"] by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
((((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a)) ⋅⇩D
𝖺⇩D⇧-⇧1[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f, τ⇩0' a, τ⇩0 a] ⋅⇩D
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D ((F⇩0 b ⋆⇩D F f) ⋆⇩D η a)
= (η b ⋆⇩D F f) ⋆⇩D η a"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "η b ⋆⇩D F f" "F⇩0 b ⋆⇩D F f" "τ⇩0' a ⋆⇩D τ⇩0 a" "η a"]
by auto
also have "... = (((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D ((η b ⋆⇩D F f) ⋆⇩D F⇩0 a)"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f" "η b ⋆⇩D F f" "η a" "F⇩0 a"]
by auto
finally have "((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D ((F⇩0 b ⋆⇩D F f) ⋆⇩D η a) =
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D ((η b ⋆⇩D F f) ⋆⇩D F⇩0 a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
((((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f, τ⇩0' a, τ⇩0 a]) ⋅⇩D
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
((𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) =
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a"
using a b f ide_f D.whisker_right τ.iso_map⇩1_ide by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a)) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f, τ⇩0' a, τ⇩0 a] =
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a)"
using a b f ide_f τ.iso_map⇩1_ide
D.assoc'_naturality
[of "(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]" "τ⇩0' a" "τ⇩0 a"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋆⇩D η a) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) =
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]) ⋅⇩D ((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D
(τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D η a"
using a b f ide_f τ.iso_map⇩1_ide
D.interchange [of "(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]"
"(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f" "τ⇩0' a ⋆⇩D τ⇩0 a" "η a"]
by auto
also have "... = (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D η a"
using a b f ide_f τ.iso_map⇩1_ide D.comp_arr_dom D.comp_cod_arr D.comp_assoc
by auto
also have "... = (τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋅⇩D
(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D
𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]
⋆⇩D η a ⋅⇩D F⇩0 a"
using a b f ide_f τ.iso_map⇩1_ide D.comp_arr_dom D.comp_cod_arr by auto
also have "... = ((τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋆⇩D η a) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a)"
proof -
have "D.seq (τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f])"
using a b f ide_f τ.iso_map⇩1_ide
by (intro D.seqI D.hseqI') auto
thus ?thesis
using a b f ide_f τ.iso_map⇩1_ide D.comp_arr_dom D.comp_cod_arr
D.interchange [of "(τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a)"
"(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]"
"η a" "F⇩0 a"]
by simp
qed
finally have "((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f) ⋆⇩D η a) =
((τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋆⇩D η a) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a ⋆⇩D τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, τ⇩0 a, τ⇩0' a ⋆⇩D τ⇩0 a]) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a
= (𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a ⋆⇩D τ⇩0' a, τ⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a)"
proof -
have "(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋆⇩D τ⇩0 a
= (𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a)"
using a b f ide_f D.hcomp_reassoc D.whisker_right [of "τ⇩0 a"] by auto
also have "... = (𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a ⋆⇩D τ⇩0' a, τ⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a)"
using a b f ide_f D.hcomp_reassoc(1) [of "τ⇩0' b ⋆⇩D G f" "ε a" "τ⇩0 a"]
by auto
finally show ?thesis by blast
qed
moreover have "(τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋆⇩D η a
= (𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, τ⇩0 a, τ⇩0' a ⋆⇩D τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)"
proof -
have "(τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a) ⋆⇩D η a =
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D ((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a) ⋅⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D
(τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D η a ⋅⇩D F⇩0 a"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.hcomp_reassoc(2) [of "τ⇩0' b" "G f" "τ⇩0 a"]
by auto
also have "... = (𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a) ⋆⇩D η a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)"
using a b f ide_f D.inv_inv D.iso_inv_iso D.interchange by auto
also have "... = (𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, τ⇩0 a, τ⇩0' a ⋆⇩D τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)"
using a b f ide_f D.hcomp_reassoc(1) [of "τ⇩0' b ⋆⇩D G f" "τ⇩0 a" "η a"] by auto
finally show ?thesis by blast
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
(((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a]) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a)) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a ⋆⇩D τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, τ⇩0 a, τ⇩0' a ⋆⇩D τ⇩0 a] =
(τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a]"
proof -
have "𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a ⋆⇩D τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a ⋆⇩D τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D (G f ⋆⇩D τ⇩0 a), τ⇩0' a, τ⇩0 a] ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D τ⇩0' a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, τ⇩0 a, τ⇩0' a ⋆⇩D τ⇩0 a]
= ⦃❙𝖺❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩, ❙⟨τ⇩0 a❙⟩❙] ❙⋅
(❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩❙] ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
((❙⟨τ⇩0' b❙⟩ ❙⋆ ❙𝖺❙[ ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
(❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩ ❙⋆ ❙⟨τ⇩0 a❙⟩, ❙⟨τ⇩0' a❙⟩❙] ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩ ❙⋆ (❙⟨G f❙⟩ ❙⋆ ❙⟨τ⇩0 a❙⟩), ❙⟨τ⇩0' a❙⟩, ❙⟨τ⇩0 a❙⟩❙] ❙⋅
(❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩❙] ❙⋆ ❙⟨τ⇩0' a❙⟩ ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩, ❙⟨τ⇩0' a❙⟩ ❙⋆ ❙⟨τ⇩0 a❙⟩❙]⦄"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C
by auto
also have "... = ⦃(❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩) ❙⋆ ❙𝖺⇧-⇧1❙[❙⟨τ⇩0 a❙⟩, ❙⟨τ⇩0' a❙⟩, ❙⟨τ⇩0 a❙⟩❙]⦄"
using a b f ide_f by (intro EV.eval_eqI, auto)
also have "... = (τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a]"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C
by auto
finally show ?thesis by blast
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝗅⇩D⇧-⇧1[τ⇩0 a] ⋅⇩D 𝗋⇩D[τ⇩0 a]) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)) ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
interpret adjoint_equivalence_in_bicategory
V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹τ⇩0 a› ‹τ⇩0' a› ‹η a› ‹ε a›
using a chosen_adjoint_equivalence by simp
have "((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a]) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a)
= (τ⇩0' b ⋆⇩D G f) ⋆⇩D (ε a ⋆⇩D τ⇩0 a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a] ⋅⇩D
(τ⇩0 a ⋆⇩D η a)"
using a b f ide_f D.whisker_left by auto
also have "... = (τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝗅⇩D⇧-⇧1[τ⇩0 a] ⋅⇩D 𝗋⇩D[τ⇩0 a]"
using triangle_left by simp
finally have "((τ⇩0' b ⋆⇩D G f) ⋆⇩D ε a ⋆⇩D τ⇩0 a) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 a, τ⇩0' a, τ⇩0 a]) ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D τ⇩0 a ⋆⇩D η a)
= (τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝗅⇩D⇧-⇧1[τ⇩0 a] ⋅⇩D 𝗋⇩D[τ⇩0 a]"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
(τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
(𝗋⇩D[τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a)) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝗅⇩D⇧-⇧1[τ⇩0 a] ⋅⇩D 𝗋⇩D[τ⇩0 a]) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)
= 𝗋⇩D[τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a]"
proof -
have "𝖺⇩D[τ⇩0' b, G f, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, G f, G⇩0 a] ⋆⇩D τ⇩0 a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D G f, G⇩0 a, τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D G f) ⋆⇩D 𝗅⇩D⇧-⇧1[τ⇩0 a] ⋅⇩D 𝗋⇩D[τ⇩0 a]) ⋅⇩D
𝖺⇩D[τ⇩0' b ⋆⇩D G f, τ⇩0 a, F⇩0 a]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0' b, G f, τ⇩0 a] ⋆⇩D F⇩0 a)
= ⦃❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩❙] ❙⋅
((❙⟨τ⇩0' b❙⟩ ❙⋆ ❙𝗋❙[❙⟨G f❙⟩❙]) ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
(❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩, ❙⟨G⇩0 a❙⟩⇩0❙] ❙⋆ ❙⟨τ⇩0 a❙⟩) ❙⋅
(❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩, ❙⟨G⇩0 a❙⟩⇩0, ❙⟨τ⇩0 a❙⟩❙] ❙⋅
((❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩) ❙⋆ ❙𝗅⇧-⇧1❙[❙⟨τ⇩0 a❙⟩❙] ❙⋅ ❙𝗋❙[❙⟨τ⇩0 a❙⟩❙]) ❙⋅
❙𝖺❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩, ❙⟨F⇩0 a❙⟩⇩0❙]) ❙⋅
(❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩, ❙⟨G f❙⟩, ❙⟨τ⇩0 a❙⟩❙] ❙⋆ ❙⟨F⇩0 a❙⟩⇩0)⦄"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C D.𝔩_ide_simp D.𝔯_ide_simp
by auto
also have "... = ⦃❙𝗋❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨G f❙⟩ ❙⋆ ❙⟨τ⇩0 a❙⟩❙]⦄"
using a b f ide_f by (intro EV.eval_eqI, auto)
also have "... = 𝗋⇩D[τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a]"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C D.𝔩_ide_simp D.𝔯_ide_simp
by auto
finally show ?thesis by blast
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
((τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D
(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)))) ⋅⇩D
𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D 𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f] ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "𝗋⇩D[τ⇩0' b ⋆⇩D G f ⋆⇩D τ⇩0 a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D F⇩0 a)
= (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D
𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f]"
using a b f ide_f D.comp_assoc τ.iso_map⇩1_ide
D.runit_naturality [of "(τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = ((𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D
𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]) ⋅⇩D
𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f]) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D ((τ⇩0' b ⋆⇩D τ⇩1 f) ⋅⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)))
= 𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f]"
using a b f ide_f D.comp_arr_inv' D.comp_arr_dom τ.iso_map⇩1_ide
D.whisker_left [of "τ⇩0' b" "τ⇩1 f" "D.inv (τ⇩1 f)"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f] ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D F⇩0 a)) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "(𝖺⇩D⇧-⇧1[τ⇩0' b, τ⇩0 b, F f] ⋅⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f]) ⋅⇩D 𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f]
= 𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f]"
using a b f ide_f D.comp_inv_arr' D.comp_cod_arr by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (η b ⋆⇩D F f) ⋅⇩D 𝗋⇩D[F⇩0 b ⋆⇩D F f] ⋅⇩D (𝗅⇩D⇧-⇧1[F f] ⋆⇩D F⇩0 a)"
proof -
have "𝗋⇩D[(τ⇩0' b ⋆⇩D τ⇩0 b) ⋆⇩D F f] ⋅⇩D ((η b ⋆⇩D F f) ⋆⇩D F⇩0 a)
= (η b ⋆⇩D F f) ⋅⇩D 𝗋⇩D[F⇩0 b ⋆⇩D F f]"
using a b f ide_f D.runit_naturality [of "η b ⋆⇩D F f"] by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (η b ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f] ⋅⇩D 𝗋⇩D[F f]"
using a b f ide_f D.runit_naturality [of "𝗅⇩D⇧-⇧1[F f]"] by auto
finally show "τ'τ.map⇩1 f ⋅⇩D (F f ⋆⇩D η a) = (η b ⋆⇩D F f) ⋅⇩D 𝗅⇩D⇧-⇧1[F f] ⋅⇩D 𝗋⇩D[F f]"
by blast
qed
qed
lemma unit_is_invertible_modification:
shows "invertible_modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D F Φ⇩F F Φ⇩F
ι⇩F.map⇩0 ι⇩F.map⇩1 τ'τ.map⇩0 τ'τ.map⇩1 η"
..
interpretation ε: invertible_modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G G Φ⇩G
ττ'.map⇩0 ττ'.map⇩1 ι⇩G.map⇩0 ι⇩G.map⇩1 ε
proof
show "⋀a. C.obj a ⟹ «ε a : ττ'.map⇩0 a ⇒⇩D G⇩0 a»"
using counit_in_hom ττ'.map⇩0_def by simp
show "⋀a. C.obj a ⟹ D.iso (ε a)"
by simp
show "⋀f a b. ⟦«f : a →⇩C b»; C.ide f⟧
⟹ (𝗅⇩D⇧-⇧1[G f] ⋅⇩D 𝗋⇩D[G f]) ⋅⇩D (G f ⋆⇩D ε a) = (ε b ⋆⇩D G f) ⋅⇩D ττ'.map⇩1 f"
proof -
fix f a b
assume f: "«f : a →⇩C b»" and ide_f: "C.ide f"
have a: "C.obj a" and b: "C.obj b"
using f by auto
have "(ε b ⋆⇩D G f) ⋅⇩D ττ'.map⇩1 f
= (ε b ⋆⇩D G f) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f] ⋅⇩D
(τ⇩0 b ⋆⇩D
(τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
unfolding ττ'.map⇩1_def map⇩1_def
using a b f D.comp_assoc by auto
also have "... = (ε b ⋆⇩D G f) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
((τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a)) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "τ⇩0 b ⋆⇩D
(τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a)
= (τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a)"
proof -
have "D.arr ((τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
((η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a))"
using a b f ide_f τ.iso_map⇩1_ide
by (intro D.seqI) auto
thus ?thesis
using a b f D.whisker_left [of "τ⇩0 b"] by fastforce
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (ε b ⋆⇩D G f) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a)
= τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a] ⋅⇩D
((τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a)"
using a b f ide_f D.whisker_left [of "τ⇩0 b"] τ.iso_map⇩1_ide by auto
also have "... = τ⇩0 b ⋆⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]"
using a b f ide_f τ.iso_map⇩1_ide
D.assoc_naturality [of "τ⇩0' b" "D.inv (τ⇩1 f)" "τ⇩0' a"]
by auto
also have "... = (τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a])"
using a b f ide_f D.whisker_left [of "τ⇩0 b"] τ.iso_map⇩1_ide by auto
finally have "(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, G f ⋆⇩D τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D (τ⇩0' b ⋆⇩D D.inv (τ⇩1 f)) ⋆⇩D τ⇩0' a)
= (τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a])"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (ε b ⋆⇩D G f) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝗋⇩D[G f])) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)
= τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"
using a b f ide_f D.whisker_left τ.iso_map⇩1_ide by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (ε b ⋆⇩D G f) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D G⇩0 a] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a)) ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f] ⋅⇩D (τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝗋⇩D[G f])
= ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D G⇩0 a]"
using a b f ide_f D.assoc'_naturality [of "τ⇩0 b" "τ⇩0' b" "𝗋⇩D[G f]"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (ε b ⋆⇩D G f) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D G⇩0 a] ⋅⇩D (τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D G f ⋆⇩D ε a)
= ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a]"
using a b f ide_f D.assoc'_naturality [of "τ⇩0 b" "τ⇩0' b" "G f ⋆⇩D ε a"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = ((ε b ⋆⇩D G f) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f])) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D τ⇩0' b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))
= ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a]"
using a b f ide_f τ.iso_map⇩1_ide
D.assoc'_naturality
[of "τ⇩0 b" "τ⇩0' b" "𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
((ε b ⋆⇩D G f ⋆⇩D G⇩0 a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a)) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(ε b ⋆⇩D G f) ⋅⇩D ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f]) = ε b ⋆⇩D 𝗋⇩D[G f]"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "ε b" "τ⇩0 b ⋆⇩D τ⇩0' b" "G f" "𝗋⇩D[G f]"]
by simp
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D (ε b ⋆⇩D G f ⋆⇩D G⇩0 a)"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "G⇩0 b" "ε b" "𝗋⇩D[G f]" "G f ⋆⇩D G⇩0 a"]
by auto
finally have "(ε b ⋆⇩D G f) ⋅⇩D ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝗋⇩D[G f]) =
(G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D (ε b ⋆⇩D G f ⋆⇩D G⇩0 a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
((ε b ⋆⇩D G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(ε b ⋆⇩D G f ⋆⇩D G⇩0 a) ⋅⇩D ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a)
= ε b ⋆⇩D G f ⋆⇩D ε a"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "ε b" "τ⇩0 b ⋆⇩D τ⇩0' b" "G f ⋆⇩D G⇩0 a" "G f ⋆⇩D ε a"]
by auto
also have "... = (G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D (ε b ⋆⇩D G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a)"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.interchange [of "G⇩0 b" "ε b" "G f ⋆⇩D ε a" "G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a"]
by auto
finally have "(ε b ⋆⇩D G f ⋆⇩D G⇩0 a) ⋅⇩D ((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D G f ⋆⇩D ε a) =
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D (ε b ⋆⇩D G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(ε b ⋆⇩D (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have 1: "D.seq (G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a)
(𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))"
using a b f ide_f τ.iso_map⇩1_ide
by (intro D.seqI D.hseqI') auto
have 2: "D.seq (𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))
((τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a)"
using a b f ide_f τ.iso_map⇩1_ide
by (intro D.seqI D.hseqI') auto
have "(ε b ⋆⇩D G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) =
ε b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"
using 1 a b f ide_f D.comp_arr_dom D.comp_cod_arr τ.iso_map⇩1_ide
D.interchange [of "ε b" "τ⇩0 b ⋆⇩D τ⇩0' b" "G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a"
"𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"]
by auto
also have "... = G⇩0 b ⋅⇩D ε b ⋆⇩D
(𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
((τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a)"
using a b f ide_f τ.iso_map⇩1_ide D.comp_arr_dom D.comp_cod_arr by auto
also have "... = (G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(ε b ⋆⇩D (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a)"
using 2 a b f ide_f τ.iso_map⇩1_ide D.comp_assoc
D.interchange [of "G⇩0 b" "ε b"
"𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"
"(τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a"]
by simp
finally have "(ε b ⋆⇩D G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a))
= (G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(ε b ⋆⇩D (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a)"
by blast
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b ⋆⇩D τ⇩0' b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0 b, τ⇩0' b ⋆⇩D τ⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "ε b ⋆⇩D (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a
= (G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b ⋆⇩D τ⇩0' b, τ⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a])"
proof -
have "ε b ⋆⇩D (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a
= (G⇩0 b ⋅⇩D ε b ⋅⇩D (τ⇩0 b ⋆⇩D τ⇩0' b)) ⋆⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D (τ⇩0 b ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr
D.hcomp_reassoc(1) [of "τ⇩0 b" "F f" "τ⇩0' a"]
by auto
also have "... = (G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(ε b ⋆⇩D τ⇩0 b ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a])"
using a b f ide_f D.comp_arr_dom D.comp_cod_arr D.assoc'_is_natural_1
D.interchange [of "G⇩0 b" "ε b ⋅⇩D (τ⇩0 b ⋆⇩D τ⇩0' b)" "𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]"
"(τ⇩0 b ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]"]
D.interchange [of "ε b" "τ⇩0 b ⋆⇩D τ⇩0' b" "τ⇩0 b ⋆⇩D F f ⋆⇩D τ⇩0' a"
"𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]"]
by fastforce
also have "... = (G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b ⋆⇩D τ⇩0' b, τ⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a])"
using a b f ide_f D.hcomp_reassoc(2) [of "ε b" "τ⇩0 b" "F f ⋆⇩D τ⇩0' a"]
by auto
finally show ?thesis by blast
qed
moreover have "τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a
= (τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[τ⇩0 b, τ⇩0' b ⋆⇩D τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a])"
proof -
have "τ⇩0 b ⋆⇩D (η b ⋆⇩D F f) ⋆⇩D τ⇩0' a =
(τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D η b ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a])"
using a b f ide_f D.hcomp_reassoc(1) [of "η b" "F f" "τ⇩0' a"]
D.whisker_left [of "τ⇩0 b"]
by auto
also have "... = (τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[τ⇩0 b, τ⇩0' b ⋆⇩D τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a])"
using a b f ide_f D.hcomp_reassoc(2) [of "τ⇩0 b" "η b" "F f ⋆⇩D τ⇩0' a"]
by auto
finally show ?thesis by blast
qed
ultimately show ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
(((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a] ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0 b ⋆⇩D τ⇩0' b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0 b, τ⇩0' b ⋆⇩D τ⇩0 b, F f ⋆⇩D τ⇩0' a]
= 𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a"
proof -
have "𝖺⇩D⇧-⇧1[τ⇩0 b ⋆⇩D τ⇩0' b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
((τ⇩0 b ⋆⇩D τ⇩0' b) ⋆⇩D 𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, (τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a] ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b ⋆⇩D F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[τ⇩0' b, τ⇩0 b, F f] ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0' b ⋆⇩D τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
𝖺⇩D[τ⇩0 b, τ⇩0' b ⋆⇩D τ⇩0 b, F f ⋆⇩D τ⇩0' a]
= ⦃❙𝖺⇧-⇧1❙[❙⟨τ⇩0 b❙⟩ ❙⋆ ❙⟨τ⇩0' b❙⟩, ❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩❙] ❙⋅
((❙⟨τ⇩0 b❙⟩ ❙⋆ ❙⟨τ⇩0' b❙⟩) ❙⋆ ❙𝖺❙[❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
❙𝖺⇧-⇧1❙[❙⟨τ⇩0 b❙⟩, ❙⟨τ⇩0' b❙⟩, (❙⟨τ⇩0 b❙⟩ ❙⋆ ❙⟨F f❙⟩) ❙⋆ ❙⟨τ⇩0' a❙⟩❙] ❙⋅
(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨τ⇩0 b❙⟩ ❙⋆ ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙𝖺❙[❙⟨τ⇩0' b❙⟩, ❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩❙] ❙⋆ ❙⟨τ⇩0' a❙⟩) ❙⋅
(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙𝖺⇧-⇧1❙[❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
❙𝖺❙[❙⟨τ⇩0 b❙⟩, ❙⟨τ⇩0' b❙⟩ ❙⋆ ❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩❙]⦄"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C
by auto
also have "... = ⦃❙𝖺⇧-⇧1❙[❙⟨τ⇩0 b❙⟩, ❙⟨τ⇩0' b❙⟩, ❙⟨τ⇩0 b❙⟩❙] ❙⋆ ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩⦄"
using a b f ide_f by (intro EV.eval_eqI, auto)
also have "... = 𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C
by auto
finally show ?thesis by blast
qed
thus ?thesis
using D.comp_assoc by auto
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
(G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
((G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
(𝗅⇩D⇧-⇧1[τ⇩0 b] ⋅⇩D 𝗋⇩D[τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a)
= 𝗅⇩D⇧-⇧1[τ⇩0 b] ⋅⇩D 𝗋⇩D[τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a"
proof -
interpret adjoint_equivalence_in_bicategory
V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D ‹τ⇩0 b› ‹τ⇩0' b› ‹η b› ‹ε b›
using b chosen_adjoint_equivalence by simp
have "((ε b ⋆⇩D τ⇩0 b) ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
(𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
((τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a)
= (ε b ⋆⇩D τ⇩0 b) ⋅⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, τ⇩0' b, τ⇩0 b] ⋅⇩D (τ⇩0 b ⋆⇩D η b) ⋆⇩D F f ⋆⇩D τ⇩0' a"
using a b f ide_f D.whisker_right by auto
also have "... = 𝗅⇩D⇧-⇧1[τ⇩0 b] ⋅⇩D 𝗋⇩D[τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a"
using triangle_left by simp
finally show ?thesis by blast
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
((G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
𝗅⇩D⇧-⇧1[(τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
(𝗅⇩D⇧-⇧1[τ⇩0 b] ⋅⇩D 𝗋⇩D[τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]
= 𝗅⇩D⇧-⇧1[(τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a]"
proof -
have "(G⇩0 b ⋆⇩D 𝖺⇩D⇧-⇧1[τ⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(𝖺⇩D[G⇩0 b, τ⇩0 b, F f ⋆⇩D τ⇩0' a] ⋅⇩D
(𝗅⇩D⇧-⇧1[τ⇩0 b] ⋅⇩D 𝗋⇩D[τ⇩0 b] ⋆⇩D F f ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D⇧-⇧1[τ⇩0 b, F⇩0 b, F f ⋆⇩D τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝖺⇩D[F⇩0 b, F f, τ⇩0' a]) ⋅⇩D
(τ⇩0 b ⋆⇩D 𝗅⇩D⇧-⇧1[F f] ⋆⇩D τ⇩0' a) ⋅⇩D
𝖺⇩D[τ⇩0 b, F f, τ⇩0' a]
= ⦃(❙⟨G⇩0 b❙⟩⇩0 ❙⋆ ❙𝖺⇧-⇧1❙[❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
(❙𝖺❙[❙⟨G⇩0 b❙⟩⇩0, ❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩❙] ❙⋅
(❙𝗅⇧-⇧1❙[❙⟨τ⇩0 b❙⟩❙] ❙⋅ ❙𝗋❙[❙⟨τ⇩0 b❙⟩❙] ❙⋆ ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩) ❙⋅
❙𝖺⇧-⇧1❙[❙⟨τ⇩0 b❙⟩, ❙⟨F⇩0 b❙⟩⇩0, ❙⟨F f❙⟩ ❙⋆ ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙𝖺❙[❙⟨F⇩0 b❙⟩⇩0, ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]) ❙⋅
(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙𝗅⇧-⇧1❙[❙⟨F f❙⟩❙] ❙⋆ ❙⟨τ⇩0' a❙⟩) ❙⋅
❙𝖺❙[❙⟨τ⇩0 b❙⟩, ❙⟨F f❙⟩, ❙⟨τ⇩0' a❙⟩❙]⦄"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C D.𝔩_ide_simp D.𝔯_ide_simp
by auto
also have "... = ⦃❙𝗅⇧-⇧1❙[(❙⟨τ⇩0 b❙⟩ ❙⋆ ❙⟨F f❙⟩) ❙⋆ ❙⟨τ⇩0' a❙⟩❙]⦄"
using a b f ide_f by (intro EV.eval_eqI, auto)
also have "... = 𝗅⇩D⇧-⇧1[(τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a]"
using a b f ide_f D.α_def D.α'.map_ide_simp D.VVV.ide_char⇩S⇩b⇩C D.VVV.arr_char⇩S⇩b⇩C
D.VV.ide_char⇩S⇩b⇩C D.VV.arr_char⇩S⇩b⇩C D.𝔩_ide_simp
by auto
finally show ?thesis by blast
qed
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D
𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D
((D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D
(τ⇩1 f ⋆⇩D τ⇩0' a)) ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "(G⇩0 b ⋆⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)) ⋅⇩D
𝗅⇩D⇧-⇧1[(τ⇩0 b ⋆⇩D F f) ⋆⇩D τ⇩0' a]
= 𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D
𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D
(D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"
using a b f ide_f τ.iso_map⇩1_ide
D.lunit'_naturality [of "𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D (D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a)"]
by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D
𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D
𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
proof -
have "((D.inv (τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D (τ⇩1 f ⋆⇩D τ⇩0' a)) ⋅⇩D 𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a] =
((D.inv (τ⇩1 f) ⋅⇩D τ⇩1 f) ⋆⇩D τ⇩0' a) ⋅⇩D 𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
using a b f ide_f τ.iso_map⇩1_ide D.whisker_right [of "τ⇩0' a"] by simp
also have "... = 𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a]"
using a b f ide_f τ.iso_map⇩1_ide D.comp_inv_arr' D.comp_cod_arr by auto
finally show ?thesis
using D.comp_assoc by simp
qed
also have "... = (G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D
(G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D
𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a]"
proof -
have "𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] ⋅⇩D 𝖺⇩D[G f, τ⇩0 a, τ⇩0' a] ⋅⇩D 𝖺⇩D⇧-⇧1[G f, τ⇩0 a, τ⇩0' a] =
𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a]"
using a b f ide_f D.comp_arr_inv' D.comp_arr_dom by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = ((G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D 𝗅⇩D⇧-⇧1[G f ⋆⇩D G⇩0 a]) ⋅⇩D (G f ⋆⇩D ε a)"
proof -
have "(G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D (G⇩0 b ⋆⇩D G f ⋆⇩D ε a) ⋅⇩D 𝗅⇩D⇧-⇧1[G f ⋆⇩D τ⇩0 a ⋆⇩D τ⇩0' a] =
(G⇩0 b ⋆⇩D 𝗋⇩D[G f]) ⋅⇩D 𝗅⇩D⇧-⇧1[G f ⋆⇩D G⇩0 a] ⋅⇩D (G f ⋆⇩D ε a)"
using a b f ide_f D.lunit'_naturality [of "G f ⋆⇩D ε a"] by auto
thus ?thesis
using D.comp_assoc by simp
qed
also have "... = (𝗅⇩D⇧-⇧1[G f] ⋅⇩D 𝗋⇩D[G f]) ⋅⇩D (G f ⋆⇩D ε a)"
using a b f ide_f D.lunit'_naturality [of "𝗋⇩D[G f]"] by auto
finally show "(𝗅⇩D⇧-⇧1[G f] ⋅⇩D 𝗋⇩D[G f]) ⋅⇩D (G f ⋆⇩D ε a) = (ε b ⋆⇩D G f) ⋅⇩D ττ'.map⇩1 f"
by simp
qed
qed
lemma counit_is_invertible_modification:
shows "invertible_modification
V⇩C H⇩C 𝖺⇩C 𝗂⇩C src⇩C trg⇩C V⇩D H⇩D 𝖺⇩D 𝗂⇩D src⇩D trg⇩D G Φ⇩G G Φ⇩G
ττ'.map⇩0 ττ'.map⇩1 ι⇩G.map⇩0 ι⇩G.map⇩1 ε"
..
end
end