Theory Subbicategory
section "Sub-Bicategories"
text ‹
In this section we give a construction of a sub-bicategory in terms of a predicate
on the arrows of an ambient bicategory that has certain closure properties with respect
to that bicategory. While the construction given here is likely to be of general use,
it is not the most general sub-bicategory construction that one could imagine,
because it requires that the sub-bicategory actually contain the unit and associativity
isomorphisms of the ambient bicategory. Our main motivation for including this construction
here is to apply it to exploit the fact that the sub-bicategory of endo-arrows of a fixed
object is a monoidal category, which will enable us to transfer to bicategories a result
about unit isomorphisms in monoidal categories.
›
theory Subbicategory
imports Bicategory
begin
subsection "Construction"
locale subbicategory =
B: bicategory V H 𝖺⇩B 𝗂 src⇩B trg⇩B +
subcategory V Arr
for V :: "'a comp" (infixr ‹⋅⇩B› 55)
and H :: "'a comp" (infixr ‹⋆⇩B› 55)
and 𝖺⇩B :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹𝖺⇩B[_, _, _]›)
and 𝗂 :: "'a ⇒ 'a" (‹𝗂[_]›)
and src⇩B :: "'a ⇒ 'a"
and trg⇩B :: "'a ⇒ 'a"
and Arr :: "'a ⇒ bool" +
assumes src_closed: "Arr f ⟹ Arr (src⇩B f)"
and trg_closed: "Arr f ⟹ Arr (trg⇩B f)"
and hcomp_closed: "⟦ Arr f; Arr g; trg⇩B f = src⇩B g ⟧ ⟹ Arr (g ⋆⇩B f)"
and assoc_closed: "⟦ Arr f ∧ B.ide f; Arr g ∧ B.ide g; Arr h ∧ B.ide h;
src⇩B f = trg⇩B g; src⇩B g = trg⇩B h ⟧ ⟹ Arr (𝖺⇩B f g h)"
and assoc'_closed: "⟦ Arr f ∧ B.ide f; Arr g ∧ B.ide g; Arr h ∧ B.ide h;
src⇩B f = trg⇩B g; src⇩B g = trg⇩B h ⟧ ⟹ Arr (B.inv (𝖺⇩B f g h))"
and lunit_closed: "⟦ Arr f; B.ide f ⟧ ⟹ Arr (B.𝔩 f)"
and lunit'_closed: "⟦ Arr f; B.ide f ⟧ ⟹ Arr (B.inv (B.𝔩 f))"
and runit_closed: "⟦ Arr f; B.ide f ⟧ ⟹ Arr (B.𝔯 f)"
and runit'_closed: "⟦ Arr f; B.ide f ⟧ ⟹ Arr (B.inv (B.𝔯 f))"
begin
notation B.in_hom (‹«_ : _ ⇒⇩B _»›)
notation comp (infixr ‹⋅› 55)
definition hcomp (infixr ‹⋆› 53)
where "g ⋆ f = (if arr f ∧ arr g ∧ trg⇩B f = src⇩B g then g ⋆⇩B f else null)"
definition src
where "src μ = (if arr μ then src⇩B μ else null)"
definition trg
where "trg μ = (if arr μ then trg⇩B μ else null)"
interpretation src: endofunctor ‹(⋅)› src
using src_def null_char inclusion arr_char⇩S⇩b⇩C src_closed trg_closed dom_closed cod_closed
dom_simp cod_simp
apply unfold_locales
apply auto[4]
by (metis B.src.as_nat_trans.preserves_comp_2 comp_char seq_char⇩S⇩b⇩C)
interpretation trg: endofunctor ‹(⋅)› trg
using trg_def null_char inclusion arr_char⇩S⇩b⇩C src_closed trg_closed dom_closed cod_closed
dom_simp cod_simp
apply unfold_locales
apply auto[4]
by (metis B.trg.as_nat_trans.preserves_comp_2 comp_char seq_char⇩S⇩b⇩C)
interpretation horizontal_homs ‹(⋅)› src trg
using src_def trg_def src.preserves_arr trg.preserves_arr null_char ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
inclusion
by (unfold_locales, simp_all)
interpretation "functor" VV.comp ‹(⋅)› ‹λμν. fst μν ⋆ snd μν›
using hcomp_def VV.arr_char⇩S⇩b⇩C src_def trg_def arr_char⇩S⇩b⇩C hcomp_closed dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C
VV.dom_char⇩S⇩b⇩C VV.cod_char⇩S⇩b⇩C
apply unfold_locales
apply auto[2]
proof -
fix f
assume f: "VV.arr f"
show "dom (fst f ⋆ snd f) = fst (VV.dom f) ⋆ snd (VV.dom f)"
proof -
have "dom (fst f ⋆ snd f) = B.dom (fst f) ⋆⇩B B.dom (snd f)"
proof -
have "dom (fst f ⋆ snd f) = B.dom (fst f ⋆ snd f)"
using f dom_char⇩S⇩b⇩C
by (simp add: arr_char⇩S⇩b⇩C hcomp_closed hcomp_def)
also have "... = B.dom (fst f) ⋆⇩B B.dom (snd f)"
using f
by (metis (no_types, lifting) B.hcomp_simps(3) B.hseqI' VV.arrE arrE hcomp_def
inclusion src_def trg_def)
finally show ?thesis by blast
qed
also have "... = fst (VV.dom f) ⋆ snd (VV.dom f)"
using f VV.arr_char⇩S⇩b⇩C VV.dom_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C hcomp_def B.seq_if_composable dom_closed
apply simp
by (metis (no_types, lifting) dom_char⇩S⇩b⇩C)
finally show ?thesis by simp
qed
show "cod (fst f ⋆ snd f) = fst (VV.cod f) ⋆ snd (VV.cod f)"
proof -
have "cod (fst f ⋆ snd f) = B.cod (fst f) ⋆⇩B B.cod (snd f)"
using f VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C hcomp_def src_def trg_def
src_closed trg_closed hcomp_closed inclusion B.hseq_char arrE
by auto
also have "... = fst (VV.cod f) ⋆ snd (VV.cod f)"
using f VV.arr_char⇩S⇩b⇩C VV.cod_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C hcomp_def B.seq_if_composable cod_closed
apply simp
by (metis (no_types, lifting) cod_char⇩S⇩b⇩C)
finally show ?thesis by simp
qed
next
fix f g
assume fg: "VV.seq g f"
show "fst (VV.comp g f) ⋆ snd (VV.comp g f) = (fst g ⋆ snd g) ⋅ (fst f ⋆ snd f)"
proof -
have "fst (VV.comp g f) ⋆ snd (VV.comp g f) = fst g ⋅ fst f ⋆ snd g ⋅ snd f"
using fg VV.seq_char⇩S⇩b⇩C VV.comp_char VxV.comp_char VxV.not_Arr_Null
by (metis (no_types, lifting) VxV.seqE⇩P⇩C prod.sel(1-2))
also have "... = (fst g ⋅⇩B fst f) ⋆⇩B (snd g ⋅⇩B snd f)"
using fg comp_char hcomp_def VV.seq_char⇩S⇩b⇩C inclusion arr_char⇩S⇩b⇩C seq_char⇩S⇩b⇩C B.hseq_char
by (metis (no_types, lifting) B.hseq_char' VxV.seq_char null_char)
also have 1: "... = (fst g ⋆⇩B snd g) ⋅⇩B (fst f ⋆⇩B snd f)"
proof -
have "src⇩B (fst g) = trg⇩B (snd g)"
by (metis (no_types, lifting) VV.arrE VV.seq_char⇩S⇩b⇩C fg src_def trg_def)
thus ?thesis
using fg VV.seq_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C seq_char⇩S⇩b⇩C inclusion B.interchange
by (meson VxV.seqE⇩P⇩C)
qed
also have "... = (fst g ⋆ snd g) ⋅ (fst f ⋆ snd f)"
using fg comp_char hcomp_def VV.seq_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C seq_char⇩S⇩b⇩C inclusion
B.hseq_char' hcomp_closed src_def trg_def
by (metis (no_types, lifting) 1)
finally show ?thesis by auto
qed
qed
interpretation horizontal_composition ‹(⋅)› ‹(⋆)› src trg
using arr_char⇩S⇩b⇩C src_def trg_def src_closed trg_closed
apply (unfold_locales)
using hcomp_def inclusion not_arr_null by auto
abbreviation 𝖺
where "𝖺 μ ν τ ≡ if VVV.arr (μ, ν, τ) then 𝖺⇩B μ ν τ else null"
abbreviation (input) α⇩S⇩B
where "α⇩S⇩B μντ ≡ 𝖺 (fst μντ) (fst (snd μντ)) (snd (snd μντ))"
lemma assoc_closed':
assumes "VVV.arr μντ"
shows "Arr (α⇩S⇩B μντ)"
proof -
have 1: "B.VVV.arr μντ"
using assms VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
src_def trg_def inclusion
by auto
show "Arr (α⇩S⇩B μντ)"
proof -
have "Arr (α⇩S⇩B μντ) =
Arr ((fst μντ ⋆⇩B fst (snd μντ) ⋆⇩B snd (snd μντ)) ⋅⇩B α⇩S⇩B (B.VVV.dom μντ))"
using assms 1 B.α_def B.assoc_naturality1 [of "fst μντ" "fst (snd μντ)" "snd (snd μντ)"]
VV.arr_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VVV.dom_char⇩S⇩b⇩C B.VV.dom_char⇩S⇩b⇩C
apply simp
by (metis (no_types, lifting) arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C dom_closed src.preserves_dom
trg.preserves_dom)
also have "..."
proof (intro comp_closed)
show "Arr (fst μντ ⋆⇩B fst (snd μντ) ⋆⇩B snd (snd μντ))"
using assms 1 B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C hcomp_closed
by (metis (no_types, lifting) B.H.preserves_reflects_arr B.trg_hcomp
VV.arr_char⇩S⇩b⇩C VVV.arrE arr_char⇩S⇩b⇩C)
show "B.cod (𝖺 (fst (B.VVV.dom μντ)) (fst (snd (B.VVV.dom μντ)))
(snd (snd (B.VVV.dom μντ)))) =
B.dom (fst μντ ⋆⇩B fst (snd μντ) ⋆⇩B snd (snd μντ))"
using assms 1 VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VxVxV.dom_char
B.VVV.dom_simp B.VVV.cod_simp
apply simp
by (metis (no_types, lifting) B.VV.arr_char⇩S⇩b⇩C B.VVV.arrE B.α.preserves_reflects_arr
B.assoc_naturality1 B.seqE arr_dom dom_char⇩S⇩b⇩C src_dom trg_dom)
show "Arr (𝖺 (fst (B.VVV.dom μντ)) (fst (snd (B.VVV.dom μντ)))
(snd (snd (B.VVV.dom μντ))))"
proof -
have "VVV.arr (B.VVV.dom μντ)"
using 1 B.VVV.dom_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
apply simp
by (metis (no_types, lifting) VVV.arrE arr_dom assms dom_simp src_dom trg_dom)
moreover have "Arr (𝖺⇩B (B.dom (fst μντ)) (B.dom (fst (snd μντ)))
(B.dom (snd (snd μντ))))"
proof -
have "B.VVV.ide (B.VVV.dom μντ)"
using 1 B.VVV.ide_dom by blast
thus ?thesis
using assms B.α_def B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C B.VVV.ide_char B.VV.ide_char
dom_closed assoc_closed
by (metis (no_types, lifting) "1" B.ide_dom B.src_dom B.trg_dom VV.arr_char⇩S⇩b⇩C
VVV.arrE arr_char⇩S⇩b⇩C)
qed
ultimately show ?thesis
using 1 B.VVV.ide_dom assoc_closed B.VVV.dom_char⇩S⇩b⇩C
apply simp
by (metis (no_types, lifting) B.VV.arr_char⇩S⇩b⇩C B.VVV.arrE B.VVV.inclusion
B.VxV.dom_char B.VxVxV.arrE B.VxVxV.dom_char prod.sel(1) prod.sel(2))
qed
qed
finally show ?thesis by blast
qed
qed
lemma lunit_closed':
assumes "Arr f"
shows "Arr (B.𝔩 f)"
proof -
have 1: "arr f ∧ arr (B.𝔩 (B.dom f))"
using assms arr_char⇩S⇩b⇩C lunit_closed dom_closed B.ide_dom inclusion by simp
moreover have "B.dom f = B.cod (B.𝔩 (B.dom f))"
using 1 arr_char⇩S⇩b⇩C B.𝔩.preserves_cod inclusion by simp
moreover have "B.𝔩 f = f ⋅ B.𝔩 (B.dom f)"
using assms 1 B.𝔩.naturality1 inclusion comp_char arr_char⇩S⇩b⇩C by simp
ultimately show ?thesis
using arr_char⇩S⇩b⇩C comp_closed cod_char⇩S⇩b⇩C seqI dom_simp by auto
qed
lemma runit_closed':
assumes "Arr f"
shows "Arr (B.𝔯 f)"
proof -
have 1: "arr f ∧ arr (B.𝔯 (B.dom f))"
using assms arr_char⇩S⇩b⇩C runit_closed dom_closed B.ide_dom inclusion
by simp
moreover have "B.dom f = B.cod (B.𝔯 (B.dom f))"
using 1 arr_char⇩S⇩b⇩C B.𝔩.preserves_cod inclusion by simp
moreover have "B.𝔯 f = f ⋅ B.𝔯 (B.dom f)"
using assms 1 B.𝔯.naturality1 inclusion comp_char arr_char⇩S⇩b⇩C by simp
ultimately show ?thesis
using arr_char⇩S⇩b⇩C comp_closed cod_char⇩S⇩b⇩C seqI dom_simp by auto
qed
interpretation natural_isomorphism VVV.comp ‹(⋅)› HoHV HoVH α⇩S⇩B
proof
fix μντ
show "¬ VVV.arr μντ ⟹ α⇩S⇩B μντ = null"
by simp
assume μντ: "VVV.arr μντ"
have 1: "B.VVV.arr μντ"
using μντ VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
src_def trg_def inclusion
by auto
show "arr (α⇩S⇩B μντ)"
using μντ assoc_closed' by blast
have 3: "Arr (fst μντ) ∧ Arr (fst (snd μντ)) ∧ Arr (snd (snd μντ)) ∧
src⇩B (fst μντ) = trg⇩B (fst (snd μντ)) ∧
src⇩B (fst (snd μντ)) = trg⇩B (snd (snd μντ))"
using μντ VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def arr_char⇩S⇩b⇩C by auto
show "HoVH μντ ⋅ α⇩S⇩B (VVV.dom μντ) = α⇩S⇩B μντ"
proof -
have "α⇩S⇩B μντ = (fst μντ ⋆⇩B fst (snd μντ) ⋆⇩B snd (snd μντ)) ⋅⇩B
𝖺⇩B (B.dom (fst μντ)) (B.dom (fst (snd μντ))) (B.dom (snd (snd μντ)))"
using 3 inclusion B.assoc_naturality1 [of "fst μντ" "fst (snd μντ)" "snd (snd μντ)"]
by (simp add: μντ)
also have "... = (fst μντ ⋆ fst (snd μντ) ⋆ snd (snd μντ)) ⋅
𝖺⇩B (dom (fst μντ)) (dom (fst (snd μντ))) (dom (snd (snd μντ)))"
using 1 3 μντ hcomp_closed assoc_closed dom_closed hcomp_def comp_def inclusion
comp_char dom_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
apply simp
using B.hcomp_simps(2-3) arr_char⇩S⇩b⇩C by presburger
also have "... = HoVH μντ ⋅ α⇩S⇩B (VVV.dom μντ)"
using μντ B.α_def HoVH_def VVV.dom_char⇩S⇩b⇩C VV.dom_char⇩S⇩b⇩C VxVxV.dom_char
apply simp
by (metis (no_types, lifting) VV.arr_char⇩S⇩b⇩C VVV.arrE VVV.arr_dom VxV.dom_char
dom_simp)
finally show ?thesis by argo
qed
show "α⇩S⇩B (VVV.cod μντ) ⋅ HoHV μντ = α⇩S⇩B μντ"
proof -
have "α⇩S⇩B μντ =
𝖺⇩B (B.cod (fst μντ)) (B.cod (fst (snd μντ))) (B.cod (snd (snd μντ))) ⋅⇩B
(fst μντ ⋆⇩B fst (snd μντ)) ⋆⇩B snd (snd μντ)"
using 3 inclusion B.assoc_naturality2 [of "fst μντ" "fst (snd μντ)" "snd (snd μντ)"]
by (simp add: μντ)
also have "... = 𝖺⇩B (cod (fst μντ)) (cod (fst (snd μντ))) (cod (snd (snd μντ))) ⋅
((fst μντ ⋆ fst (snd μντ)) ⋆ snd (snd μντ))"
by (simp add: "3" arrI⇩S⇩b⇩C assoc_closed cod_char⇩S⇩b⇩C cod_closed hcomp_closed hcomp_def
inclusion comp_def)
also have "... = α⇩S⇩B (VVV.cod μντ) ⋅ HoHV μντ"
using μντ B.α_def HoHV_def VVV.cod_char⇩S⇩b⇩C VV.cod_char⇩S⇩b⇩C VxVxV.cod_char
VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C arr_cod src_cod trg_cod
by simp
finally show ?thesis by argo
qed
next
fix fgh
assume fgh: "VVV.ide fgh"
show "iso (α⇩S⇩B fgh)"
proof -
have 1: "B.arr (fst (snd fgh)) ∧ B.arr (snd (snd fgh)) ∧
src⇩B (fst (snd fgh)) = trg⇩B (snd (snd fgh)) ∧
src⇩B (fst fgh) = trg⇩B (fst (snd fgh))"
using fgh VVV.ide_char VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def
arr_char⇩S⇩b⇩C inclusion
by auto
have 2: "B.ide (fst fgh) ∧ B.ide (fst (snd fgh)) ∧ B.ide (snd (snd fgh))"
using fgh VVV.ide_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C by blast
have "α⇩S⇩B fgh = 𝖺⇩B (fst fgh) (fst (snd fgh)) (snd (snd fgh))"
using fgh B.α_def by simp
moreover have "B.VVV.ide fgh"
using fgh 1 2 VVV.ide_char B.VVV.ide_char⇩S⇩b⇩C VVV.arr_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C
src_def trg_def inclusion arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
by simp
moreover have "Arr (𝖺⇩B (fst fgh) (fst (snd fgh)) (snd (snd fgh)))"
using fgh 1 VVV.ide_char VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def
arr_char⇩S⇩b⇩C assoc_closed' B.α_def
by simp
moreover have "Arr (B.inv (𝖺⇩B (fst fgh) (fst (snd fgh)) (snd (snd fgh))))"
using fgh 1 VVV.ide_char VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def
arr_char⇩S⇩b⇩C assoc'_closed
by (simp add: VVV.arr_char⇩S⇩b⇩C "2" B.VVV.ide_char calculation(2))
ultimately show ?thesis
using fgh iso_char⇩S⇩b⇩C B.α.components_are_iso by auto
qed
qed
interpretation L: endofunctor ‹(⋅)› L
using endofunctor_L by auto
interpretation R: endofunctor ‹(⋅)› R
using endofunctor_R by auto
interpretation L: faithful_functor ‹(⋅)› ‹(⋅)› L
proof
fix f f'
assume par: "par f f'"
assume eq: "L f = L f'"
have "B.par f f'"
using par inclusion arr_char⇩S⇩b⇩C dom_simp cod_simp by fastforce
moreover have "B.L f = B.L f'"
proof -
have "∀a. Arr a ⟶ B.arr a"
by (simp add: inclusion)
moreover have 1: "∀a. arr a ⟶ (if arr a then hseq (trg a) a else arr null)"
using L.preserves_arr by presburger
moreover have "Arr f ∧ Arr (trg f) ∧ trg⇩B f = src⇩B (trg f)"
by (simp add: ‹B.par f f'› arrE par trg_closed trg_def)
ultimately show ?thesis
by (metis ‹B.par f f'› eq hcomp_def hseq_char' par trg_def)
qed
ultimately show "f = f'"
using B.L.is_faithful by blast
qed
interpretation L: full_functor ‹(⋅)› ‹(⋅)› L
proof
fix f f' ν
assume f: "ide f" and f': "ide f'" and ν: "«ν : L f ⇒ L f'»"
have 1: "L f = trg⇩B f ⋆⇩B f ∧ L f' = trg⇩B f' ⋆⇩B f'"
using f f' hcomp_def trg_def arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C trg_closed by simp
have 2: "«ν : trg⇩B f ⋆⇩B f ⇒⇩B trg⇩B f' ⋆⇩B f'»"
using 1 f f' ν hcomp_def trg_def src_def inclusion
dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C hseq_char' arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C trg_closed null_char
by (simp add: arr_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C)
show "∃μ. «μ : f ⇒ f'» ∧ L μ = ν"
proof -
let ?μ = "B.𝔩 f' ⋅⇩B ν ⋅⇩B B.inv (B.𝔩 f)"
have μ: "«?μ : f ⇒ f'» ∧ «?μ : f ⇒⇩B f'»"
proof -
have "«?μ : f ⇒⇩B f'»"
using f f' ν 2 B.𝔩_ide_simp lunit'_closed lunit_closed' ide_char⇩S⇩b⇩C by auto
thus ?thesis
using f f' ν in_hom_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C comp_closed ide_char⇩S⇩b⇩C
lunit'_closed lunit_closed
by (metis (no_types, lifting) B.arrI B.seqE in_homE)
qed
have μ_eq: "?μ = B.𝔩 f' ⋅ ν ⋅ B.inv (B.𝔩 f)"
proof -
have "?μ = B.𝔩 f' ⋅ ν ⋅⇩B B.inv (B.𝔩 f)"
by (metis (no_types, lifting) B.arrI B.seqE μ ν arrE comp_closed f f'
ide_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C comp_def lunit'_closed lunit_closed)
also have "... = B.𝔩 f' ⋅ ν ⋅ B.inv (B.𝔩 f)"
using f f' ν μ arr_char⇩S⇩b⇩C inclusion comp_char comp_closed ide_char⇩S⇩b⇩C
lunit'_closed lunit_closed
by (metis (no_types, lifting) B.seqE in_homE)
finally show ?thesis by simp
qed
have "L ?μ = ν"
proof -
have "L ?μ = trg⇩B ?μ ⋆⇩B ?μ"
using μ μ_eq hcomp_def trg_def inclusion arr_char⇩S⇩b⇩C trg_closed by auto
also have "... = (trg⇩B ?μ ⋆⇩B ?μ) ⋅⇩B (B.inv (B.𝔩 f) ⋅⇩B B.𝔩 f)"
proof -
have "B.inv (B.𝔩 f) ⋅⇩B B.𝔩 f = trg⇩B f ⋆⇩B f"
using f ide_char⇩S⇩b⇩C B.comp_inv_arr B.inv_is_inverse by auto
moreover have "B.dom (trg⇩B ?μ ⋆⇩B ?μ) = trg⇩B f ⋆⇩B f"
proof -
have "B.dom (trg⇩B ?μ) = trg⇩B f"
using f μ B.vconn_implies_hpar(2) by force
moreover have "B.dom ?μ = f"
using μ by blast
ultimately show ?thesis
using B.hcomp_simps [of "trg⇩B ?μ" ?μ]
by (metis (no_types, lifting) B.hseqI' B.ideD(1) B.src_trg
B.trg.preserves_reflects_arr B.trg_dom f ide_char⇩S⇩b⇩C)
qed
ultimately show ?thesis
using μ μ_eq B.comp_arr_dom in_hom_char⇩S⇩b⇩C by auto
qed
also have "... = ((trg⇩B ?μ ⋆⇩B ?μ) ⋅⇩B B.inv (B.𝔩 f)) ⋅⇩B B.𝔩 f"
using B.comp_assoc by simp
also have "... = (B.inv (B.𝔩 f') ⋅⇩B ?μ) ⋅⇩B B.𝔩 f"
using μ μ_eq B.𝔩'.naturality [of ?μ] by auto
also have "... = (B.inv (B.𝔩 f') ⋅⇩B B.𝔩 f') ⋅⇩B ν ⋅⇩B (B.inv (B.𝔩 f) ⋅⇩B B.𝔩 f)"
using μ μ_eq arr_char⇩S⇩b⇩C arrI comp_simp B.comp_assoc by metis
also have "... = ν"
using f f' ν 2 B.comp_arr_dom B.comp_cod_arr ide_char⇩S⇩b⇩C
B.𝔩.components_are_iso B.𝔩_ide_simp B.comp_inv_arr'
by auto
finally show ?thesis by blast
qed
thus ?thesis
using μ by auto
qed
qed
interpretation R: faithful_functor ‹(⋅)› ‹(⋅)› R
proof
fix f f'
assume par: "par f f'"
assume eq: "R f = R f'"
have "B.par f f'"
using par inclusion arr_char⇩S⇩b⇩C dom_simp cod_simp by fastforce
moreover have "B.R f = B.R f'"
proof -
have "∀a. Arr a ⟶ B.arr a"
by (simp add: inclusion)
moreover have 1: "∀a. arr a ⟶ (if arr a then hseq a (src a) else arr null)"
using R.preserves_arr by presburger
moreover have "arr f ∧ arr (src f) ∧ trg⇩B (src f) = src⇩B f"
by (meson 1 hcomp_def hseq_char' par)
ultimately show ?thesis
by (metis ‹B.par f f'› eq hcomp_def hseq_char' src_def)
qed
ultimately show "f = f'"
using B.R.is_faithful by blast
qed
interpretation R: full_functor ‹(⋅)› ‹(⋅)› R
proof
fix f f' ν
assume f: "ide f" and f': "ide f'" and ν: "«ν : R f ⇒ R f'»"
have 1: "R f = f ⋆⇩B src⇩B f ∧ R f' = f' ⋆⇩B src⇩B f'"
using f f' hcomp_def src_def arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C src_closed by simp
have 2: "«ν : f ⋆⇩B src⇩B f ⇒⇩B f' ⋆⇩B src⇩B f'»"
using 1 f f' ν hcomp_def trg_def src_def inclusion
dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C hseq_char' arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C trg_closed null_char
by (simp add: arr_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C)
show "∃μ. «μ : f ⇒ f'» ∧ R μ = ν"
proof -
let ?μ = "B.𝔯 f' ⋅⇩B ν ⋅⇩B B.inv (B.𝔯 f)"
have μ: "«?μ : f ⇒ f'» ∧ «?μ : f ⇒⇩B f'»"
proof -
have "«?μ : f ⇒⇩B f'»"
using f f' ν 2 B.𝔯_ide_simp runit'_closed runit_closed' ide_char⇩S⇩b⇩C by auto
thus ?thesis
by (metis (no_types, lifting) B.arrI B.seqE ν arrE arrI⇩S⇩b⇩C comp_closed f f'
ide_char⇩S⇩b⇩C in_hom_char⇩S⇩b⇩C runit'_closed runit_closed')
qed
have μ_eq: "?μ = B.𝔯 f' ⋅ ν ⋅ B.inv (B.𝔯 f)"
proof -
have "?μ = B.𝔯 f' ⋅ ν ⋅⇩B B.inv (B.𝔯 f)"
using f f' ν μ arr_char⇩S⇩b⇩C inclusion comp_char comp_closed ide_char⇩S⇩b⇩C
runit'_closed runit_closed
by (metis (no_types, lifting) B.seqE in_homE)
also have "... = B.𝔯 f' ⋅ ν ⋅ B.inv (B.𝔯 f)"
using f f' ν μ arr_char⇩S⇩b⇩C inclusion comp_char comp_closed ide_char⇩S⇩b⇩C
runit'_closed runit_closed
by (metis (no_types, lifting) B.arrI B.comp_in_homE in_hom_char⇩S⇩b⇩C)
finally show ?thesis by simp
qed
have "R ?μ = ν"
proof -
have "R ?μ = ?μ ⋆⇩B src⇩B ?μ"
using μ μ_eq hcomp_def src_def inclusion arr_char⇩S⇩b⇩C src_closed by auto
also have "... = (?μ ⋆⇩B src⇩B ?μ) ⋅⇩B (B.inv (B.𝔯 f) ⋅⇩B B.𝔯 f)"
proof -
have "B.inv (B.𝔯 f) ⋅⇩B B.𝔯 f = f ⋆⇩B src⇩B f"
using f ide_char⇩S⇩b⇩C B.comp_inv_arr B.inv_is_inverse by auto
moreover have "B.dom (?μ ⋆⇩B src⇩B ?μ) = f ⋆⇩B src⇩B f"
using f μ μ_eq ide_char arr_char⇩S⇩b⇩C B.src_dom [of ?μ]
by (metis (no_types, lifting) B.R.as_nat_trans.preserves_comp_2 B.R.preserves_seq
B.dom_src B.hcomp_simps(3) B.in_homE)
ultimately show ?thesis
using μ μ_eq B.comp_arr_dom in_hom_char⇩S⇩b⇩C by auto
qed
also have "... = ((?μ ⋆⇩B src⇩B ?μ) ⋅⇩B B.inv (B.𝔯 f)) ⋅⇩B B.𝔯 f"
using B.comp_assoc by simp
also have "... = (B.inv (B.𝔯 f') ⋅⇩B ?μ) ⋅⇩B B.𝔯 f"
using μ μ_eq B.𝔯'.naturality [of ?μ] by auto
also have "... = (B.inv (B.𝔯 f') ⋅⇩B B.𝔯 f') ⋅⇩B ν ⋅⇩B (B.inv (B.𝔯 f) ⋅⇩B B.𝔯 f)"
using μ μ_eq arr_char⇩S⇩b⇩C arrI comp_simp B.comp_assoc by metis
also have "... = ν"
using f f' ν 2 B.comp_arr_dom B.comp_cod_arr ide_char⇩S⇩b⇩C
B.𝔩.components_are_iso B.𝔩_ide_simp B.comp_inv_arr'
by auto
finally show ?thesis by blast
qed
thus ?thesis
using μ by blast
qed
qed
interpretation bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg
proof
show "⋀a. obj a ⟹ «𝗂[a] : a ⋆ a ⇒ a»"
proof (intro in_homI)
fix a
assume a: "obj a"
have 1: "Arr (𝗂 a)"
using a obj_def src_def trg_def in_hom_char⇩S⇩b⇩C B.unit_in_hom
arr_char⇩S⇩b⇩C hcomp_def B.obj_def ide_char⇩S⇩b⇩C objE hcomp_closed
by (metis (no_types, lifting) B.𝔩_ide_simp B.unitor_coincidence(1) inclusion lunit_closed)
show 2: "arr 𝗂[a]"
using 1 arr_char⇩S⇩b⇩C by simp
show "dom 𝗂[a] = a ⋆ a"
using a 2 dom_char⇩S⇩b⇩C
by (metis (full_types) B.objI_trg B.unit_simps(4) R.preserves_reflects_arr
hcomp_def hseq_char' inclusion objE obj_simps(1)
subcategory.arrE subcategory_axioms trg_def)
show "cod 𝗂[a] = a"
using a 2 cod_char⇩S⇩b⇩C
by (metis B.obj_def' B.unit_simps(5) inclusion objE obj_simps(1)
subcategory.arrE subcategory_axioms trg_def)
qed
show "⋀a. obj a ⟹ iso (𝗂 a)"
proof -
fix a
assume a: "obj a"
have 1: "trg⇩B a = src⇩B a"
using a obj_def src_def trg_def B.obj_def arr_char⇩S⇩b⇩C
by (metis horizontal_homs.objE horizontal_homs_axioms)
have 2: "Arr (𝗂 a)"
using a 1 obj_def src_def trg_def in_hom_char⇩S⇩b⇩C B.unit_in_hom
arr_char⇩S⇩b⇩C hcomp_def B.obj_def ide_char⇩S⇩b⇩C objE hcomp_closed
by (metis (no_types, lifting) B.𝔩_ide_simp B.unitor_coincidence(1) inclusion lunit_closed)
have "iso (B.𝔩 a)"
using a 2 obj_def B.iso_unit iso_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C lunit_closed lunit'_closed B.iso_lunit
apply simp
by (metis (no_types, lifting) B.𝔩.components_are_iso B.ide_src inclusion src_def)
thus "iso (𝗂 a)"
using a 2 obj_def B.iso_unit iso_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C B.unitor_coincidence
apply simp
by (metis (no_types, lifting) B.𝔩_ide_simp B.ide_src B.obj_src inclusion src_def)
qed
show "⋀f g h k. ⟦ ide f; ide g; ide h; ide k;
src f = trg g; src g = trg h; src h = trg k ⟧ ⟹
(f ⋆ 𝖺 g h k) ⋅ 𝖺 f (g ⋆ h) k ⋅ (𝖺 f g h ⋆ k) =
𝖺 f g (h ⋆ k) ⋅ 𝖺 (f ⋆ g) h k"
using B.pentagon VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C hcomp_def assoc_closed arr_char⇩S⇩b⇩C comp_char
hcomp_closed comp_closed ide_char⇩S⇩b⇩C inclusion src_def trg_def
by simp
qed
proposition is_bicategory:
shows "bicategory (⋅) (⋆) 𝖺 𝗂 src trg"
..
lemma obj_char:
shows "obj a ⟷ arr a ∧ B.obj a"
proof
assume a: "obj a"
show "arr a ∧ B.obj a"
using a obj_def B.obj_def src_def arr_char⇩S⇩b⇩C inclusion by metis
next
assume a: "arr a ∧ B.obj a"
have "src a = a"
using a src_def by auto
thus "obj a"
using a obj_def by simp
qed
lemma hcomp_char:
shows "hcomp = (λf g. if arr f ∧ arr g ∧ src f = trg g then f ⋆⇩B g else null)"
using hcomp_def src_def trg_def by metis
lemma assoc_simp:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "𝖺 f g h = 𝖺⇩B f g h"
using assms VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C by auto
lemma assoc'_simp:
assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
shows "𝖺' f g h = B.𝖺' f g h"
proof -
have "𝖺' f g h = B.inv (𝖺⇩B f g h)"
using assms inv_char⇩S⇩b⇩C by fastforce
also have "... = B.𝖺' f g h"
using assms ide_char⇩S⇩b⇩C src_def trg_def
B.VVV.ide_char⇩S⇩b⇩C B.VVV.arr_char⇩S⇩b⇩C B.VV.arr_char⇩S⇩b⇩C
by force
finally show ?thesis by blast
qed
lemma lunit_simp:
assumes "ide f"
shows "lunit f = B.lunit f"
proof -
have "B.lunit f = lunit f"
proof (intro lunit_eqI)
show "ide f" by fact
show 1: "«B.lunit f : trg f ⋆ f ⇒ f»"
proof
show 2: "arr (B.lunit f)"
using assms arr_char⇩S⇩b⇩C lunit_closed
by (simp add: arr_char⇩S⇩b⇩C B.𝔩_ide_simp ide_char⇩S⇩b⇩C)
show "dom (B.lunit f) = trg f ⋆ f"
using assms 2 dom_char⇩S⇩b⇩C hcomp_char ide_char⇩S⇩b⇩C src_trg trg.preserves_arr trg_def
by auto
show "cod (B.lunit f) = f"
using assms 2 in_hom_char⇩S⇩b⇩C
by (simp add: cod_simp ide_char⇩S⇩b⇩C)
qed
show "trg f ⋆ B.lunit f = (𝗂[trg f] ⋆ f) ⋅ 𝖺' (trg f) (trg f) f"
proof -
have "trg f ⋆ B.lunit f = trg⇩B f ⋆⇩B B.lunit f"
using assms 1 arr_char⇩S⇩b⇩C hcomp_char
by (metis (no_types, lifting) ideD(1) src_trg trg.preserves_reflects_arr
trg_def vconn_implies_hpar(2,4))
also have "... = (𝗂[trg f] ⋆⇩B f) ⋅⇩B B.𝖺' (trg f) (trg f) f"
using assms ide_char⇩S⇩b⇩C B.lunit_char(2) trg_def by simp
also have "... = (𝗂[trg f] ⋆⇩B f) ⋅⇩B 𝖺' (trg f) (trg f) f"
using assms assoc'_simp [of "trg f" "trg f" f] by simp
also have "... = (𝗂[trg f] ⋆ f) ⋅⇩B 𝖺' (trg f) (trg f) f"
using assms hcomp_char by simp
also have "... = (𝗂[trg f] ⋆ f) ⋅ 𝖺' (trg f) (trg f) f"
using assms seq_char⇩S⇩b⇩C [of "𝗂[trg f] ⋆ f" "𝖺' (trg f) (trg f) f"]
comp_char [of "𝗂[trg f] ⋆ f" "𝖺' (trg f) (trg f) f"]
by simp
finally show ?thesis by blast
qed
qed
thus ?thesis by simp
qed
lemma lunit'_simp:
assumes "ide f"
shows "lunit' f = B.lunit' f"
using assms inv_char⇩S⇩b⇩C [of "lunit f"] lunit_simp by fastforce
lemma runit_simp:
assumes "ide f"
shows "runit f = B.runit f"
proof -
have "B.runit f = runit f"
proof (intro runit_eqI)
show "ide f" by fact
show 1: "«B.runit f : f ⋆ src f ⇒ f»"
proof
show 2: "arr (B.runit f)"
using assms arr_char⇩S⇩b⇩C runit_closed
by (simp add: arr_char⇩S⇩b⇩C B.𝔯_ide_simp ide_char⇩S⇩b⇩C)
show "dom (B.runit f) = f ⋆ src f"
using assms 2 dom_char⇩S⇩b⇩C hcomp_char
by (metis (no_types, lifting) B.runit_simps(4) ide_char⇩S⇩b⇩C src.preserves_reflects_arr
src_def trg_src)
show "cod (B.runit f) = f"
using assms 2 in_hom_char⇩S⇩b⇩C
by (simp add: cod_simp ide_char⇩S⇩b⇩C)
qed
show "B.runit f ⋆ src f = (f ⋆ 𝗂[src f]) ⋅ 𝖺 f (src f) (src f)"
proof -
have "B.runit f ⋆ src f = B.runit f ⋆⇩B src⇩B f"
using assms 1 arr_char⇩S⇩b⇩C hcomp_char
by (metis (no_types, lifting) ideD(1) src.preserves_reflects_arr src_def
trg_src vconn_implies_hpar(1,3))
also have "... = (f ⋆⇩B 𝗂[src f]) ⋅⇩B 𝖺⇩B f (src f) (src f)"
using assms ide_char⇩S⇩b⇩C B.runit_char(2) src_def by simp
also have "... = (f ⋆⇩B 𝗂[src f]) ⋅⇩B 𝖺 f (src f) (src f)"
using assms assoc_simp by simp
also have "... = (f ⋆ 𝗂[src f]) ⋅⇩B 𝖺 f (src f) (src f)"
using assms 1 hcomp_char by simp
also have "... = (f ⋆ 𝗂[src f]) ⋅ 𝖺 f (src f) (src f)"
proof -
have "B.seq (f ⋆ 𝗂[src f]) (𝖺 f (src f) (src f))"
using assms seq_char⇩S⇩b⇩C [of "f ⋆ 𝗂[src f]" "𝖺 f (src f) (src f)"] by simp
thus ?thesis
using assms comp_char [of "f ⋆ 𝗂[src f]" "𝖺 f (src f) (src f)"] by simp
qed
finally show ?thesis by blast
qed
qed
thus ?thesis by simp
qed
lemma runit'_simp:
assumes "ide f"
shows "runit' f = B.runit' f"
using assms inv_char⇩S⇩b⇩C [of "runit f"] runit_simp by fastforce
lemma comp_eqI [intro]:
assumes "seq f g" and "f = f'" and "g = g'"
shows "f ⋅ g = f' ⋅⇩B g'"
using assms comp_char ext ext not_arr_null by auto
lemma comp_eqI' [intro]:
assumes "seq f g" and "f = f'" and "g = g'"
shows "f ⋅⇩B g = f' ⋅ g'"
using assms comp_char ext ext not_arr_null by auto
lemma hcomp_eqI [intro]:
assumes "hseq f g" and "f = f'" and "g = g'"
shows "f ⋆ g = f' ⋆⇩B g'"
using assms hcomp_char not_arr_null by auto
lemma hcomp_eqI' [intro]:
assumes "hseq f g" and "f = f'" and "g = g'"
shows "f ⋆⇩B g = f' ⋆ g'"
using assms hcomp_char not_arr_null by auto
lemma arr_compI:
assumes "seq f g"
shows "arr (f ⋅⇩B g)"
using assms seq_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C
by (metis (no_types, lifting) comp_simp)
lemma arr_hcompI:
assumes "hseq f g"
shows "arr (f ⋆⇩B g)"
using assms hseq_char src_def trg_def hcomp_eqI' by auto
end
sublocale subbicategory ⊆ bicategory ‹(⋅)› ‹(⋆)› 𝖺 𝗂 src trg
using is_bicategory by auto
subsection "The Sub-bicategory of Endo-arrows of an Object"
text ‹
We now consider the sub-bicategory consisting of all arrows having the same
object ‹a› both as their source and their target and we show that the resulting structure
is a monoidal category. We actually prove a slightly more general result,
in which the unit of the monoidal category is taken to be an arbitrary isomorphism
‹«ω : w ⋆⇩B w ⇒ w»› with ‹w› isomorphic to ‹a›, rather than the particular choice
‹«𝗂[a] : a ⋆⇩B a ⇒ a»› made by the ambient bicategory.
›
locale subbicategory_at_object =
B: bicategory V H 𝖺⇩B 𝗂 src⇩B trg⇩B +
subbicategory V H 𝖺⇩B 𝗂 src⇩B trg⇩B ‹λμ. B.arr μ ∧ src⇩B μ = a ∧ trg⇩B μ = a›
for V :: "'a comp" (infixr ‹⋅⇩B› 55)
and H :: "'a comp" (infixr ‹⋆⇩B› 55)
and 𝖺⇩B :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (‹𝖺⇩B[_, _, _]›)
and 𝗂 :: "'a ⇒ 'a" (‹𝗂[_]›)
and src⇩B :: "'a ⇒ 'a"
and trg⇩B :: "'a ⇒ 'a"
and a :: "'a"
and w :: "'a"
and ω :: "'a" +
assumes obj_a: "B.obj a"
and isomorphic_a_w: "B.isomorphic a w"
and ω_in_vhom: "«ω : w ⋆⇩B w ⇒ w»"
and ω_is_iso: "B.iso ω"
begin
notation hcomp (infixr ‹⋆› 53)
lemma arr_simps:
assumes "arr μ"
shows "src μ = a" and "trg μ = a"
apply (metis (no_types, lifting) arrE assms src_def)
by (metis (no_types, lifting) arrE assms trg_def)
lemma ω_simps [simp]:
shows "arr ω"
and "src ω = a" and "trg ω = a"
and "dom ω = w ⋆⇩B w" and "cod ω = w"
using isomorphic_a_w ω_in_vhom in_hom_char⇩S⇩b⇩C arr_simps by auto
lemma ide_w:
shows "B.ide w"
using isomorphic_a_w B.isomorphic_def by auto
lemma w_simps [simp]:
shows "ide w" and "B.ide w"
and "src w = a" and "trg w = a" and "src⇩B w = a" and "trg⇩B w = a"
and "dom w = w" and "cod w = w"
proof -
show w: "ide w"
using ω_in_vhom ide_cod by blast
show "B.ide w"
using w ide_char⇩S⇩b⇩C by simp
obtain φ where φ: "«φ : a ⇒⇩B w» ∧ B.iso φ"
using isomorphic_a_w B.isomorphic_def by auto
show "src⇩B w = a"
using obj_a w φ B.src_cod by force
show "trg⇩B w = a"
using obj_a w φ B.src_cod by force
show "src w = a"
using ‹src⇩B w = a› w ide_w src_def by simp
show "trg w = a"
using ‹src⇩B w = a› w ide_w trg_def
by (simp add: ‹trg⇩B w = a›)
show "dom w = w"
using w by simp
show "cod w = w"
using w by simp
qed
lemma VxV_arr_eq_VV_arr:
shows "VxV.arr f ⟷ VV.arr f"
using inclusion VxV.arr_char VV.arr_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C src_def trg_def
by auto
lemma VxV_comp_eq_VV_comp:
shows "VxV.comp = VV.comp"
proof -
have "⋀f g. VxV.comp f g = VV.comp f g"
proof -
fix f g
show "VxV.comp f g = VV.comp f g"
unfolding VV.comp_def
using VxV.comp_char arr_simps(1) arr_simps(2)
apply (cases "seq (fst f) (fst g)", cases "seq (snd f) (snd g)")
by (elim seqE) auto
qed
thus ?thesis by blast
qed
lemma VxVxV_arr_eq_VVV_arr:
shows "VxVxV.arr f ⟷ VVV.arr f"
using VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def inclusion arr_char⇩S⇩b⇩C
by auto
lemma VxVxV_comp_eq_VVV_comp:
shows "VxVxV.comp = VVV.comp"
proof -
have "⋀f g. VxVxV.comp f g = VVV.comp f g"
proof -
fix f g
show "VxVxV.comp f g = VVV.comp f g"
proof (cases "VxVxV.seq f g")
assume 1: "¬ VxVxV.seq f g"
have "VxVxV.comp f g = VxVxV.null"
using 1 VxVxV.ext by blast
also have "... = (null, null, null)"
using VxVxV.null_char VxV.null_char by simp
also have "... = VVV.null"
using VVV.null_char VV.null_char by simp
also have "... = VVV.comp f g"
proof -
have "¬ VVV.seq f g"
using 1 VVV.seq_char⇩S⇩b⇩C by blast
thus ?thesis
by (metis (no_types, lifting) VVV.ext)
qed
finally show ?thesis by simp
next
assume 1: "VxVxV.seq f g"
have 2: "B.arr (fst f) ∧ B.arr (fst (snd f)) ∧ B.arr (snd (snd f)) ∧
src⇩B (fst f) = a ∧ src⇩B (fst (snd f)) = a ∧ src⇩B (snd (snd f)) = a ∧
trg⇩B (fst f) = a ∧ trg⇩B (fst (snd f)) = a ∧ trg⇩B (snd (snd f)) = a"
using 1 VxVxV.seq_char VxV.seq_char arr_char⇩S⇩b⇩C by blast
have 3: "B.arr (fst g) ∧ B.arr (fst (snd g)) ∧ B.arr (snd (snd g)) ∧
src⇩B (fst g) = a ∧ src⇩B (fst (snd g)) = a ∧ src⇩B (snd (snd g)) = a ∧
trg⇩B (fst g) = a ∧ trg⇩B (fst (snd g)) = a ∧ trg⇩B (snd (snd g)) = a"
using 1 VxVxV.seq_char VxV.seq_char arr_char⇩S⇩b⇩C by blast
have 4: "B.seq (fst f) (fst g) ∧ B.seq (fst (snd f)) (fst (snd g)) ∧
B.seq (snd (snd f)) (snd (snd g))"
using 1 VxVxV.seq_char VxV.seq_char seq_char⇩S⇩b⇩C by blast
have 5: "VxVxV.comp f g =
(fst f ⋅ fst g, fst (snd f) ⋅ fst (snd g), snd (snd f) ⋅ snd (snd g))"
using 1 2 3 4 VxVxV.seqE⇩P⇩C VxVxV.comp_char VxV.comp_char seq_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
by (metis (no_types, lifting))
also have "... = VVV.comp f g"
using 1 VVV.comp_char VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
apply simp
using 2 3 5 arrI⇩S⇩b⇩C arr_simps(1) arr_simps(2) by presburger
finally show ?thesis by blast
qed
qed
thus ?thesis by blast
qed
interpretation H: "functor" VxV.comp ‹(⋅)› ‹λμν. fst μν ⋆ snd μν›
using H.functor_axioms hcomp_def VxV_comp_eq_VV_comp by simp
interpretation H: binary_endofunctor ‹(⋅)› ‹λμν. fst μν ⋆ snd μν› ..
lemma HoHV_eq_ToTC:
shows "HoHV = H.ToTC"
using HoHV_def H.ToTC_def VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def inclusion arr_char⇩S⇩b⇩C
by auto
lemma HoVH_eq_ToCT:
shows "HoVH = H.ToCT"
using HoVH_def H.ToCT_def VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def inclusion arr_char⇩S⇩b⇩C
by auto
interpretation ToTC: "functor" VxVxV.comp ‹(⋅)› H.ToTC
using HoHV_eq_ToTC VxVxV_comp_eq_VVV_comp HoHV.functor_axioms by simp
interpretation ToCT: "functor" VxVxV.comp ‹(⋅)› H.ToCT
using HoVH_eq_ToCT VxVxV_comp_eq_VVV_comp HoVH.functor_axioms by simp
interpretation α: natural_isomorphism VxVxV.comp ‹(⋅)› H.ToTC H.ToCT α
unfolding α_def
using α.natural_isomorphism_axioms HoHV_eq_ToTC HoVH_eq_ToCT α_def
VxVxV_comp_eq_VVV_comp
by simp
interpretation L: endofunctor ‹(⋅)› ‹λf. fst (w, f) ⋆ snd (w, f)›
proof
fix f
show "¬ arr f ⟹ fst (w, f) ⋆ snd (w, f) = null"
using arr_char⇩S⇩b⇩C hcomp_def by auto
assume f: "arr f"
show "hseq (fst (w, f)) (snd (w, f))"
using f hseq_char arr_char⇩S⇩b⇩C src_def trg_def ω_in_vhom cod_char⇩S⇩b⇩C by simp
show "dom (fst (w, f) ⋆ snd (w, f)) = fst (w, dom f) ⋆ snd (w, dom f)"
using f arr_char⇩S⇩b⇩C hcomp_def dom_simp by simp
show "cod (fst (w, f) ⋆ snd (w, f)) = fst (w, cod f) ⋆ snd (w, cod f)"
using f arr_char⇩S⇩b⇩C hcomp_def cod_simp by simp
next
fix f g
assume fg: "seq g f"
show "fst (w, g ⋅ f) ⋆ snd (w, g ⋅ f) = (fst (w, g) ⋆ snd (w, g)) ⋅ (fst (w, f) ⋆ snd (w, f))"
by (simp add: fg whisker_left)
qed
interpretation L': equivalence_functor ‹(⋅)› ‹(⋅)› ‹λf. fst (w, f) ⋆ snd (w, f)›
proof -
obtain φ where φ: "«φ : w ⇒⇩B a» ∧ B.iso φ"
using isomorphic_a_w B.isomorphic_symmetric by force
have "«φ : w ⇒ a»"
using φ in_hom_char⇩S⇩b⇩C
by (metis (no_types, lifting) B.in_homE B.src_cod B.src_src B.trg_cod B.trg_trg
ω_in_vhom arr_char⇩S⇩b⇩C arr_cod cod_simp)
hence φ: "«φ : w ⇒⇩B a» ∧ B.iso φ ∧ «φ : w ⇒ a» ∧ iso φ"
using φ iso_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C by auto
interpret 𝗅: natural_isomorphism ‹(⋅)› ‹(⋅)›
‹λf. fst (w, f) ⋆ snd (w, f)› map ‹λf. 𝔩 f ⋅ (φ ⋆ dom f)›
proof
fix μ
show "¬ arr μ ⟹ 𝔩 μ ⋅ (φ ⋆ dom μ) = null"
using φ arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C ext
apply simp
using null_is_zero(2) hcomp_def by fastforce
assume μ: "arr μ"
have 0: "in_hhom (dom μ) a a"
using μ arr_char⇩S⇩b⇩C src_dom trg_dom src_def trg_def dom_simp by simp
have 1: "in_hhom φ a a"
using φ arr_char⇩S⇩b⇩C src_dom trg_dom src_def trg_def by auto
have 2: "hseq φ (B.dom μ)"
using μ 0 1 dom_simp by (intro hseqI) auto
have 3: "seq (𝔩 μ) (φ ⋆ dom μ)"
proof (intro seqI')
show "«φ ⋆ dom μ : w ⋆ dom μ ⇒ a ⋆ dom μ»"
by (metis (no_types, lifting) 0 μ φ hcomp_in_vhom ide_dom ide_in_hom(2)
in_hhom_def w_simps(3))
show "«𝔩 μ : a ⋆ dom μ ⇒ cod μ»"
using μ 2 𝔩.preserves_hom [of μ "dom μ" "cod μ"] arr_simps(2) arr_cod by fastforce
qed
show "arr (𝔩 μ ⋅ (φ ⋆ dom μ))"
using 3 by blast
show "map μ ⋅ 𝔩 (dom μ) ⋅ (φ ⋆ dom (dom μ)) = 𝔩 μ ⋅ (φ ⋆ dom μ)"
proof -
have "map μ ⋅ 𝔩 (dom μ) ⋅ (φ ⋆ dom (dom μ)) = (map μ ⋅ 𝔩 (dom μ)) ⋅ (φ ⋆ dom μ)"
using μ comp_assoc by simp
also have "... = 𝔩 μ ⋅ (φ ⋆ dom μ)"
using μ φ 𝔩.naturality1 by auto
finally show ?thesis by blast
qed
show "(𝔩 (cod μ) ⋅ (φ ⋆ dom (cod μ))) ⋅ (fst (w, μ) ⋆ snd (w, μ)) = 𝔩 μ ⋅ (φ ⋆ dom μ)"
proof -
have "(𝔩 (cod μ) ⋅ (φ ⋆ dom (cod μ))) ⋅ (fst (w, μ) ⋆ snd (w, μ)) =
(𝔩 (cod μ) ⋅ (φ ⋆ B.cod μ)) ⋅ (w ⋆ μ)"
using μ φ dom_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C ω_in_vhom cod_simp by simp
also have "... = 𝔩 (cod μ) ⋅ (φ ⋅ w ⋆ B.cod μ ⋅ μ)"
proof -
have "seq φ w"
using φ ω_in_vhom w_simps(1) by blast
moreover have 2: "seq (B.cod μ) μ"
using μ seq_char⇩S⇩b⇩C cod_simp by (simp add: comp_cod_arr)
moreover have "src φ = trg (B.cod μ)"
using μ φ 2
by (metis (no_types, lifting) arr_simps(2) seqE vconn_implies_hpar(1) w_simps(3))
ultimately show ?thesis
using interchange comp_assoc by simp
qed
also have "... = 𝔩 (cod μ) ⋅ (φ ⋆ μ)"
using μ φ ω_in_vhom comp_arr_dom comp_cod_arr cod_simp
apply (elim conjE in_homE) by auto
also have "... = (𝔩 (cod μ) ⋅ (cod φ ⋆ μ)) ⋅ (φ ⋆ dom μ)"
proof -
have 1: "seq (cod φ) φ"
using φ arr_cod_iff_arr dom_cod iso_is_arr seqI by presburger
moreover have 2: "seq μ (dom μ)"
using μ by (simp add: comp_arr_dom)
moreover have "src (cod φ) = trg μ"
using μ φ arr_cod arr_simps(1-2) iso_is_arr by auto
ultimately show ?thesis
using 1 2 interchange [of "cod φ" φ μ "dom μ"] comp_arr_dom comp_cod_arr
comp_assoc by fastforce
qed
also have "... = 𝔩 μ ⋅ (φ ⋆ dom μ)"
proof -
have "L μ = cod φ ⋆ μ"
using μ φ arr_simps(2) in_homE by auto
hence "𝔩 (cod μ) ⋅ (cod φ ⋆ μ) = 𝔩 μ"
using μ 𝔩.naturality2 [of μ] by simp
thus ?thesis by simp
qed
finally show ?thesis by simp
qed
next
show "⋀f. ide f ⟹ iso (𝔩 f ⋅ (φ ⋆ dom f))"
proof -
fix f
assume f: "ide f"
have "iso (𝔩 f)"
using f iso_lunit by simp
moreover have "iso (φ ⋆ dom f)"
using φ f src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
apply (intro iso_hcomp, simp_all)
by (metis (no_types, lifting) in_homE)
moreover have "seq (𝔩 f) (φ ⋆ dom f)"
proof (intro seqI')
show " «𝔩 f : a ⋆ f ⇒ f»"
using f lunit_in_hom(2) 𝔩_ide_simp ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C trg_def by simp
show "«φ ⋆ dom f : w ⋆ f ⇒ a ⋆ f»"
using φ f ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C hcomp_def src_def trg_def obj_a ide_in_hom
in_hom_char⇩S⇩b⇩C
by (intro hcomp_in_vhom, auto)
qed
ultimately show "iso (𝔩 f ⋅ (φ ⋆ dom f))"
using isos_compose by simp
qed
qed
show "equivalence_functor (⋅) (⋅) (λf. fst (w, f) ⋆ snd (w, f))"
using 𝗅.natural_isomorphism_axioms L.isomorphic_to_identity_is_equivalence by simp
qed
interpretation L: equivalence_functor ‹(⋅)› ‹(⋅)› ‹λf. fst (cod ω, f) ⋆ snd (cod ω, f)›
proof -
have "(λf. fst (cod ω, f) ⋆ snd (cod ω, f)) = (λf. fst (w, f) ⋆ snd (w, f))"
using ω_in_vhom by simp
thus "equivalence_functor (⋅) (⋅) (λf. fst (cod ω, f) ⋆ snd (cod ω, f))"
using L'.equivalence_functor_axioms by simp
qed
interpretation R: endofunctor ‹(⋅)› ‹λf. fst (f, w) ⋆ snd (f, w)›
proof
fix f
show "¬ arr f ⟹ fst (f, w) ⋆ snd (f, w) = null"
using arr_char⇩S⇩b⇩C hcomp_def by auto
assume f: "arr f"
show "hseq (fst (f, w)) (snd (f, w))"
using f hseq_char arr_char⇩S⇩b⇩C src_def trg_def ω_in_vhom cod_char⇩S⇩b⇩C isomorphic_a_w
B.isomorphic_def in_hom_char⇩S⇩b⇩C
by simp
show "dom (fst (f, w) ⋆ snd (f, w)) = fst (dom f, w) ⋆ snd (dom f, w)"
using f arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C hcomp_def ω_in_vhom by simp
show "cod (fst (f, w) ⋆ snd (f, w)) = fst (cod f, w) ⋆ snd (cod f, w)"
using f arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C cod_char⇩S⇩b⇩C hcomp_def ω_in_vhom by simp
next
fix f g
assume fg: "seq g f"
have 1: "a ⋅⇩B a = a"
using obj_a by auto
show "fst (g ⋅ f, w) ⋆ snd (g ⋅ f, w) = (fst (g, w) ⋆ snd (g, w)) ⋅ (fst (f, w) ⋆ snd (f, w))"
by (simp add: fg whisker_right)
qed
interpretation R': equivalence_functor ‹(⋅)› ‹(⋅)› ‹λf. fst (f, w) ⋆ snd (f, w)›
proof -
obtain φ where φ: "«φ : w ⇒⇩B a» ∧ B.iso φ"
using isomorphic_a_w B.isomorphic_symmetric by force
have "«φ : w ⇒ a»"
using φ in_hom_char⇩S⇩b⇩C
by (metis (no_types, lifting) B.in_homE B.src_cod B.src_src B.trg_cod B.trg_trg
ω_in_vhom arr_char⇩S⇩b⇩C arr_cod cod_simp)
hence φ: "«φ : w ⇒⇩B a» ∧ B.iso φ ∧ «φ : w ⇒ a» ∧ iso φ"
using φ iso_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C by auto
interpret 𝗋: natural_isomorphism comp comp
‹λf. fst (f, w) ⋆ snd (f, w)› map ‹λf. 𝔯 f ⋅ (dom f ⋆ φ)›
proof
fix μ
show "¬ arr μ ⟹ 𝔯 μ ⋅ (dom μ ⋆ φ) = null"
using φ arr_char⇩S⇩b⇩C dom_char⇩S⇩b⇩C ext
apply simp
using null_is_zero(2) hcomp_def by fastforce
assume μ: "arr μ"
have 0: "in_hhom (dom μ) a a"
using μ arr_char⇩S⇩b⇩C src_dom trg_dom src_def trg_def dom_simp by simp
have 1: "in_hhom φ a a"
using φ arr_char⇩S⇩b⇩C src_dom trg_dom src_def trg_def by auto
have 2: "hseq (B.dom μ) φ"
using μ 0 1 dom_simp hseqI by auto
have 3: "seq (𝔯 μ) (dom μ ⋆ φ)"
proof (intro seqI')
show "«dom μ ⋆ φ : dom μ ⋆ w ⇒ dom μ ⋆ a»"
by (metis (no_types, lifting) "0" "1" μ φ hcomp_in_vhom hseqI hseq_char
ide_dom ide_in_hom(2) vconn_implies_hpar(2))
show "«𝔯 μ : dom μ ⋆ a ⇒ cod μ»"
using μ 2 𝔯.preserves_hom [of μ "dom μ" "cod μ"] arr_simps(2) arr_cod
dom_simp cod_simp
by fastforce
qed
show "arr (𝔯 μ ⋅ (dom μ ⋆ φ))"
using 3 by blast
show "map μ ⋅ 𝔯 (dom μ) ⋅ (dom (dom μ) ⋆ φ) = 𝔯 μ ⋅ (dom μ ⋆ φ)"
proof -
have "map μ ⋅ 𝔯 (dom μ) ⋅ (dom (dom μ) ⋆ φ) =
(map μ ⋅ 𝔯 (dom μ)) ⋅ (dom (dom μ) ⋆ φ)"
using comp_assoc by simp
also have "... = (map μ ⋅ 𝔯 (dom μ)) ⋅ (dom μ ⋆ φ)"
using μ dom_dom by simp
also have "... = 𝔯 μ ⋅ (dom μ ⋆ φ)"
using μ φ 𝔯.naturality1 by auto
finally show ?thesis by blast
qed
show "(𝔯 (cod μ) ⋅ (dom (cod μ) ⋆ φ)) ⋅ (fst (μ, w) ⋆ snd (μ, w)) = 𝔯 μ ⋅ (dom μ ⋆ φ)"
proof -
have "(𝔯 (cod μ) ⋅ (dom (cod μ) ⋆ φ)) ⋅ (fst (μ, w) ⋆ snd (μ, w)) =
(𝔯 (cod μ) ⋅ (B.cod μ ⋆ φ)) ⋅ (μ ⋆ w)"
using μ φ dom_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C ω_in_vhom cod_simp by simp
also have "... = 𝔯 (cod μ) ⋅ (B.cod μ ⋅ μ ⋆ φ ⋅ w)"
proof -
have 2: "seq φ w"
using φ ω_in_vhom w_simps(1) by blast
moreover have "seq (B.cod μ) μ"
using μ seq_char⇩S⇩b⇩C cod_simp by (simp add: comp_cod_arr)
moreover have "src (B.cod μ) = trg φ"
using μ φ 2
using arr_simps(1) calculation(2) seq_char⇩S⇩b⇩C vconn_implies_hpar(2) by force
ultimately show ?thesis
using interchange comp_assoc by simp
qed
also have "... = 𝔯 (cod μ) ⋅ (μ ⋆ φ)"
using μ φ ω_in_vhom comp_arr_dom comp_cod_arr cod_simp
apply (elim conjE in_homE) by auto
also have "... = (𝔯 (cod μ) ⋅ (μ ⋆ cod φ)) ⋅ (dom μ ⋆ φ)"
proof -
have "(μ ⋆ cod φ) ⋅ (dom μ ⋆ φ) = μ ⋆ φ"
proof -
have "seq μ (dom μ)"
using μ by (simp add: comp_arr_dom)
moreover have "seq (cod φ) φ"
using φ iso_is_arr arr_cod dom_cod by auto
moreover have "src μ = trg (cod φ)"
using μ φ 2
by (metis (no_types, lifting) arr_simps(1) arr_simps(2) calculation(2) seqE)
ultimately show ?thesis
using μ φ iso_is_arr comp_arr_dom comp_cod_arr
interchange [of μ "dom μ" "cod φ" φ]
by simp
qed
thus ?thesis
using comp_assoc by simp
qed
also have "... = 𝔯 μ ⋅ (dom μ ⋆ φ)"
proof -
have "μ ⋆ cod φ = R μ"
using μ φ arr_simps(1) in_homE by auto
hence "𝔯 (cod μ) ⋅ (μ ⋆ cod φ) = 𝔯 μ"
using μ φ 𝔯.naturality2 by simp
thus ?thesis by simp
qed
finally show ?thesis by simp
qed
next
show "⋀f. ide f ⟹ iso (𝔯 f ⋅ (dom f ⋆ φ))"
proof -
fix f
assume f: "ide f"
have 1: "iso (𝔯 f)"
using f iso_lunit by simp
moreover have 2: "iso (dom f ⋆ φ)"
using φ f src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
apply (intro iso_hcomp, simp_all)
by (metis (no_types, lifting) in_homE)
moreover have "seq (𝔯 f) (dom f ⋆ φ)"
proof (intro seqI')
show "«𝔯 f : f ⋆ a ⇒ f»"
using f runit_in_hom(2) 𝔯_ide_simp ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C src_def by simp
show "«dom f ⋆ φ : f ⋆ w ⇒ f ⋆ a»"
using φ f ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C hcomp_def src_def trg_def obj_a ide_in_hom
in_hom_char⇩S⇩b⇩C
by (intro hcomp_in_vhom, auto)
qed
ultimately show "iso (𝔯 f ⋅ (dom f ⋆ φ))"
using isos_compose by blast
qed
qed
show "equivalence_functor (⋅) (⋅) (λf. fst (f, w) ⋆ snd (f, w))"
using 𝗋.natural_isomorphism_axioms R.isomorphic_to_identity_is_equivalence by simp
qed
interpretation R: equivalence_functor ‹(⋅)› ‹(⋅)› ‹λf. fst (f, cod ω) ⋆ snd (f, cod ω)›
proof -
have "(λf. fst (f, cod ω) ⋆ snd (f, cod ω)) = (λf. fst (f, w) ⋆ snd (f, w))"
using ω_in_vhom by simp
thus "equivalence_functor (⋅) (⋅) (λf. fst (f, cod ω) ⋆ snd (f, cod ω))"
using R'.equivalence_functor_axioms by simp
qed
interpretation M: monoidal_category ‹(⋅)› ‹λμν. fst μν ⋆ snd μν› α ω
proof
show "«ω : fst (cod ω, cod ω) ⋆ snd (cod ω, cod ω) ⇒ cod ω»"
using ω_in_vhom hcomp_def arr_char⇩S⇩b⇩C by auto
show "iso ω"
using ω_is_iso iso_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C inv_char⇩S⇩b⇩C ω_in_vhom by auto
show "⋀f g h k. ⟦ ide f; ide g; ide h; ide k ⟧ ⟹
(fst (f, α (g, h, k)) ⋆ snd (f, α (g, h, k))) ⋅
α (f, hcomp (fst (g, h)) (snd (g, h)), k) ⋅
(fst (α (f, g, h), k) ⋆ snd (α (f, g, h), k)) =
α (f, g, fst (h, k) ⋆ snd (h, k)) ⋅ α (fst (f, g) ⋆ snd (f, g), h, k)"
proof -
fix f g h k
assume f: "ide f" and g: "ide g" and h: "ide h" and k: "ide k"
have 1: "VVV.arr (f, g, h) ∧ VVV.arr (g, h, k)"
using f g h k VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
by simp
have 2: "VVV.arr (f, g ⋆ h, k)"
using f g h k src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C VxVxV_comp_eq_VVV_comp hseqI'
by auto
have 3: "VVV.arr (f, g, h ⋆ k)"
using f g h k 1 VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C
VxV.arrI VxVxV.arrI VxVxV_comp_eq_VVV_comp H.preserves_reflects_arr hseqI'
by auto
have 4: "VVV.arr (f ⋆ g, h, k)"
using f g h k src_def trg_def ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C hseq_char VxVxV_comp_eq_VVV_comp
by auto
have "(fst (f, α (g, h, k)) ⋆ snd (f, α (g, h, k))) ⋅
α (f, fst (g, h) ⋆ snd (g, h), k) ⋅
(fst (α (f, g, h), k) ⋆ snd (α (f, g, h), k)) =
(f ⋆ 𝖺⇩B[g, h, k]) ⋅ 𝖺⇩B[f, g ⋆ h, k] ⋅ (𝖺⇩B[f, g, h] ⋆ k)"
unfolding α_def by (simp add: 1 2)
also have "... = (f ⋆⇩B 𝖺⇩B g h k) ⋅ 𝖺⇩B f (g ⋆⇩B h) k ⋅ (𝖺⇩B f g h ⋆⇩B k)"
unfolding hcomp_def
using f g h k src_def trg_def arr_char⇩S⇩b⇩C
using assoc_closed ide_char⇩S⇩b⇩C by auto
also have "... = (f ⋆⇩B 𝖺⇩B g h k) ⋅⇩B 𝖺⇩B f (g ⋆⇩B h) k ⋅⇩B (𝖺⇩B f g h ⋆⇩B k)"
proof -
have "arr (f ⋆⇩B 𝖺⇩B g h k)"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k by simp
moreover have "arr (𝖺⇩B f (g ⋆⇩B h) k)"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k by simp
moreover have "arr (𝖺⇩B f g h ⋆⇩B k)"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k by simp
moreover have "arr (𝖺⇩B f (g ⋆⇩B h) k ⋅⇩B (𝖺⇩B f g h ⋆⇩B k))"
unfolding arr_char⇩S⇩b⇩C
apply (intro conjI)
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k B.HoHV_def B.HoVH_def
apply (intro B.seqI)
apply simp_all
proof -
have 1: "B.arr (𝖺⇩B f (g ⋆⇩B h) k ⋅⇩B 𝖺⇩B f g h ⋆⇩B k)"
using f g h k ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C B.HoHV_def B.HoVH_def
apply (intro B.seqI)
by auto
show "src⇩B (𝖺⇩B f (g ⋆⇩B h) k ⋅⇩B 𝖺⇩B f g h ⋆⇩B k) = a"
using 1 f g h k arr_char⇩S⇩b⇩C B.src_vcomp B.vseq_implies_hpar(1) by fastforce
show "trg⇩B (𝖺⇩B f (g ⋆⇩B h) k ⋅⇩B 𝖺⇩B f g h ⋆⇩B k) = a"
using "1" arr_char⇩S⇩b⇩C calculation(2-3) by auto
qed
ultimately show ?thesis
using B.ext comp_char by (metis (no_types, lifting))
qed
also have "... = 𝖺⇩B f g (h ⋆⇩B k) ⋅⇩B 𝖺⇩B (f ⋆⇩B g) h k"
using f g h k src_def trg_def arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C B.pentagon
using "4" α_def hcomp_def by auto
also have "... = 𝖺⇩B f g (h ⋆⇩B k) ⋅ 𝖺⇩B (f ⋆⇩B g) h k"
proof -
have "arr (𝖺⇩B (f ⋆⇩B g) h k)"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k by simp
moreover have "arr (𝖺⇩B f g (h ⋆⇩B k))"
using ide_char⇩S⇩b⇩C arr_char⇩S⇩b⇩C assoc_closed f g h hcomp_closed k by fastforce
ultimately show ?thesis
using B.ext comp_char by auto
qed
also have "... = 𝖺⇩B[f, g, fst (h, k) ⋆ snd (h, k)] ⋅ 𝖺⇩B[fst (f, g) ⋆ snd (f, g), h, k]"
unfolding hcomp_def
using f g h k src_def trg_def arr_char⇩S⇩b⇩C ide_char⇩S⇩b⇩C by simp
also have "... = α (f, g, fst (h, k) ⋆ snd (h, k)) ⋅ α (fst (f, g) ⋆ snd (f, g), h, k)"
unfolding α_def using 1 2 3 4 by simp
finally show "(fst (f, α (g, h, k)) ⋆ snd (f, α (g, h, k))) ⋅
α (f, fst (g, h) ⋆ snd (g, h), k) ⋅
(fst (α (f, g, h), k) ⋆ snd (α (f, g, h), k)) =
α (f, g, fst (h, k) ⋆ snd (h, k)) ⋅ α (fst (f, g) ⋆ snd (f, g), h, k)"
by simp
qed
qed
proposition is_monoidal_category:
shows "monoidal_category (⋅) (λμν. fst μν ⋆ snd μν) α ω"
..
end
text ‹
In a bicategory, the ``objects'' are essentially arbitrarily chosen representatives
of their isomorphism classes. Choosing any other representatives results in an
equivalent structure. Each object ‹a› is additionally equipped with an arbitrarily chosen
unit isomorphism ‹«ι : a ⋆ a ⇒ a»›. For any ‹(a, ι)› and ‹(a', ι')›,
where ‹a› and ‹a'› are isomorphic to the same object, there exists a unique isomorphism
‹«ψ: a ⇒ a'»› that is compatible with the chosen unit isomorphisms ‹ι› and ‹ι'›.
We have already proved this property for monoidal categories, which are bicategories
with just one ``object''. Here we use that already-proven property to establish its
generalization to arbitary bicategories, by exploiting the fact that if ‹a› is an object
in a bicategory, then the sub-bicategory consisting of all ‹μ› such that
‹src μ = a = trg μ›, is a monoidal category.
At some point it would potentially be nicer to transfer the proof for monoidal
categories to obtain a direct, ``native'' proof of this fact for bicategories.
›
lemma (in bicategory) unit_unique_upto_unique_iso:
assumes "obj a"
and "isomorphic a w"
and "«ω : w ⋆ w ⇒ w»"
and "iso ω"
shows "∃!ψ. «ψ : a ⇒ w» ∧ iso ψ ∧ ψ ⋅ 𝗂[a] = ω ⋅ (ψ ⋆ ψ)"
proof -
have ω_in_hhom: "«ω : a → a»"
using assms
apply (intro in_hhomI)
apply auto
apply (metis src_cod in_homE isomorphic_implies_hpar(3) objE)
by (metis trg_cod in_homE isomorphic_implies_hpar(4) objE)
interpret S: subbicategory V H 𝖺 𝗂 src trg ‹λμ. arr μ ∧ src μ = a ∧ trg μ = a›
using assms iso_unit in_homE isoE isomorphicE VVV.arr_char⇩S⇩b⇩C VV.arr_char⇩S⇩b⇩C
apply unfold_locales
apply auto[7]
proof
fix f g h
assume f: "(arr f ∧ src f = a ∧ trg f = a) ∧ ide f"
and g: "(arr g ∧ src g = a ∧ trg g = a) ∧ ide g"
and h: "(arr h ∧ src h = a ∧ trg h = a) ∧ ide h"
and fg: "src f = trg g" and gh: "src g = trg h"
show "arr (𝖺[f, g, h])"
using assms f g h fg gh by auto
show "src (𝖺[f, g, h]) = a ∧ trg (𝖺[f, g, h]) = a"
using assms f g h fg gh by auto
show "arr (inv (𝖺[f, g, h])) ∧ src (inv (𝖺[f, g, h])) = a ∧ trg (inv (𝖺[f, g, h])) = a"
using assms f g h fg gh α.preserves_hom src_dom trg_dom by simp
next
fix f
assume f: "arr f ∧ src f = a ∧ trg f = a"
assume ide_left: "ide f"
show "arr (𝔩 f) ∧ src (𝔩 f) = a ∧ trg (𝔩 f) = a"
using f assms(1) 𝔩.preserves_hom src_cod [of "𝔩 f"] trg_cod [of "𝔩 f"] by simp
show "arr (inv (𝔩 f)) ∧ src (inv (𝔩 f)) = a ∧ trg (inv (𝔩 f)) = a"
using f ide_left assms(1) 𝔩'.preserves_hom src_dom [of "𝔩'.map f"] trg_dom [of "𝔩'.map f"]
by simp
show "arr (𝔯 f) ∧ src (𝔯 f) = a ∧ trg (𝔯 f) = a"
using f assms(1) 𝔯.preserves_hom src_cod [of "𝔯 f"] trg_cod [of "𝔯 f"] by simp
show "arr (inv (𝔯 f)) ∧ src (inv (𝔯 f)) = a ∧ trg (inv (𝔯 f)) = a"
using f ide_left assms(1) 𝔯'.preserves_hom src_dom [of "𝔯'.map f"] trg_dom [of "𝔯'.map f"]
by simp
qed
interpret S: subbicategory_at_object V H 𝖺 𝗂 src trg a a ‹𝗂[a]›
proof
show "obj a" by fact
show "isomorphic a a"
using assms(1) isomorphic_reflexive by blast
show "S.in_hom 𝗂[a] (a ⋆ a) a"
using S.arr_char⇩S⇩b⇩C S.in_hom_char⇩S⇩b⇩C assms(1) by fastforce
show "iso 𝗂[a]"
using assms iso_unit by simp
qed
interpret S⇩ω: subbicategory_at_object V H 𝖺 𝗂 src trg a w ω
proof
show "obj a" by fact
show "iso ω" by fact
show "isomorphic a w"
using assms by simp
show "S.in_hom ω (w ⋆ w) w"
using assms S.arr_char⇩S⇩b⇩C S.dom_char⇩S⇩b⇩C S.cod_char⇩S⇩b⇩C ω_in_hhom
by (intro S.in_homI, auto)
qed
interpret M: monoidal_category S.comp ‹λμν. S.hcomp (fst μν) (snd μν)› S.α ‹𝗂[a]›
using S.is_monoidal_category by simp
interpret M⇩ω: monoidal_category S.comp ‹λμν. S.hcomp (fst μν) (snd μν)› S.α ω
using S⇩ω.is_monoidal_category by simp
interpret M: monoidal_category_with_alternate_unit
S.comp ‹λμν. S.hcomp (fst μν) (snd μν)› S.α ‹𝗂[a]› ω ..
have 1: "M⇩ω.unity = w"
using assms S.cod_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) S.in_homE S⇩ω.ω_in_vhom)
have 2: "M.unity = a"
using assms S.cod_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C by simp
have "∃!ψ. S.in_hom ψ a w ∧ S.iso ψ ∧ S.comp ψ 𝗂[a] = S.comp ω (M.tensor ψ ψ)"
using assms 1 2 M.unit_unique_upto_unique_iso S.cod_char⇩S⇩b⇩C
by simp
show "∃!ψ. «ψ : a ⇒ w» ∧ iso ψ ∧ ψ ⋅ 𝗂[a] = ω ⋅ (ψ ⋆ ψ)"
proof -
have 1: "⋀ψ. S.in_hom ψ a w ⟷ «ψ : a ⇒ w»"
using assms S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C
by (metis (no_types, lifting) S.ideD(1) S.w_simps(1) S⇩ω.w_simps(1) in_homE
src_dom trg_dom)
moreover have "⋀ψ. S.in_hom ψ a w ⟹ S.iso ψ ⟷ iso ψ"
using assms S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C S.iso_char⇩S⇩b⇩C by auto
moreover have "⋀ψ. S.in_hom ψ a w ⟹ M.tensor ψ ψ = ψ ⋆ ψ"
using assms S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C S.hcomp_def by simp
moreover have "⋀ψ. S.in_hom ψ a w ⟹ S.comp ψ 𝗂[a] = ψ ⋅ 𝗂[a]"
using assms S.in_hom_char⇩S⇩b⇩C S.comp_char by auto
moreover have "⋀ψ. S.in_hom ψ a w ⟹ S.comp ω (M.tensor ψ ψ) = ω ⋅ (ψ ⋆ ψ)"
using assms S.in_hom_char⇩S⇩b⇩C S.arr_char⇩S⇩b⇩C S.hcomp_def S.comp_char S.dom_char⇩S⇩b⇩C S.cod_char⇩S⇩b⇩C
by (metis (no_types, lifting) M⇩ω.arr_tensor S⇩ω.ω_simps(1) calculation(3) ext)
ultimately show ?thesis
by (metis (no_types, lifting) M.unit_unique_upto_unique_iso S.ω_in_vhom S.in_homE
S⇩ω.ω_in_vhom)
qed
qed
end