Theory CatBicat
section "Bicategory of Categories"
text ‹
In this section we construct a bicategory whose objects correspond to categories having arrows
in a given type, whose 1-cells correspond to functors between such categories, and whose 2-cells
correspond to natural transformations between such functors. We show that the bicategory that
results from the construction is strict.
›
theory CatBicat
imports Bicategory.Strictness ConcreteBicategory
begin
locale catbicat
begin
abbreviation ARR
where "ARR A B ≡ partial_composition.arr (functor_category.comp A B)"
abbreviation MKARR
where "MKARR ≡ concrete_category.MkArr"
abbreviation MAP
where "MAP ≡ concrete_category.Map"
abbreviation DOM
where "DOM ≡ concrete_category.Dom"
abbreviation COD
where "COD ≡ concrete_category.Cod"
abbreviation NULL
where "NULL ≡ concrete_category.Null"
abbreviation OBJ
where "OBJ ≡ Collect category"
abbreviation HOM
where "HOM ≡ functor_category.comp"
abbreviation COMP
where "COMP C B A μ ν ≡ if ARR B C μ ∧ ARR A B ν
then MKARR (DOM μ o DOM ν) (COD μ o COD ν) (MAP μ o MAP ν)
else NULL"
abbreviation ID
where "ID A ≡ MKARR (identity_functor.map A) (identity_functor.map A)
(identity_functor.map A)"
abbreviation ASSOC
where "ASSOC D C B A τ μ ν ≡
if ARR C D τ ∧ ARR B C μ ∧ ARR A B ν then
MKARR (DOM τ o DOM μ o DOM ν) (COD τ o COD μ o COD ν)
(MAP τ o MAP μ o MAP ν)
else NULL"
text ‹
Although we are using the ‹concrete_bicategory› construction to take care of some
of the details, the proof is still awkward, because the locale assumptions we need to
verify are all conditioned on universally quantified entities being in the set ‹OBJ›,
and we cannot create interpretations to unpack these conditions until we are within
a proof context where these entities have been fixed and the conditions have been
introduced as assumptions.
So, for example, to prove that ‹COMP› has the required functoriality property,
we have to fix ‹A›, ‹B›, and ‹C› and introduce assumptions ‹A ∈ OBJ›, ‹B ∈ OBJ›,
and ‹C ∈ OBJ›, and only then can we use these assumptions to interpret ‹A›, ‹B›,
and ‹C› as categories and ‹HOM A B›, ‹HOM B C›, and ‹HOM A C› as functor categories.
We have to go into a still deeper proof context before we can fix particular arguments
‹μ› and ‹ν› to ‹COMP C B A›, introduce the assumptions that they are arrows of
their respective hom-categories, and finally use those assumptions to interpret them
as natural transformations. At that point, we are finally in a position to apply
the already-proved interchange law for natural transformations, which is the essential
core of the functoriality property we need to show.
›
sublocale concrete_bicategory OBJ HOM ID COMP ID ASSOC
proof (unfold concrete_bicategory_def, intro conjI allI impI)
show 1: "⋀(A :: 'a comp) (B :: 'a comp). ⟦ A ∈ OBJ; B ∈ OBJ ⟧ ⟹ category (HOM A B)"
using functor_category_def functor_category.is_category by auto
show COMP:
"⋀(A :: 'a comp) (B :: 'a comp) (C :: 'a comp).
⟦ A ∈ OBJ; B ∈ OBJ; C ∈ OBJ ⟧
⟹ binary_functor (HOM B C) (HOM A B) (HOM A C)
(λ(μ, ν). COMP C B A μ ν)"
proof -
fix A :: "'a comp" and B :: "'a comp" and C :: "'a comp"
assume A: "A ∈ OBJ" and B: "B ∈ OBJ" and C: "C ∈ OBJ"
let ?COMP = "λ(μ, ν). COMP C B A μ ν"
interpret A: category A using A by simp
interpret B: category B using B by simp
interpret C: category C using C by simp
interpret BC: functor_category B C ..
interpret AB: functor_category A B ..
interpret AC: functor_category A C ..
interpret BC_AB: product_category BC.comp AB.comp ..
show "binary_functor (HOM B C) (HOM A B) (HOM A C) (λ(μ, ν). COMP C B A μ ν)"
proof
show "⋀μν. ¬ BC_AB.arr μν ⟹ ?COMP μν = AC.null"
using BC_AB.arr_char AC.null_char AC.arr_MkArr by auto
fix μν
assume μν: "BC_AB.arr μν"
interpret μ: natural_transformation B C
‹AC.Dom (fst μν)› ‹AC.Cod (fst μν)› ‹MAP (fst μν)›
using μν BC.arr_char [of "fst μν"] by simp
interpret ν: natural_transformation A B
‹AC.Dom (snd μν)› ‹AC.Cod (snd μν)› ‹MAP (snd μν)›
using μν AB.arr_char [of "snd μν"] by simp
interpret μν: natural_transformation A C
‹AC.Dom (fst μν) o AC.Dom (snd μν)›
‹AC.Cod (fst μν) o AC.Cod (snd μν)›
‹MAP (fst μν) o MAP (snd μν)›
using μ.natural_transformation_axioms ν.natural_transformation_axioms
horizontal_composite
by blast
show "AC.arr (?COMP μν)"
using μν BC_AB.arr_char μν.natural_transformation_axioms
μν.F.functor_axioms μν.G.functor_axioms AC.arr_MkArr
by (cases μν) simp
show "AC.dom (?COMP μν) = ?COMP (BC_AB.dom μν)"
using μν BC_AB.arr_char μν.natural_transformation_axioms
μν.F.functor_axioms μν.G.functor_axioms AC.arr_MkArr
by (cases μν) simp
show "AC.cod (?COMP μν) = ?COMP (BC_AB.cod μν)"
using μν BC_AB.arr_char μν.natural_transformation_axioms
μν.F.functor_axioms μν.G.functor_axioms AC.arr_MkArr
by (cases μν) simp
next
fix μν στ
assume seq: "BC_AB.seq μν στ"
interpret μ: natural_transformation B C
‹BC.Dom (fst μν)› ‹BC.Cod (fst μν)› ‹MAP (fst μν)›
using seq BC_AB.seq_char BC_AB.arr_char BC.arr_char [of "fst μν"] AB.arr_char
by auto
interpret ν: natural_transformation A B
‹AB.Dom (snd μν)› ‹AB.Cod (snd μν)› ‹MAP (snd μν)›
using seq BC_AB.seq_char BC_AB.arr_char BC.arr_char AB.arr_char [of "snd μν"]
by auto
interpret μν: natural_transformation A C
‹AC.Dom (fst μν) o AC.Dom (snd μν)›
‹AC.Cod (fst μν) o AC.Cod (snd μν)›
‹MAP (fst μν) o MAP (snd μν)›
using μ.natural_transformation_axioms ν.natural_transformation_axioms
horizontal_composite
by blast
interpret σ: natural_transformation B C
‹BC.Dom (fst στ)› ‹BC.Cod (fst στ)› ‹MAP (fst στ)›
using seq BC_AB.seq_char BC_AB.arr_char BC.arr_char [of "fst στ"] AB.arr_char
by auto
interpret τ: natural_transformation A B
‹AB.Dom (snd στ)› ‹AB.Cod (snd στ)› ‹MAP (snd στ)›
using seq BC_AB.seq_char BC_AB.arr_char BC.arr_char AB.arr_char [of "snd στ"]
by auto
interpret στ: natural_transformation A C
‹AC.Dom (fst στ) o AC.Dom (snd στ)›
‹AC.Cod (fst στ) o AC.Cod (snd στ)›
‹MAP (fst στ) o MAP (snd στ)›
using σ.natural_transformation_axioms τ.natural_transformation_axioms
horizontal_composite
by blast
interpret μoσ: vertical_composite B C
‹BC.Dom (fst στ)› ‹BC.Cod (fst στ)› ‹BC.Cod (fst μν)›
‹MAP (fst στ)› ‹MAP (fst μν)›
using seq BC_AB.seq_char BC.seq_char μ.natural_transformation_axioms
by intro_locales (simp add: natural_transformation_def)
interpret νoτ: vertical_composite A B
‹AB.Dom (snd στ)› ‹AB.Cod (snd στ)› ‹AB.Cod (snd μν)›
‹MAP (snd στ)› ‹MAP (snd μν)›
using seq BC_AB.seq_char AB.seq_char ν.natural_transformation_axioms
by intro_locales (simp add: natural_transformation_def)
show "?COMP (BC_AB.comp μν στ) = AC.comp (?COMP μν) (?COMP στ)"
proof -
have "?COMP (BC_AB.comp μν στ) =
AC.MkArr
(BC.Dom (fst (BC_AB.comp μν στ)) ∘ AB.Dom (snd (BC_AB.comp μν στ)))
(BC.Cod (fst (BC_AB.comp μν στ)) ∘ AB.Cod (snd (BC_AB.comp μν στ)))
(BC.Map (fst (BC_AB.comp μν στ)) ∘ AB.Map (snd (BC_AB.comp μν στ)))"
using seq BC_AB.arr_char by (cases "BC_AB.comp μν στ", simp)
also have
"... =
AC.MkArr
(BC.Dom (fst στ) ∘ AB.Dom (snd στ)) (BC.Cod (fst μν) ∘ AB.Cod (snd μν))
(vertical_composite.map B C (BC.Map (fst στ)) (AB.Map (fst μν)) ∘
vertical_composite.map A B (BC.Map (snd στ)) (AB.Map (snd μν)))"
using seq BC_AB.comp_char BC_AB.seq_char BC_AB.arr_char BC.seq_char AB.seq_char
BC.Dom_comp BC.Cod_comp BC.Map_comp
AB.Dom_comp AB.Cod_comp AB.Map_comp
by auto
also have "... = AC.MkArr
(BC.Dom (fst στ) ∘ AB.Dom (snd στ))
(BC.Cod (fst μν) ∘ AB.Cod (snd μν))
(vertical_composite.map A C
(AC.Map (fst στ) ∘ AC.Map (snd στ))
(AC.Map (fst μν) ∘ AC.Map (snd μν)))"
using σ.natural_transformation_axioms τ.natural_transformation_axioms
μ.natural_transformation_axioms ν.natural_transformation_axioms
μoσ.τ.natural_transformation_axioms νoτ.τ.natural_transformation_axioms
interchange
by blast
also have "... = AC.comp (AC.MkArr (AC.Dom (fst μν) ∘ AC.Dom (snd μν))
(AC.Cod (fst μν) ∘ AC.Cod (snd μν))
(AC.Map (fst μν) ∘ AC.Map (snd μν)))
(AC.MkArr (AC.Dom (fst στ) ∘ AC.Dom (snd στ))
(AC.Cod (fst στ) ∘ AC.Cod (snd στ))
(AC.Map (fst στ) ∘ AC.Map (snd στ)))"
using seq BC_AB.seq_char BC.seq_char AB.seq_char AC.comp_MkArr
στ.natural_transformation_axioms μν.natural_transformation_axioms
by simp
also have "... = AC.comp (?COMP μν) (?COMP στ)"
using seq BC_AB.seq_char BC_AB.arr_char BC.seq_char AB.seq_char
BC.Dom_comp BC.Cod_comp BC.Map_comp
AB.Dom_comp AB.Cod_comp AB.Map_comp
by (cases μν, cases στ) simp
finally show ?thesis by blast
qed
qed
qed
show 2: "⋀(A :: 'a comp). A ∈ OBJ ⟹ partial_composition.ide (HOM A A) (ID A)"
using concrete_category.ide_MkIde functor_category.is_concrete_category
functor_category_def identity_functor.intro identity_functor.is_functor
by fastforce
show "⋀(A :: 'a comp). A ∈ OBJ
⟹ partial_composition.in_hom (HOM A A) (ID A)
(COMP A A A (ID A) (ID A)) (ID A)"
proof -
fix A :: "'a comp"
assume A: "A ∈ OBJ"
interpret A: category A
using A by simp
interpret AA: functor_category A A ..
show "AA.in_hom (ID A) (COMP A A A (ID A) (ID A)) (ID A)"
using A.is_functor by force
qed
show "⋀(A :: 'a comp). A ∈ OBJ ⟹ category.iso (HOM A A) (ID A)"
by (simp add: 1 2 category.ide_is_iso)
show "⋀(A :: 'a comp) (B :: 'a comp) (C :: 'a comp) (D :: 'a comp).
⟦ A ∈ OBJ; B ∈ OBJ; C ∈ OBJ; D ∈ OBJ ⟧
⟹ natural_isomorphism
(product_category.comp
(HOM C D) (product_category.comp (HOM B C) (HOM A B)))
(HOM A D)
(λ(f, g, h). COMP D B A (COMP D C B f g) h)
(λ(f, g, h). COMP D C A f (COMP C B A g h))
(λ(f, g, h). ASSOC D C B A f g h)"
proof -
fix A :: "'a comp" and B :: "'a comp" and C :: "'a comp" and D :: "'a comp"
assume A: "A ∈ OBJ" and B: "B ∈ OBJ" and C: "C ∈ OBJ" and D: "D ∈ OBJ"
interpret A: category A using A by simp
interpret B: category B using B by simp
interpret C: category C using C by simp
interpret D: category D using D by simp
interpret AB: functor_category A B ..
interpret BC: functor_category B C ..
interpret CD: functor_category C D ..
interpret AD: functor_category A D ..
interpret BD: functor_category B D ..
interpret AC: functor_category A C ..
interpret BC_AB: product_category BC.comp AB.comp ..
interpret CD_BC_AB: product_category CD.comp BC_AB.comp ..
let ?L = "λ(f, g, h). COMP D B A (COMP D C B f g) h"
let ?R = "λ(f, g, h). COMP D C A f (COMP C B A g h)"
let ?A = "λ(f, g, h). ASSOC D C B A f g h"
have *:
"⋀fgh fgh'. CD_BC_AB.seq fgh fgh' ⟹
AD.comp
(AD.MkArr
(CD.Dom (fst fgh) ∘ BC.Dom (fst (snd fgh)) ∘ AB.Dom (snd (snd fgh)))
(CD.Cod (fst fgh) ∘ BC.Cod (fst (snd fgh)) ∘ AB.Cod (snd (snd fgh)))
(CD.Map (fst fgh) ∘ BC.Map (fst (snd fgh)) ∘ AB.Map (snd (snd fgh))))
(AD.MkArr
(CD.Dom (fst fgh') ∘ BC.Dom (fst (snd fgh')) ∘ AB.Dom (snd (snd fgh')))
(CD.Cod (fst fgh') ∘ BC.Cod (fst (snd fgh')) ∘ AB.Cod (snd (snd fgh')))
(CD.Map (fst fgh') ∘ BC.Map (fst (snd fgh')) ∘ AB.Map (snd (snd fgh')))) =
AD.MkArr (AD.Dom (fst fgh') ∘ AD.Dom (BC.comp (fst (snd fgh)) (fst (snd fgh')))
∘ AD.Dom (AB.comp (snd (snd fgh)) (snd (snd fgh'))))
(AD.Cod (fst fgh) ∘ AD.Cod (BC.comp (fst (snd fgh)) (fst (snd fgh')))
∘ AD.Cod (AB.comp (snd (snd fgh)) (snd (snd fgh'))))
(vertical_composite.map C D (AD.Map (fst fgh')) (AD.Map (fst fgh))
∘ AD.Map (BC.comp (fst (snd fgh)) (fst (snd fgh')))
∘ AD.Map (AB.comp (snd (snd fgh)) (snd (snd fgh'))))"
proof -
fix fgh fgh'
assume seq: "CD_BC_AB.seq fgh fgh'"
have fgh: "CD_BC_AB.arr fgh"
using seq by blast
have fgh': "CD_BC_AB.arr fgh'"
using seq by blast
let ?f = "fst (fgh)" and ?g = "fst (snd (fgh))" and ?h = "snd (snd fgh)"
let ?f' = "fst (fgh')" and ?g' = "fst (snd (fgh'))" and ?h' = "snd (snd fgh')"
let ?LHS = "AD.comp
(AD.MkArr (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h)
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))
(AD.MkArr (CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(CD.Cod ?f' ∘ BC.Cod ?g' ∘ AB.Cod ?h')
(CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h'))"
let ?RHS = "AD.MkArr
(AD.Dom ?f' ∘ AD.Dom (BC.comp ?g ?g') ∘ AD.Dom (AB.comp ?h ?h'))
(AD.Cod ?f ∘ AD.Cod (BC.comp ?g ?g') ∘ AD.Cod (AB.comp ?h ?h'))
(vertical_composite.map C D (AD.Map ?f') (AD.Map ?f)
∘ AD.Map (BC.comp ?g ?g') ∘ AD.Map (AB.comp ?h ?h'))"
interpret f: natural_transformation C D ‹CD.Dom ?f› ‹CD.Cod ?f› ‹MAP ?f›
using fgh CD_BC_AB.arr_char CD.arr_char by simp
interpret g: natural_transformation B C ‹BC.Dom ?g› ‹BC.Cod ?g› ‹MAP ?g›
using fgh CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h: natural_transformation A B ‹AB.Dom ?h› ‹AB.Cod ?h› ‹MAP ?h›
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg: natural_transformation B D
‹CD.Dom ?f o BC.Dom ?g› ‹CD.Cod ?f o BC.Cod ?g› ‹MAP ?f o MAP ?g›
using f.natural_transformation_axioms g.natural_transformation_axioms
horizontal_composite
by blast
interpret fgh: natural_transformation A D
‹CD.Dom ?f o BC.Dom ?g o AB.Dom ?h›
‹CD.Cod ?f o BC.Cod ?g o AB.Cod ?h›
‹MAP ?f o MAP ?g o MAP ?h›
using f.natural_transformation_axioms g.natural_transformation_axioms
h.natural_transformation_axioms horizontal_composite
by blast
interpret f': natural_transformation C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹MAP ?f'›
using fgh' CD_BC_AB.arr_char CD.arr_char by simp
interpret g': natural_transformation B C ‹BC.Dom ?g'› ‹BC.Cod ?g'› ‹MAP ?g'›
using fgh' CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h': natural_transformation A B ‹AB.Dom ?h'› ‹AB.Cod ?h'› ‹MAP ?h'›
using fgh' CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg': natural_transformation B D
‹CD.Dom ?f' o BC.Dom ?g'› ‹CD.Cod ?f' o BC.Cod ?g'›
‹MAP ?f' o MAP ?g'›
using f'.natural_transformation_axioms g'.natural_transformation_axioms
horizontal_composite
by blast
interpret fgh': natural_transformation A D
‹CD.Dom ?f' o BC.Dom ?g' o AB.Dom ?h'›
‹CD.Cod ?f' o BC.Cod ?g' o AB.Cod ?h'›
‹MAP ?f' o MAP ?g' o MAP ?h'›
using f'.natural_transformation_axioms g'.natural_transformation_axioms
h'.natural_transformation_axioms horizontal_composite
by blast
interpret ff': vertical_composite C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹CD.Cod ?f›
‹MAP ?f'› ‹MAP ?f›
using seq CD_BC_AB.seq_char [of fgh fgh'] CD.seq_char [of ?f ?f']
f.natural_transformation_axioms f'.natural_transformation_axioms
C.category_axioms D.category_axioms
f'.F.functor_axioms f'.G.functor_axioms f.G.functor_axioms
by (metis vertical_composite.intro)
interpret gg': vertical_composite B C ‹BC.Dom ?g'› ‹BC.Cod ?g'› ‹BC.Cod ?g›
‹MAP ?g'› ‹MAP ?g›
using seq CD_BC_AB.seq_char [of fgh fgh'] BC_AB.seq_char BC.seq_char [of ?g ?g']
g.natural_transformation_axioms g'.natural_transformation_axioms
B.category_axioms C.category_axioms
g'.F.functor_axioms g'.G.functor_axioms g.G.functor_axioms
by (metis vertical_composite.intro)
interpret hh': vertical_composite A B ‹AB.Dom ?h'› ‹AB.Cod ?h'› ‹AB.Cod ?h›
‹MAP ?h'› ‹MAP ?h›
using seq CD_BC_AB.seq_char [of fgh fgh'] BC_AB.seq_char AB.seq_char [of ?h ?h']
h.natural_transformation_axioms h'.natural_transformation_axioms
A.category_axioms B.category_axioms
h'.F.functor_axioms h'.G.functor_axioms h.G.functor_axioms
by (metis vertical_composite.intro)
have "?LHS = AD.MkArr
(CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(vertical_composite.map A D
(CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h')
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))"
using AD.comp_MkArr [of "CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h'"
"CD.Cod ?f' ∘ BC.Cod ?g' ∘ AB.Cod ?h'"
"CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h'"
"CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h"
"CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h"]
using seq CD_BC_AB.seq_char CD.seq_char BC_AB.seq_char AB.arr_char
BD.seq_char AB.seq_char BC.seq_char fg.natural_transformation_axioms
fg'.natural_transformation_axioms fgh'.natural_transformation_axioms
fgh.natural_transformation_axioms
by auto
also have "... = AD.MkArr
(CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(vertical_composite.map C D (CD.Map ?f') (CD.Map ?f)
∘ vertical_composite.map B C (BC.Map ?g') (BC.Map ?g)
o vertical_composite.map A B (AB.Map ?h') (AB.Map ?h))"
proof -
have "vertical_composite.map A D
(CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h')
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h) =
vertical_composite.map C D (CD.Map ?f') (CD.Map ?f)
∘ vertical_composite.map B C (BC.Map ?g') (BC.Map ?g)
o vertical_composite.map A B (AB.Map ?h') (AB.Map ?h)"
using interchange
[of B C "BC.Dom ?g'" "BC.Cod ?g'" "BC.Map ?g'"
"BC.Cod ?g" "BC.Map ?g" D
"CD.Dom ?f'" "CD.Cod ?f'" "CD.Map ?f'"
"CD.Cod ?f" "CD.Map ?f"]
interchange
f'.natural_transformation_axioms ff'.τ.natural_transformation_axioms
g'.natural_transformation_axioms gg'.τ.natural_transformation_axioms
fg'.natural_transformation_axioms
gg'.τ.natural_transformation_axioms h'.natural_transformation_axioms
hh'.τ.natural_transformation_axioms horizontal_composite
by (metis (no_types, lifting))
thus ?thesis by simp
qed
also have "... = ?RHS"
by (metis (no_types, lifting) AB.Cod_comp AB.Dom_comp AB.Map_comp'
AB.seq_char BC.Cod_comp BC.Dom_comp BC.Map_comp' BC.seq_char
BC_AB.seq_char CD_BC_AB.seqE⇩P⇩C seq)
finally show "?LHS = ?RHS" by fastforce
qed
interpret L: "functor" CD_BC_AB.comp AD.comp ?L
proof
interpret CD_BC: product_category CD.comp BC.comp ..
interpret BD: functor_category B D ..
fix fgh
show "¬ CD_BC_AB.arr fgh ⟹ ?L fgh = AD.null"
using AD.null_char BD.null_char by (cases fgh, auto)
assume fgh: "CD_BC_AB.arr fgh"
let ?f = "fst (fgh)" and ?g = "fst (snd (fgh))" and ?h = "snd (snd fgh)"
interpret f: natural_transformation C D ‹CD.Dom ?f› ‹CD.Cod ?f› ‹MAP ?f›
using fgh CD_BC_AB.arr_char CD.arr_char by simp
interpret g: natural_transformation B C ‹BC.Dom ?g› ‹BC.Cod ?g› ‹MAP ?g›
using fgh CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h: natural_transformation A B ‹AB.Dom ?h› ‹AB.Cod ?h› ‹MAP ?h›
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg: natural_transformation B D
‹CD.Dom ?f o BC.Dom ?g› ‹CD.Cod ?f o BC.Cod ?g› ‹MAP ?f o MAP ?g›
using f.natural_transformation_axioms g.natural_transformation_axioms
horizontal_composite
by blast
interpret fgh: natural_transformation A D
‹CD.Dom ?f o BC.Dom ?g o AB.Dom ?h›
‹CD.Cod ?f o BC.Cod ?g o AB.Cod ?h›
‹MAP ?f o MAP ?g o MAP ?h›
using f.natural_transformation_axioms g.natural_transformation_axioms
h.natural_transformation_axioms horizontal_composite
by blast
show 1: "AD.arr (?L fgh)"
using fgh CD_BC_AB.arr_char CD.arr_char BC_AB.arr_char BC.arr_char AB.arr_char
fg.natural_transformation_axioms fgh.natural_transformation_axioms
fgh.F.functor_axioms fgh.G.functor_axioms AD.arr_char
by (cases fgh, auto)
show "AD.dom (?L fgh) = ?L (CD_BC_AB.dom fgh)"
using fgh 1 fg.natural_transformation_axioms fg.F.functor_axioms
by (cases fgh, auto)
show "AD.cod (?L fgh) = ?L (CD_BC_AB.cod fgh)"
using fgh 1 fg.natural_transformation_axioms fg.G.functor_axioms
by (cases fgh, auto)
next
fix fgh fgh'
assume seq: "CD_BC_AB.seq fgh fgh'"
have fgh: "CD_BC_AB.arr fgh"
using seq by blast
have fgh': "CD_BC_AB.arr fgh'"
using seq by blast
let ?f = "fst (fgh)" and ?g = "fst (snd (fgh))" and ?h = "snd (snd fgh)"
interpret f: natural_transformation C D ‹CD.Dom ?f› ‹CD.Cod ?f› ‹MAP ?f›
using fgh CD_BC_AB.arr_char CD.arr_char by simp
interpret g: natural_transformation B C ‹BC.Dom ?g› ‹BC.Cod ?g› ‹MAP ?g›
using fgh CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h: natural_transformation A B ‹AB.Dom ?h› ‹AB.Cod ?h› ‹MAP ?h›
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg: natural_transformation B D
‹CD.Dom ?f o BC.Dom ?g› ‹CD.Cod ?f o BC.Cod ?g› ‹MAP ?f o MAP ?g›
using f.natural_transformation_axioms g.natural_transformation_axioms
horizontal_composite
by blast
let ?f' = "fst (fgh')" and ?g' = "fst (snd (fgh'))" and ?h' = "snd (snd fgh')"
interpret f': natural_transformation C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹MAP ?f'›
using fgh' CD_BC_AB.arr_char CD.arr_char by simp
interpret g': natural_transformation B C ‹BC.Dom ?g'› ‹BC.Cod ?g'› ‹MAP ?g'›
using fgh' CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h': natural_transformation A B ‹AB.Dom ?h'› ‹AB.Cod ?h'› ‹MAP ?h'›
using fgh' CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg': natural_transformation B D
‹CD.Dom ?f' o BC.Dom ?g'› ‹CD.Cod ?f' o BC.Cod ?g'›
‹MAP ?f' o MAP ?g'›
using f'.natural_transformation_axioms g'.natural_transformation_axioms
horizontal_composite
by blast
interpret ff': vertical_composite C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹CD.Cod ?f›
‹MAP ?f'› ‹MAP ?f›
using seq CD_BC_AB.seq_char [of fgh fgh'] CD.seq_char [of ?f ?f']
f.natural_transformation_axioms f'.natural_transformation_axioms
C.category_axioms D.category_axioms
f'.F.functor_axioms f'.G.functor_axioms f.G.functor_axioms
by (unfold vertical_composite_def) presburger
interpret gg': vertical_composite B C ‹CD.Dom ?g'› ‹CD.Cod ?g'› ‹CD.Cod ?g›
‹MAP ?g'› ‹MAP ?g›
using seq CD_BC_AB.seq_char [of fgh fgh'] CD.seq_char [of ?g ?g']
g.natural_transformation_axioms g'.natural_transformation_axioms
C.category_axioms D.category_axioms
by (unfold vertical_composite_def)
(metis BC.seq_char BC_AB.seqE⇩P⇩C natural_transformation_def)
interpret gg'off': natural_transformation B D
‹AC.Dom (fst fgh') ∘ AC.Dom (fst (snd fgh'))›
‹AC.Cod (fst fgh) ∘ AC.Cod (fst (snd fgh))› ‹ff'.map ∘ gg'.map›
by (meson ff'.natural_transformation_axioms gg'.natural_transformation_axioms
horizontal_composite)
show "?L (CD_BC_AB.comp fgh fgh') = AD.comp (?L fgh) (?L fgh')"
proof -
have "AD.comp (?L fgh) (?L fgh') =
AD.comp
(AD.MkArr (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h)
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))
(AD.MkArr (CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(CD.Cod ?f' ∘ BC.Cod ?g' ∘ AB.Cod ?h')
(CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h'))"
using seq CD_BC_AB.seq_char CD.seq_char BC_AB.seq_char AB.arr_char
BD.seq_char AB.seq_char BC.seq_char fg.natural_transformation_axioms
fg'.natural_transformation_axioms
by (cases fgh, cases fgh') auto
also have "... =
AD.MkArr
(AD.Dom ?f' ∘ AD.Dom (BC.comp ?g ?g') ∘ AD.Dom (AB.comp ?h ?h'))
(AD.Cod ?f ∘ AD.Cod (BC.comp ?g ?g') ∘ AD.Cod (AB.comp ?h ?h'))
(vertical_composite.map C D (AD.Map ?f') (AD.Map ?f)
∘ AD.Map (BC.comp ?g ?g')
∘ AD.Map (AB.comp ?h ?h'))"
using seq * [of fgh fgh'] by blast
also have "... = ?L (CD_BC_AB.comp fgh fgh')"
using fgh fgh' CD_BC_AB.comp_char CD.seq_char BC_AB.comp_char
BC.seq_char AB.seq_char gg'off'.natural_transformation_axioms
apply simp
by (metis (no_types, lifting) BC_AB.seqE⇩P⇩C CD_BC_AB.seqE⇩P⇩C seq)
finally show ?thesis by argo
qed
qed
interpret R: "functor" CD_BC_AB.comp AD.comp ?R
proof
interpret CD_BC: product_category CD.comp BC.comp ..
interpret AC: functor_category A C ..
fix fgh
show "¬ CD_BC_AB.arr fgh ⟹ ?R fgh = AD.null"
using AD.null_char AC.null_char by (cases fgh, auto)
assume fgh: "CD_BC_AB.arr fgh"
let ?f = "fst (fgh)" and ?g = "fst (snd (fgh))" and ?h = "snd (snd fgh)"
interpret f: natural_transformation C D ‹CD.Dom ?f› ‹CD.Cod ?f› ‹MAP ?f›
using fgh CD_BC_AB.arr_char CD.arr_char by simp
interpret g: natural_transformation B C ‹BC.Dom ?g› ‹BC.Cod ?g› ‹MAP ?g›
using fgh CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h: natural_transformation A B ‹AB.Dom ?h› ‹AB.Cod ?h› ‹MAP ?h›
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret fg: natural_transformation B D
‹CD.Dom ?f o BC.Dom ?g› ‹CD.Cod ?f o BC.Cod ?g› ‹MAP ?f o MAP ?g›
using f.natural_transformation_axioms g.natural_transformation_axioms
horizontal_composite
by blast
interpret gh: natural_transformation A C
‹BC.Dom ?g o AB.Dom ?h› ‹BC.Cod ?g o AB.Cod ?h›
‹MAP ?g o MAP ?h›
using g.natural_transformation_axioms h.natural_transformation_axioms
horizontal_composite
by blast
interpret fgh: natural_transformation A D
‹CD.Dom ?f o (BC.Dom ?g o AB.Dom ?h)›
‹CD.Cod ?f o (BC.Cod ?g o AB.Cod ?h)›
‹MAP ?f o (MAP ?g o MAP ?h)›
using f.natural_transformation_axioms g.natural_transformation_axioms
h.natural_transformation_axioms horizontal_composite
by blast
show 1: "AD.arr (?R fgh)"
using fgh CD_BC_AB.arr_char AB.arr_char CD_BC.arr_char CD.arr_char BC.arr_char
gh.natural_transformation_axioms fgh.natural_transformation_axioms
fgh.F.functor_axioms fgh.G.functor_axioms AD.arr_char AC.arr_char
by (cases fgh) (simp add: natural_transformation_def)
show "AD.dom (?R fgh) = ?R (CD_BC_AB.dom fgh)"
using fgh 1 gh.natural_transformation_axioms gh.F.functor_axioms
by (cases fgh) auto
show "AD.cod (?R fgh) = ?R (CD_BC_AB.cod fgh)"
using fgh 1 gh.natural_transformation_axioms gh.G.functor_axioms
by (cases fgh) auto
next
fix fgh fgh'
assume seq: "CD_BC_AB.seq fgh fgh'"
have fgh: "CD_BC_AB.arr fgh"
using seq by blast
have fgh': "CD_BC_AB.arr fgh'"
using seq by blast
let ?f = "fst (fgh)" and ?g = "fst (snd (fgh))" and ?h = "snd (snd fgh)"
have f: "CD.arr ?f" and g: "BC.arr ?g" and h: "AB.arr ?h"
using fgh by simp_all
interpret f: natural_transformation C D ‹CD.Dom ?f› ‹CD.Cod ?f› ‹MAP ?f›
using fgh CD_BC_AB.arr_char CD.arr_char by simp
interpret g: natural_transformation B C ‹BC.Dom ?g› ‹BC.Cod ?g› ‹MAP ?g›
using fgh CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by simp
interpret h: natural_transformation A B ‹AB.Dom ?h› ‹AB.Cod ?h› ‹MAP ?h›
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by simp
interpret gh: natural_transformation A C
‹BC.Dom ?g o AB.Dom ?h› ‹BC.Cod ?g o AB.Cod ?h›
‹MAP ?g o MAP ?h›
using g.natural_transformation_axioms h.natural_transformation_axioms
horizontal_composite
by blast
let ?f' = "fst (fgh')" and ?g' = "fst (snd (fgh'))" and ?h' = "snd (snd fgh')"
have f': "CD.arr ?f'" and g': "BC.arr ?g'" and h': "AB.arr ?h'"
using fgh' by simp_all
interpret f': natural_transformation C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹MAP ?f'›
using seq CD_BC_AB.arr_char CD.arr_char by blast
interpret g': natural_transformation B C ‹BC.Dom ?g'› ‹BC.Cod ?g'› ‹MAP ?g'›
using seq CD_BC_AB.arr_char BC_AB.arr_char BC.arr_char by blast
interpret h': natural_transformation A B ‹AB.Dom ?h'› ‹AB.Cod ?h'› ‹MAP ?h'›
using seq CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char by blast
interpret gh': natural_transformation A C
‹BC.Dom ?g' o AB.Dom ?h'› ‹BC.Cod ?g' o AB.Cod ?h'›
‹MAP ?g' o MAP ?h'›
using g'.natural_transformation_axioms h'.natural_transformation_axioms
horizontal_composite
by blast
interpret fg': natural_transformation B D
‹CD.Dom ?f' o BC.Dom ?g'› ‹CD.Cod ?f' o BC.Cod ?g'›
‹MAP ?f' o MAP ?g'›
using f'.natural_transformation_axioms g'.natural_transformation_axioms
horizontal_composite
by blast
interpret ff': vertical_composite C D ‹CD.Dom ?f'› ‹CD.Cod ?f'› ‹CD.Cod ?f›
‹MAP ?f'› ‹MAP ?f›
using seq CD_BC_AB.seq_char [of fgh fgh'] CD.seq_char [of ?f ?f']
f.natural_transformation_axioms f'.natural_transformation_axioms
C.category_axioms D.category_axioms
f'.F.functor_axioms f'.G.functor_axioms f.G.functor_axioms
by (metis vertical_composite.intro)
interpret gg': vertical_composite B C ‹BC.Dom ?g'› ‹BC.Cod ?g'› ‹BC.Cod ?g›
‹MAP ?g'› ‹MAP ?g›
using seq CD_BC_AB.seq_char [of fgh fgh'] BC_AB.seq_char BC.seq_char [of ?g ?g']
g.natural_transformation_axioms g'.natural_transformation_axioms
B.category_axioms C.category_axioms
g'.F.functor_axioms g'.G.functor_axioms g.G.functor_axioms
by (metis vertical_composite.intro)
interpret hh': vertical_composite A B ‹AB.Dom ?h'› ‹AB.Cod ?h'› ‹AB.Cod ?h›
‹MAP ?h'› ‹MAP ?h›
using seq CD_BC_AB.seq_char [of fgh fgh'] BC_AB.seq_char AB.seq_char [of ?h ?h']
h.natural_transformation_axioms h'.natural_transformation_axioms
A.category_axioms B.category_axioms
h'.F.functor_axioms h'.G.functor_axioms h.G.functor_axioms
by (metis vertical_composite.intro)
show "?R (CD_BC_AB.comp fgh fgh') = AD.comp (?R fgh) (?R fgh')"
proof -
have "AD.comp (?R fgh) (?R fgh') =
AD.comp
(AD.MkArr (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h)
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))
(AD.MkArr (CD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(CD.Cod ?f' ∘ BC.Cod ?g' ∘ AB.Cod ?h')
(CD.Map ?f' ∘ BC.Map ?g' ∘ AB.Map ?h'))"
using fgh fgh' gh.natural_transformation_axioms gh'.natural_transformation_axioms
apply (cases fgh, cases fgh')
by (simp add: o_assoc)
also have "... =
AD.MkArr
(AD.Dom ?f' ∘ AD.Dom (BC.comp ?g ?g') ∘ AD.Dom (AB.comp ?h ?h'))
(AD.Cod ?f ∘ AD.Cod (BC.comp ?g ?g') ∘ AD.Cod (AB.comp ?h ?h'))
(vertical_composite.map C D (AD.Map ?f') (AD.Map ?f)
∘ AD.Map (BC.comp ?g ?g')
∘ AD.Map (AB.comp ?h ?h'))"
using seq * [of fgh fgh'] by blast
also have "... = AD.MkArr
(AD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(AD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(vertical_composite.map C D (AD.Map ?f') (AD.Map ?f)
∘ AD.Map (BC.comp ?g ?g')
∘ AD.Map (AB.comp ?h ?h'))"
using seq CD_BC_AB.seq_char BC_AB.seq_char BC.Dom_comp AB.Dom_comp
BC.Cod_comp AB.Cod_comp BC.seq_char AB.seq_char
by (simp add: o_assoc)
also have "... = AD.MkArr
(AD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(AD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(vertical_composite.map C D (AD.Map ?f') (AD.Map ?f) o
vertical_composite.map B C (BC.Map ?g') (BC.Map ?g) o
vertical_composite.map A B (AB.Map ?h') (AB.Map ?h))"
using seq CD_BC_AB.seq_char BC_AB.seq_char BC.Map_comp AB.Map_comp
BC.seq_char AB.seq_char
by (cases fgh) simp
also have "... = AD.MkArr
(AD.Dom ?f' ∘ BC.Dom ?g' ∘ AB.Dom ?h')
(AD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map (CD.comp ?f ?f') o BC.Map (BC.comp ?g ?g')
o AB.Map (AB.comp ?h ?h'))"
using seq CD_BC_AB.seq_char BC_AB.seq_char CD.Map_comp BC.Map_comp
AB.Map_comp CD.seq_char BC.seq_char AB.seq_char
by simp
also have
"... =
AD.MkArr
(CD.Dom (CD.comp ?f ?f') ∘ (BC.Dom (BC.comp ?g ?g') ∘ AB.Dom (AB.comp ?h ?h')))
(CD.Cod (CD.comp ?f ?f') ∘ (BC.Cod (BC.comp ?g ?g') ∘ AB.Cod (AB.comp ?h ?h')))
(CD.Map (CD.comp ?f ?f') ∘ (BC.Map (BC.comp ?g ?g') ∘ AB.Map (AB.comp ?h ?h')))"
using seq CD_BC_AB.seq_char BC_AB.seq_char BC.Dom_comp AB.Dom_comp
BC.Cod_comp AB.Cod_comp CD.seq_char BC.seq_char AB.seq_char
by (cases fgh) (simp add: o_assoc)
also have "... = ?R (CD.comp ?f ?f', BC.comp ?g ?g', AB.comp ?h ?h')"
proof -
have "CD.seq ?f ?f' ∧ BC.seq ?g ?g' ∧ AB.seq ?h ?h'"
using seq CD_BC_AB.seq_char BC_AB.seq_char CD.seq_char BC.seq_char AB.seq_char
by simp
moreover have "natural_transformation A C
(AC.Dom (BC.comp ?g ?g') ∘ AC.Dom (AB.comp ?h ?h'))
(AC.Cod (BC.comp ?g ?g') ∘ AC.Cod (AB.comp ?h ?h'))
(AC.Map (BC.comp ?g ?g') ∘ AC.Map (AB.comp ?h ?h'))"
using horizontal_composite calculation by blast
ultimately show ?thesis by simp
qed
also have "... = ?R (CD_BC_AB.comp fgh fgh')"
using seq fgh fgh' CD_BC_AB.comp_simp BC_AB.comp_simp CD_BC_AB.seq_char
BC_AB.seq_char
by (cases fgh) simp
finally show ?thesis by argo
qed
qed
interpret A: natural_transformation CD_BC_AB.comp AD.comp ?L ?R ?A
proof
interpret CD_BC: product_category CD.comp BC.comp ..
fix fgh
show "¬ CD_BC_AB.arr fgh ⟹ ?A fgh = AD.null"
using AD.null_char BD.null_char by (cases fgh, auto)
assume fgh: "CD_BC_AB.arr fgh"
show "AD.dom (?A fgh) = ?L (CD_BC_AB.dom fgh)"
using fgh AD.dom_char AB.arr_char BC.arr_char CD.arr_char
AB.dom_char BC.dom_char CD.dom_char
apply (cases fgh) apply simp
by (metis (no_types, lifting) functor_is_transformation horizontal_composite)
show "AD.cod (?A fgh) = ?R (CD_BC_AB.cod fgh)"
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char CD.arr_char
AD.cod_char AB.arr_char BC.arr_char CD.arr_char
AB.cod_char BC.cod_char CD.cod_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis (no_types, lifting) functor_is_transformation horizontal_composite)
show "AD.comp (?A (CD_BC_AB.cod fgh)) (?L fgh) = ?A fgh"
proof -
let ?f = "fst fgh" and ?g = "fst (snd fgh)" and ?h = "snd (snd fgh)"
have 1: "natural_transformation B D
(CD.Dom ?f ∘ BC.Dom ?g) (CD.Cod ?f ∘ BC.Cod ?g)
(CD.Map ?f ∘ BC.Map ?g)"
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis (no_types, lifting) horizontal_composite)
have 2: "natural_transformation A D (AC.Dom ?f ∘ AC.Dom ?g ∘ AC.Dom ?h)
(AC.Cod ?f ∘ AC.Cod ?g ∘ AC.Cod ?h)
(AC.Map ?f ∘ AC.Map ?g ∘ AC.Map ?h)"
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char
CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis (no_types, lifting) horizontal_composite)
have "AD.comp (?A (CD_BC_AB.cod fgh)) (?L fgh) =
AD.comp (AD.MkIde (CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h))
(AD.MkArr (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h)
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))"
using 1 2 fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis AB.cod_char BC.MkIde_Cod CD.arr.simps(2) CD.arr_cod_iff_arr)
also have "... = ?A fgh"
using 2 fgh
by (cases fgh) (simp add: o_assoc AD.comp_cod_arr)
finally show ?thesis by simp
qed
show "AD.comp (?R fgh) (?A (CD_BC_AB.dom fgh)) = ?A fgh"
proof -
let ?f = "fst fgh" and ?g = "fst (snd fgh)" and ?h = "snd (snd fgh)"
have 1: "natural_transformation A C
(AC.Dom ?g ∘ AC.Dom ?h) (AC.Cod ?g ∘ AC.Cod ?h)
(AC.Map ?g ∘ AC.Map ?h)"
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis (no_types, lifting) horizontal_composite)
have 2: "natural_transformation A D (AC.Dom ?f ∘ AC.Dom ?g ∘ AC.Dom ?h)
(AC.Cod ?f ∘ AC.Cod ?g ∘ AC.Cod ?h)
(AC.Map ?f ∘ AC.Map ?g ∘ AC.Map ?h)"
using fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis (no_types, lifting) horizontal_composite)
have "AD.comp (?R fgh) (?A (CD_BC_AB.dom fgh)) =
AD.comp (AD.MkArr (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h)
(CD.Cod ?f ∘ BC.Cod ?g ∘ AB.Cod ?h)
(CD.Map ?f ∘ BC.Map ?g ∘ AB.Map ?h))
(AD.MkIde (CD.Dom ?f ∘ BC.Dom ?g ∘ AB.Dom ?h))"
using 1 2 fgh CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char BC.arr_char
CD.arr_char
apply (cases fgh)
apply (simp add: o_assoc)
by (metis AB.dom_char BC.MkIde_Dom CD.arr.simps(2) CD.arr_dom_iff_arr)
also have "... = ?A fgh"
using 2 fgh
by (cases fgh) (simp add: o_assoc AD.comp_arr_dom)
finally show ?thesis by simp
qed
qed
show "natural_isomorphism CD_BC_AB.comp AD.comp ?L ?R ?A"
proof
fix abc
assume abc: "CD_BC_AB.ide abc"
show "AD.iso (?A abc)"
proof -
interpret A_abc: natural_transformation A D
‹BD.Dom (?A abc)› ‹BD.Cod (?A abc)› ‹BD.Map (?A abc)›
using abc CD_BC_AB.ideD(1) CD_BC_AB.arr_char BC_AB.arr_char AB.arr_char
BC.arr_char CD.arr_char
apply (cases abc)
apply (simp add: o_assoc)
by (metis AB.null_char BC.null_char CD.null_char functor_is_transformation
horizontal_composite)
interpret A_abc: natural_isomorphism A D
‹BD.Dom (?A abc)› ‹BD.Cod (?A abc)› ‹BD.Map (?A abc)›
proof -
have "⋀a'. A.ide a' ⟹ D.iso (CD.Map (fst abc)
(BC.Map (fst (snd abc))
(AB.Map (snd (snd abc)) a')))"
proof -
fix a'
assume a': "A.ide a'"
have "BC.ide (fst (snd abc)) ∧ AB.ide (snd (snd abc))"
using abc by force
hence "C.iso (AC.Map (fst (snd abc)) (AC.Map (snd (snd abc)) a'))"
using a' by (metis (no_types) A.ide_is_iso AB.ide_char BC.ide_char
functor.preserves_iso)
thus "D.iso (AC.Map (fst abc) (AC.Map (fst (snd abc))
(AC.Map (snd (snd abc)) a')))"
by (meson CD.ide_char CD_BC_AB.ide_char⇩P⇩C abc functor.preserves_iso)
qed
thus "natural_isomorphism A D
(BD.Dom (?A abc)) (BD.Cod (?A abc)) (BD.Map (?A abc))"
apply unfold_locales
using abc CD_BC_AB.iso_char BC_AB.iso_char A.ide_is_iso functor.preserves_iso
by (cases abc) simp
qed
have "?A abc ≠ AD.null"
using abc
by (metis (no_types, lifting) A.preserves_reflects_arr AD.not_arr_null
CD_BC_AB.ideD(1))
moreover have "natural_isomorphism A D
(BD.Dom (?A abc)) (BD.Cod (?A abc)) (BD.Map (?A abc))"
..
ultimately show ?thesis by simp
qed
qed
qed
show "⋀(A :: 'a comp) (B :: 'a comp). ⟦ A ∈ OBJ; B ∈ OBJ ⟧
⟹ fully_faithful_functor (HOM A B) (HOM A B)
(λf. if partial_composition.arr (HOM A B) f
then COMP B B A (ID B) f
else partial_magma.null (HOM A B))"
proof -
fix A :: "'a comp" and B :: "'a comp"
assume A: "A ∈ OBJ" and B: "B ∈ OBJ"
interpret A: category A using A by simp
interpret B: category B using B by simp
interpret AB: functor_category A B ..
interpret BB: functor_category B B ..
let ?L = "λf. if partial_composition.arr (HOM A B) f
then COMP B B A (ID B) f
else partial_magma.null (HOM A B)"
have "?L = AB.map"
using AB.arr_char B.functor_axioms AB.MkArr_Map AB.is_extensional by force
thus "fully_faithful_functor AB.comp AB.comp ?L"
by (simp add: AB.is_fully_faithful)
qed
show "⋀(A :: 'a comp) (B :: 'a comp). ⟦ A ∈ OBJ; B ∈ OBJ ⟧
⟹ fully_faithful_functor (HOM A B) (HOM A B)
(λf. if partial_composition.arr (HOM A B) f
then COMP B A A f (ID A)
else partial_magma.null (HOM A B))"
proof -
fix A :: "'a comp" and B :: "'a comp"
assume A: "A ∈ OBJ" and B: "B ∈ OBJ"
interpret A: category A using A by simp
interpret B: category B using B by simp
interpret AB: functor_category A B ..
interpret AA: functor_category A A ..
interpret BB: functor_category B B ..
let ?R = "λf. if partial_composition.arr (HOM A B) f
then COMP B A A f (ID A)
else partial_magma.null (HOM A B)"
have "?R = AB.map"
proof
fix f
have "¬ AB.arr f ⟹ ?R f = AB.map f"
using AB.is_extensional by simp
moreover have "AB.arr f ⟹ ?R f = AB.map f"
proof -
assume f: "AB.arr f"
have "?R f =
BB.MkArr (BB.Dom f ∘ A.map) (BB.Cod f ∘ A.map) (BB.Map f ∘ A.map)"
using f AB.arr_char BB.ide_MkIde BB.arr_char A.functor_axioms by simp
also have "... = AB.map f"
using f AB.arr_char AB.MkArr_Map by force
finally show "?R f = AB.map f" by blast
qed
ultimately show "?R f = AB.map f" by blast
qed
thus "fully_faithful_functor AB.comp AB.comp ?R"
by (simp add: AB.is_fully_faithful)
qed
show "⋀(A :: 'a comp) (B :: 'a comp) (C :: 'a comp) (D :: 'a comp) (E :: 'a comp) f g h k.
⟦ A ∈ OBJ; B ∈ OBJ; C ∈ OBJ; D ∈ OBJ; E ∈ OBJ;
partial_composition.ide (HOM D E) f; partial_composition.ide (HOM C D) g;
partial_composition.ide (HOM B C) h; partial_composition.ide (HOM A B) k ⟧ ⟹
HOM A E (COMP E D A f (ASSOC D C B A g h k))
(HOM A E (ASSOC E D B A f (COMP D C B g h) k)
(COMP E B A (ASSOC E D C B f g h) k)) =
HOM A E (ASSOC E D C A f g (COMP C B A h k))
(ASSOC E C B A (COMP E D C f g) h k)"
proof -
fix A :: "'a comp" and B :: "'a comp" and C :: "'a comp"
and D :: "'a comp" and E :: "'a comp"
fix f g h k
assume A: "A ∈ OBJ" and B: "B ∈ OBJ" and C: "C ∈ OBJ"
and D: "D ∈ OBJ" and E: "E ∈ OBJ"
assume f: "partial_composition.ide (HOM D E) f"
assume g: "partial_composition.ide (HOM C D) g"
assume h: "partial_composition.ide (HOM B C) h"
assume k: "partial_composition.ide (HOM A B) k"
interpret A: category A using A by simp
interpret B: category B using B by simp
interpret C: category C using C by simp
interpret D: category D using D by simp
interpret E: category E using E by simp
interpret AB: functor_category A B ..
interpret BC: functor_category B C ..
interpret CD: functor_category C D ..
interpret DE: functor_category D E ..
interpret BD: functor_category B D ..
interpret AD: functor_category A D ..
interpret CE: functor_category C E ..
interpret AC: functor_category A C ..
interpret BE: functor_category B E ..
interpret AE: functor_category A E ..
interpret f: natural_transformation D E ‹DE.Dom f› ‹DE.Cod f› ‹MAP f›
using f DE.arr_char by simp
interpret g: natural_transformation C D ‹CD.Dom g› ‹CD.Cod g› ‹MAP g›
using g CD.arr_char by simp
interpret h: natural_transformation B C ‹BC.Dom h› ‹BC.Cod h› ‹MAP h›
using h BC.arr_char by simp
interpret k: natural_transformation A B ‹AB.Dom k› ‹AB.Cod k› ‹MAP k›
using k AB.arr_char by simp
have 0: "natural_transformation A E
(DE.Map f ∘ CD.Map g ∘ BC.Map h ∘ AB.Map k)
(DE.Map f ∘ CD.Map g ∘ BC.Map h ∘ AB.Map k)
(DE.Map f ∘ CD.Map g ∘ BC.Map h ∘ AB.Map k)"
using f.natural_transformation_axioms g.natural_transformation_axioms
h.natural_transformation_axioms k.natural_transformation_axioms
f g h k AB.ide_char BC.ide_char CD.ide_char DE.ide_char
horizontal_composite
by (metis (no_types, lifting))
have 1: "natural_transformation B D
(CD.Map g ∘ BC.Map h) (CD.Map g ∘ BC.Map h) (CD.Map g ∘ BC.Map h)"
using g.natural_transformation_axioms h.natural_transformation_axioms
g h BC.ide_char CD.ide_char horizontal_composite
by (metis (no_types, lifting))
have 2: "natural_transformation B E
(DE.Map f ∘ CD.Map g ∘ BC.Map h)
(DE.Map f ∘ CD.Map g ∘ BC.Map h)
(DE.Map f ∘ CD.Map g ∘ BC.Map h)"
using 1 f.natural_transformation_axioms f DE.ide_char horizontal_composite o_assoc
by (metis (no_types, lifting))
have 3: "natural_transformation A C
(BC.Map h ∘ AB.Map k) (BC.Map h ∘ AB.Map k) (BC.Map h ∘ AB.Map k)"
using k.natural_transformation_axioms h.natural_transformation_axioms
k h AB.ide_char BC.ide_char horizontal_composite
by metis
have 4: "natural_transformation C E
(DE.Map f ∘ CD.Map g) (DE.Map f ∘ CD.Map g) (DE.Map f ∘ CD.Map g)"
using f g f.natural_transformation_axioms g.natural_transformation_axioms
CD.ide_char DE.ide_char horizontal_composite
by metis
have "HOM A E (COMP E D A f (ASSOC D C B A g h k))
(HOM A E (ASSOC E D B A f (COMP D C B g h) k)
(COMP E B A (ASSOC E D C B f g h) k)) =
AE.MkIde (DE.Map f ∘ CD.Map g ∘ BC.Map h ∘ AB.Map k)"
proof -
have "functor B E (DE.Map f ∘ CD.Map g ∘ BC.Map h)"
using 2 natural_transformation_def by blast
moreover have "functor A D (CD.Map g ∘ BC.Map h ∘ AB.Map k)"
using k 1 AB.ide_char horizontal_composite k.natural_transformation_axioms
natural_transformation_def
by (metis (no_types, lifting))
ultimately show ?thesis
using f g h k 0 1 2 by (simp add: o_assoc)
qed
also have "... = HOM A E (ASSOC E D C A f g (COMP C B A h k))
(ASSOC E C B A (COMP E D C f g) h k)"
using f g h k 0 3 4 AC.ide_MkIde CE.ide_MkIde
by (simp add: o_assoc)
finally show "HOM A E (COMP E D A f (ASSOC D C B A g h k))
(HOM A E (ASSOC E D B A f (COMP D C B g h) k)
(COMP E B A (ASSOC E D C B f g h) k)) =
HOM A E (ASSOC E D C A f g (COMP C B A h k))
(ASSOC E C B A (COMP E D C f g) h k)"
by blast
qed
qed
lemma is_concrete_bicategory:
shows "concrete_bicategory OBJ HOM ID COMP ID ASSOC"
..
lemma unit_simp:
assumes "obj a"
shows "𝗂 a = a"
by (metis (mono_tags, lifting) 𝗂_def assms obj_char)
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 = hcomp f (hcomp g h)"
proof -
let ?A = "Src h" and ?B = "Trg h" and ?C = "Trg g" and ?D = "Trg f"
have 1: "Src f = Trg g ∧ Src g = Trg h"
using assms by (simp add: src_def trg_def)
interpret A: category ?A using assms Src_in_Obj [of h] by simp
interpret B: category ?B using assms Trg_in_Obj [of h] by simp
interpret C: category ?C using assms Trg_in_Obj [of g] by simp
interpret D: category ?D using assms Trg_in_Obj [of f] by simp
interpret AB: functor_category ?A ?B ..
interpret BC: functor_category ?B ?C ..
interpret CD: functor_category ?C ?D ..
interpret AD: functor_category ?A ?D ..
interpret BC_AB: product_category BC.comp AB.comp ..
interpret CD_BC_AB: product_category CD.comp BC_AB.comp ..
interpret f: "functor" ?C ?D ‹CD.Map (Map f)›
using assms 1 ide_char'' [of f] arr_char [of f] CD.ide_char by simp
interpret g: "functor" ?B ?C ‹BC.Map (Map g)›
using assms 1 ide_char'' [of g] arr_char [of g] CD.ide_char by simp
interpret h: "functor" ?A ?B ‹AB.Map (Map h)›
using assms 1 ide_char'' [of h] arr_char [of h] CD.ide_char by simp
have "𝖺 f g h = MkCell ?A ?D
(AD.MkArr (AD.Dom (Map f) ∘ AD.Dom (Map g) ∘ AD.Dom (Map h))
(AD.Cod (Map f) ∘ AD.Cod (Map g) ∘ AD.Cod (Map h))
(AD.Map (Map f) ∘ AD.Map (Map g) ∘ AD.Map (Map h)))"
using assms 1 ide_char'' 𝖺_simp_ide [of f g h]
arr_char [of f] arr_char [of g] arr_char [of h]
by simp
moreover have "AD.ide (AD.MkArr
(CD.Dom (Map f) ∘ BC.Dom (Map g) ∘ AB.Dom (Map h))
(CD.Cod (Map f) ∘ BC.Cod (Map g) ∘ AB.Cod (Map h))
(CD.Map (Map f) ∘ BC.Map (Map g) ∘ AB.Map (Map h)))"
proof -
have "functor ?A ?D (CD.Map (Map f) ∘ BC.Map (Map g) ∘ AB.Map (Map h))"
using f.functor_axioms g.functor_axioms h.functor_axioms functor_comp by blast
hence "AD.ide (AD.MkArr (CD.Map (Map f) ∘ BC.Map (Map g) ∘ AB.Map (Map h))
(CD.Map (Map f) ∘ BC.Map (Map g) ∘ AB.Map (Map h))
(CD.Map (Map f) ∘ BC.Map (Map g) ∘ AB.Map (Map h)))"
using AD.ide_char AD.null_char by simp
thus ?thesis
using assms 1
ide_char'' [of f] CD.ide_char [of "Map f"]
ide_char'' [of g] BC.ide_char [of "Map g"]
ide_char'' [of h] AB.ide_char [of "Map h"]
by presburger
qed
moreover have "arr (𝖺 f g h)"
using assms by simp
ultimately have "ide (𝖺 f g h)"
using ide_char''' [of "𝖺 f g h"] by auto
hence "𝖺 f g h = cod (𝖺 f g h)"
by simp
thus "𝖺 f g h = hcomp f (hcomp g h)"
using assms by simp
qed
lemma is_strict_bicategory:
shows "strict_bicategory vcomp hcomp 𝖺 𝗂 src trg"
proof -
have "⋀f :: ('a comp, ('a, 'a) functor_category.arr) cell. ide f ⟹ hcomp f (src f) = f"
proof -
fix f :: "('a comp, ('a, 'a) functor_category.arr) cell"
assume f: "ide f"
let ?A = "Src f" and ?B = "Trg f"
interpret A: category ?A
using f Src_in_Obj [of f] by simp
interpret B: category ?B
using f Trg_in_Obj [of f] by simp
interpret AA: functor_category ?A ?A ..
interpret AB: functor_category ?A ?B ..
have 1: "functor ?A ?B (AB.Cod (Map f)) ∧ functor ?A ?B (AB.Dom (Map f)) ∧
functor ?A ?B (AB.Map (Map f))"
using f ide_char''' AB.ide_char [of "Map f"] ide_char'' [of f] arr_char [of f]
by auto
have "hcomp f (src f) = MkCell ?A ?B (Map f)"
unfolding hcomp_def src_def
using f 1 AB.arr_char AB.null_char AB.ide_char
obj_MkObj [of "Src f"] obj_def functor_is_transformation ide_char'''
AB.ide_MkIde Src_in_Obj [of f] obj_MkObj obj_def AB.null_char arr_Map [of f]
A.functor_axioms AB.MkArr_Map arr_Map
by auto
also have "... = f"
using f MkCell_Map [of f] not_arr_null ideD(1) [of f] by fastforce
finally show "hcomp f (src f) = f" by blast
qed
moreover have
"⋀f :: ('a comp, ('a, 'a) functor_category.arr) cell. ide f ⟹ hcomp (trg f) f = f"
proof -
fix f :: "('a comp, ('a, 'a) functor_category.arr) cell"
assume f: "ide f"
let ?A = "Src f" and ?B = "Trg f"
interpret A: category ?A
using f Src_in_Obj [of f] by simp
interpret B: category ?B
using f Trg_in_Obj [of f] by simp
interpret BB: functor_category ?B ?B ..
interpret AB: functor_category ?A ?B ..
have 1: "functor ?A ?B (AB.Cod (Map f)) ∧ functor ?A ?B (AB.Dom (Map f)) ∧
functor ?A ?B (AB.Map (Map f))"
using f ide_char''' AB.ide_char [of "Map f"] ide_char'' [of f] arr_char [of f]
by auto
have "hcomp (trg f) f = MkCell ?A ?B (Map f)"
unfolding hcomp_def trg_def
using f 1 AB.arr_char AB.null_char AB.ide_char
obj_MkObj [of "Trg f"] obj_def functor_is_transformation ide_char'''
AB.ide_MkIde Trg_in_Obj [of f] obj_MkObj obj_def AB.null_char arr_Map [of f]
B.functor_axioms AB.MkArr_Map arr_Map
by auto
also have "... = f"
using f MkCell_Map [of f] not_arr_null ideD(1) [of f] by fastforce
finally show "hcomp (trg f) f = f" by blast
qed
moreover have "⋀a. obj a ⟹ ide (𝗂 a)"
using 𝗂_def by (metis (mono_tags, lifting) obj_MkObj_Src objE obj_def)
moreover have "⋀(f :: ('a comp, ('a, 'a) functor_category.arr) cell) g h.
⟦ ide f; ide g; ide h; src f = trg g; src g = trg h ⟧ ⟹ ide (𝖺 f g h)"
by (simp add: assoc_simp)
ultimately show ?thesis
using is_strict_if by blast
qed
sublocale strict_bicategory vcomp hcomp 𝖺 𝗂 src trg
using is_strict_bicategory by simp
end
end