# Theory Functor

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

chapter Functor

theory Functor
imports Category ConcreteCategory DualCategory InitialTerminal
begin

text‹
One advantage of the ``object-free'' definition of category is that a functor
from category A› to category B› is simply a function from the type
of arrows of A› to the type of arrows of B› that satisfies certain
conditions: namely, that arrows are mapped to arrows, non-arrows are mapped to
null›, and domains, codomains, and composition of arrows are preserved.
›

locale "functor" =
A: category A +
B: category B
for A :: "'a comp"      (infixr "A" 55)
and B :: "'b comp"      (infixr "B" 55)
and F :: "'a  'b" +
assumes is_extensional: "¬A.arr f  F f = B.null"
and preserves_arr: "A.arr f  B.arr (F f)"
and preserves_dom [iff]: "A.arr f  B.dom (F f) = F (A.dom f)"
and preserves_cod [iff]: "A.arr f  B.cod (F f) = F (A.cod f)"
and preserves_comp [iff]: "A.seq g f  F (g A f) = F g B F f"
begin

notation A.in_hom     ("«_ : _ A _»")
notation B.in_hom     ("«_ : _ B _»")

lemma preserves_hom [intro]:
assumes "«f : a A b»"
shows "«F f : F a B F b»"
using assms B.in_homI
by (metis A.in_homE preserves_arr preserves_cod preserves_dom)

text‹
The following, which is made possible through the presence of null›,
allows us to infer that the subterm @{term f} denotes an arrow if the
term @{term "F f"} denotes an arrow.  This is very useful, because otherwise
doing anything with @{term f} would require a separate proof that it is an arrow
by some other means.
›

lemma preserves_reflects_arr [iff]:
shows "B.arr (F f)  A.arr f"
using preserves_arr is_extensional B.not_arr_null by metis

lemma preserves_seq [intro]:
assumes "A.seq g f"
shows "B.seq (F g) (F f)"
using assms by auto

lemma preserves_ide [simp]:
assumes "A.ide a"
shows "B.ide (F a)"
using assms A.ide_in_hom B.ide_in_hom by auto

lemma preserves_iso [simp]:
assumes "A.iso f"
shows "B.iso (F f)"
using assms A.inverse_arrowsE
apply (elim A.isoE A.inverse_arrowsE A.seqE A.ide_compE)
by (metis A.arr_dom_iff_arr B.ide_dom B.inverse_arrows_def B.isoI preserves_arr
preserves_comp preserves_dom)

lemma preserves_isomorphic:
assumes "A.isomorphic a b"
shows "B.isomorphic (F a) (F b)"
by (meson A.isomorphic_def B.isomorphic_def assms preserves_hom preserves_iso)

lemma preserves_section_retraction:
assumes "A.ide (A e m)"
shows "B.ide (B (F e) (F m))"
using assms by (metis A.ide_compE preserves_comp preserves_ide)

lemma preserves_section:
assumes "A.section m"
shows "B.section (F m)"
using assms preserves_section_retraction by blast

lemma preserves_retraction:
assumes "A.retraction e"
shows "B.retraction (F e)"
using assms preserves_section_retraction by blast

lemma preserves_inverse_arrows:
assumes "A.inverse_arrows f g"
shows "B.inverse_arrows (F f) (F g)"
using assms A.inverse_arrows_def B.inverse_arrows_def preserves_section_retraction
by simp

lemma preserves_inv:
assumes "A.iso f"
shows "F (A.inv f) = B.inv (F f)"
using assms preserves_inverse_arrows A.inv_is_inverse B.inv_is_inverse
B.inverse_arrow_unique
by blast

lemma preserves_iso_in_hom [intro]:
assumes "A.iso_in_hom f a b"
shows "B.iso_in_hom (F f) (F a) (F b)"
using assms preserves_hom preserves_iso by blast

end

locale endofunctor =
"functor" A A F
for A :: "'a comp"     (infixr "" 55)
and F :: "'a  'a"

locale faithful_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a  'b" +
assumes is_faithful: " A.par f f'; F f = F f'   f = f'"
begin

lemma locally_reflects_ide:
assumes "«f : a A a»" and "B.ide (F f)"
shows "A.ide f"
using assms is_faithful
by (metis A.arr_dom_iff_arr A.cod_dom A.dom_dom A.in_homE B.comp_ide_self
B.ide_self_inverse B.comp_arr_inv A.ide_cod preserves_dom)

end

locale full_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a  'b" +
assumes is_full: " A.ide a; A.ide a'; «g : F a' B F a»   f. «f : a' A a»  F f = g"

locale fully_faithful_functor =
faithful_functor A B F +
full_functor A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a  'b"
begin

lemma reflects_iso:
assumes "«f : a' A a»" and "B.iso (F f)"
shows "A.iso f"
proof -
from assms obtain g' where g': "B.inverse_arrows (F f) g'" by blast
have 1: "«g' : F a B F a'»"
using assms g' by (metis B.inv_in_hom B.inverse_unique preserves_hom)
from this obtain g where g: "«g : a A a'»  F g = g'"
using assms(1) is_full by (metis A.arrI A.ide_cod A.ide_dom A.in_homE)
have "A.inverse_arrows f g"
using assms 1 g g' A.inverse_arrowsI
by (metis A.arr_iff_in_hom A.dom_comp A.in_homE A.seqI' B.inverse_arrowsE
A.cod_comp locally_reflects_ide preserves_comp)
thus ?thesis by auto
qed

lemma reflects_isomorphic:
assumes "A.ide f" and "A.ide f'" and "B.isomorphic (F f) (F f')"
shows "A.isomorphic f f'"
proof -
obtain ψ where ψ: "B.in_hom ψ (F f) (F f')  B.iso ψ"
using assms B.isomorphic_def by auto
obtain φ where φ: "A.in_hom φ f f'  F φ = ψ"
using assms ψ is_full by blast
have "A.iso φ"
using φ ψ reflects_iso by auto
thus ?thesis
using φ A.isomorphic_def by auto
qed

end

locale embedding_functor = "functor" A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a  'b" +
assumes is_embedding: " A.arr f; A.arr f'; F f = F f'   f = f'"

sublocale embedding_functor  faithful_functor
using is_embedding by (unfold_locales, blast)

context embedding_functor
begin

lemma reflects_ide:
assumes "B.ide (F f)"
shows "A.ide f"
using assms is_embedding A.ide_in_hom B.ide_in_hom
by (metis A.in_homE B.in_homE A.ide_cod preserves_cod preserves_reflects_arr)

end

locale full_embedding_functor =
embedding_functor A B F +
full_functor A B F
for A :: "'a comp"
and B :: "'b comp"
and F :: "'a  'b"

locale essentially_surjective_functor = "functor" +
assumes essentially_surjective: "b. B.ide b  a. A.ide a  B.isomorphic (F a) b"

locale constant_functor =
A: category A +
B: category B
for A :: "'a comp"
and B :: "'b comp"
and b :: 'b +
assumes value_is_ide: "B.ide b"
begin

definition map
where "map f = (if A.arr f then b else B.null)"

lemma map_simp [simp]:
assumes "A.arr f"
shows "map f = b"
using assms map_def by auto

lemma is_functor:
shows "functor A B map"
using map_def value_is_ide by (unfold_locales, auto)

end

sublocale constant_functor  "functor" A B map
using is_functor by auto

locale identity_functor =
C: category C
for C :: "'a comp"
begin

definition map :: "'a  'a"
where "map f = (if C.arr f then f else C.null)"

lemma map_simp [simp]:
assumes "C.arr f"
shows "map f = f"
using assms map_def by simp

sublocale "functor" C C map
using C.arr_dom_iff_arr C.arr_cod_iff_arr
by (unfold_locales; auto simp add: map_def)

lemma is_functor:
shows "functor C C map"
..

sublocale fully_faithful_functor C C map
using C.arrI by unfold_locales auto

lemma is_fully_faithful:
shows
..

end

text ‹
It is convenient to have an easy way to obtain from a category the identity functor
on that category. The following declaration causes the definitions and facts from the
@{locale identity_functor} locale to be inherited by the @{locale category} locale,
including the function @{term map} on arrows that represents the identity functor.
This makes it generally unnecessary to give explicit interpretations of
@{locale identity_functor}.
›

sublocale category  identity_functor C ..

text‹
Composition of functors coincides with function composition, thanks to the
magic of null›.
›

lemma functor_comp:
assumes "functor A B F" and "functor B C G"
shows "functor A C (G o F)"
proof -
interpret F: "functor" A B F using assms(1) by auto
interpret G: "functor" B C G using assms(2) by auto
show "functor A C (G o F)"
using F.preserves_arr F.is_extensional G.is_extensional by (unfold_locales, auto)
qed

locale composite_functor =
F: "functor" A B F +
G: "functor" B C G
for A :: "'a comp"
and B :: "'b comp"
and C :: "'c comp"
and F :: "'a  'b"
and G :: "'b  'c"
begin

abbreviation map
where "map  G o F"

sublocale "functor" A C G o F
using functor_comp F.functor_axioms G.functor_axioms by blast

lemma is_functor:
shows "functor A C (G o F)"
..

end

lemma comp_functor_identity [simp]:
assumes "functor A B F"
shows
proof
interpret "functor" A B F using assms by blast
show "x. (F o A.map) x = F x"
using A.map_def is_extensional by simp
qed

lemma comp_identity_functor [simp]:
assumes "functor A B F"
shows
proof
interpret "functor" A B F using assms by blast
show "x. (B.map o F) x = F x"
using B.map_def by (metis comp_apply is_extensional preserves_arr)
qed

lemma faithful_functors_compose:
assumes "faithful_functor A B F" and "faithful_functor B C G"
shows "faithful_functor A C (G o F)"
proof -
interpret F: faithful_functor A B F
using assms(1) by simp
interpret G: faithful_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "faithful_functor A C (G o F)"
proof
show "f f'. F.A.par f f'; map f = map f'  f = f'"
using F.is_faithful G.is_faithful
by (metis (mono_tags, lifting) F.preserves_arr F.preserves_cod F.preserves_dom o_apply)
qed
qed

lemma full_functors_compose:
assumes "full_functor A B F" and "full_functor B C G"
shows "full_functor A C (G o F)"
proof -
interpret F: full_functor A B F
using assms(1) by simp
interpret G: full_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "full_functor A C (G o F)"
proof
show "a a' g. F.A.ide a; F.A.ide a'; «g : map a'  map a»
f. F.A.in_hom f a' a  map f = g"
using F.is_full G.is_full
by (metis F.preserves_ide o_apply)
qed
qed

lemma fully_faithful_functors_compose:
assumes  and
shows "full_functor A C (G o F)"
proof -
interpret F: fully_faithful_functor A B F
using assms(1) by simp
interpret G: fully_faithful_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
interpret faithful_functor A C G o F
using F.faithful_functor_axioms G.faithful_functor_axioms faithful_functors_compose
by blast
interpret full_functor A C G o F
using F.full_functor_axioms G.full_functor_axioms full_functors_compose
by blast
show "full_functor A C (G o F)" ..
qed

lemma embedding_functors_compose:
assumes "embedding_functor A B F" and "embedding_functor B C G"
shows "embedding_functor A C (G o F)"
proof -
interpret F: embedding_functor A B F
using assms(1) by simp
interpret G: embedding_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "embedding_functor A C (G o F)"
proof
show "f f'. F.A.arr f; F.A.arr f'; map f = map f'  f = f'"
qed
qed

lemma full_embedding_functors_compose:
assumes  and
shows "full_embedding_functor A C (G o F)"
proof -
interpret F: full_embedding_functor A B F
using assms(1) by simp
interpret G: full_embedding_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
interpret embedding_functor A C G o F
using F.embedding_functor_axioms G.embedding_functor_axioms embedding_functors_compose
by blast
interpret full_functor A C G o F
using F.full_functor_axioms G.full_functor_axioms full_functors_compose
by blast
show "full_embedding_functor A C (G o F)" ..
qed

lemma essentially_surjective_functors_compose:
assumes  and
shows "essentially_surjective_functor A C (G o F)"
proof -
interpret F: essentially_surjective_functor A B F
using assms(1) by simp
interpret G: essentially_surjective_functor B C G
using assms(2) by simp
interpret composite_functor A B C F G ..
show "essentially_surjective_functor A C (G o F)"
proof
show "c. G.B.ide c  a. F.A.ide a  G.B.isomorphic (map a) c"
proof -
fix c
assume c: "G.B.ide c"
obtain b where b: "F.B.ide b  G.B.isomorphic (G b) c"
using c G.essentially_surjective by auto
obtain a where a: "F.A.ide a  F.B.isomorphic (F a) b"
using b F.essentially_surjective by auto
have "G.B.isomorphic (map a) c"
proof -
have "G.B.isomorphic (G (F a)) (G b)"
using a G.preserves_iso G.B.isomorphic_def by blast
thus ?thesis
using b G.B.isomorphic_transitive by auto
qed
thus "a. F.A.ide a  G.B.isomorphic (map a) c"
using a by auto
qed
qed
qed

locale inverse_functors =
A: category A +
B: category B +
F: "functor" B A F +
G: "functor" A B G
for A :: "'a comp"      (infixr "A" 55)
and B :: "'b comp"      (infixr "B" 55)
and F :: "'b  'a"
and G :: "'a  'b" +
assumes inv:
and inv':
begin

lemma bij_betw_arr_sets:
shows "bij_betw F (Collect B.arr) (Collect A.arr)"
using inv inv'
apply (intro bij_betwI)
apply auto
using comp_eq_dest_lhs by force+

end

locale isomorphic_categories =
A: category A +
B: category B
for A :: "'a comp"      (infixr "A" 55)
and B :: "'b comp"      (infixr "B" 55) +
assumes iso: "F G. inverse_functors A B F G"

sublocale inverse_functors  isomorphic_categories A B
using inverse_functors_axioms by (unfold_locales, auto)

lemma inverse_functors_sym:
assumes "inverse_functors A B F G"
shows "inverse_functors B A G F"
proof -
interpret inverse_functors A B F G using assms by auto
show ?thesis using inv inv' by (unfold_locales, auto)
qed

text ‹
Inverse functors uniquely determine each other.
›

lemma inverse_functor_unique:
assumes "inverse_functors C D F G" and "inverse_functors C D F G'"
shows "G = G'"
proof -
interpret FG: inverse_functors C D F G using assms(1) by auto
interpret FG': inverse_functors C D F G' using assms(2) by auto
show "G = G'"
using FG.G.is_extensional FG'.G.is_extensional FG'.inv FG.inv'
by (metis FG'.G.functor_axioms FG.G.functor_axioms comp_assoc comp_identity_functor
comp_functor_identity)
qed

lemma inverse_functor_unique':
assumes "inverse_functors C D F G" and "inverse_functors C D F' G"
shows "F = F'"
using assms inverse_functors_sym inverse_functor_unique by blast

locale invertible_functor =
A: category A +
B: category B +
G: "functor" A B G
for A :: "'a comp"      (infixr "A" 55)
and B :: "'b comp"      (infixr "B" 55)
and G :: "'a  'b" +
assumes invertible: "F. inverse_functors A B F G"
begin

lemma has_unique_inverse:
shows "∃!F. inverse_functors A B F G"
using invertible inverse_functor_unique' by blast

definition inv
where "inv  THE F. inverse_functors A B F G"

interpretation inverse_functors A B inv G
using inv_def has_unique_inverse theI' [of "λF. inverse_functors A B F G"]
by simp

lemma inv_is_inverse:
shows "inverse_functors A B inv G" ..

sublocale fully_faithful_functor A B G
proof -
obtain F where F: "inverse_functors A B F G"
using invertible by auto
interpret FG: inverse_functors A B F G
using F by simp
show
proof
fix f f'
assume par: "A.par f f'" and eq: "G f = G f'"
show "f = f'"
using par eq FG.inv'
by (metis A.map_simp comp_apply)
next
fix a a' g
assume a: "A.ide a" and a': "A.ide a'" and g: "«g : G a B G a'»"
show "f. «f : a A a'»  G f = g"
by (metis A.ideD(1) A.map_simp B.arrI B.map_simp FG.F.preserves_hom FG.inv FG.inv'
a a' g o_apply)
qed
qed

lemma is_fully_faithful:
shows
..

lemma preserves_terminal:
assumes "A.terminal a"
shows "B.terminal (G a)"
proof
show 0: "B.ide (G a)" using assms G.preserves_ide A.terminal_def by blast
fix b :: 'b
assume b: "B.ide b"
show "∃!g. «g : b B G a»"
proof
let ?F = "SOME F. inverse_functors A B F G"
from invertible have F: "inverse_functors A B ?F G"
using someI_ex [of "λF. inverse_functors A B F G"] by fast
interpret inverse_functors A B ?F G using F by auto
let ?P = "λf. «f : ?F b A a»"
have 1: "∃!f. ?P f" using assms b A.terminal_def by simp
hence 2: "?P (THE f. ?P f)" by (metis (no_types, lifting) theI')
thus "«G (THE f. ?P f) : b B G a»"
using b apply (elim A.in_homE, intro B.in_homI, auto)
using B.ideD(1) B.map_simp comp_def inv by metis
hence 3: "«(THE f. ?P f) : ?F b A a»"
using assms 2 b F by simp
fix g :: 'b
assume g: "«g : b B G a»"
have "?F (G a) = a"
using assms(1) A.terminal_def inv' A.map_simp
by (metis 0 B.ideD(1) G.preserves_reflects_arr comp_eq_dest_lhs)
hence "«?F g : ?F b A a»"
using assms(1) g A.terminal_def inv
by (elim B.in_homE, auto)
hence "?F g = (THE f. ?P f)" using assms 1 3 A.terminal_def by blast
thus "g = G (THE f. ?P f)"
using inv g by (metis B.in_homE B.map_simp comp_def)
qed
qed

end

sublocale invertible_functor  inverse_functors A B inv G
using inv_is_inverse by simp

locale dual_functor =
F: "functor" A B F +
Aop: dual_category A +
Bop: dual_category B
for A :: "'a comp"      (infixr "A" 55)
and B :: "'b comp"      (infixr "B" 55)
and F :: "'a  'b"
begin

notation Aop.comp     (infixr "Aop" 55)
notation Bop.comp     (infixr "Bop" 55)

abbreviation map
where "map  F"

lemma is_functor:
shows "functor Aop.comp Bop.comp map"
using F.is_extensional by (unfold_locales, auto)

end

sublocale dual_functor  "functor" Aop.comp Bop.comp map
using is_functor by auto

text ‹
A bijection from a set S› to the set of arrows of a category C› induces an isomorphic
copy of C› having S› as its set of arrows, assuming that there exists some n ∉ S›
to serve as the null.
›

context category
begin

lemma bij_induces_invertible_functor:
assumes "bij_betw φ S (Collect arr)" and "n  S"
shows "C'. Collect (partial_composition.arr C') = S
invertible_functor C' C (λi. if partial_composition.arr C' i then φ i else null)"
proof -
define ψ where "ψ = (λf. if arr f then inv_into S φ f else n)"
have ψ: "bij_betw ψ (Collect arr) S"
using assms(1) ψ_def bij_betw_inv_into
by (metis (no_types, lifting) bij_betw_cong mem_Collect_eq)
have φ_ψ [simp]: "f. arr f  φ (ψ f) = f"
using assms(1) ψ ψ_def bij_betw_inv_into_right by fastforce
have ψ_φ [simp]: "i. i  S  ψ (φ i) = i"
unfolding ψ_def
using assms(1) ψ bij_betw_inv_into_left [of φ S "Collect arr"]
by (metis bij_betw_def image_eqI mem_Collect_eq)
define C' where "C' = (λi j. if i  S  j  S  seq (φ i) (φ j) then ψ (φ i  φ j) else n)"
interpret C': partial_composition C'
using assms(1-2) C'_def ψ_def
by unfold_locales metis
have null_char: "C'.null = n"
using assms(1-2) C'_def ψ_def C'.null_eqI by metis
have ide_char: "i. C'.ide i  i  S  ide (φ i)"
proof
fix i
assume i: "C'.ide i"
show "i  S  ide (φ i)"
proof (unfold ide_def, intro conjI)
show 1: "φ i  φ i  null"
using i assms(1) C'.ide_def C'_def null_char by auto
show 2: "i  S"
using 1 assms(1) by (metis C'.ide_def C'_def i)
show "f. (f  φ i  null  f  φ i = f)  (φ i  f  null  φ i  f = f)"
proof (intro allI conjI impI)
show "f. f  φ i  null  f  φ i = f"
proof -
fix f
assume f: "f  φ i  null"
hence 1: "arr f  arr (φ i)  seq f (φ i)"
by (meson seqE ext)
have "f  φ i = φ (C' (ψ f) i)"
using 1 2 C'_def null_char
by (metis (no_types, lifting) φ_ψ ψ bij_betw_def image_eqI mem_Collect_eq)
also have "... = f"
by (metis 1 C'.ide_def C'_def φ_ψ ψ assms(2) bij_betw_def i image_eqI
mem_Collect_eq null_char)
finally show "f  φ i = f" by simp
qed
show "f. φ i  f  null  φ i  f = f"
proof -
fix f
assume f: "φ i  f  null"
hence 1: "arr f  arr (φ i)  seq (φ i) f"
by (meson seqE ext)
show "φ i  f = f"
using 1 2 C'_def null_char ψ
by (metis (no_types, lifting) f. f  φ i  null  f  φ i = f
ide_char' codomains_null comp_cod_arr has_codomain_iff_arr
comp_ide_arr)
qed
qed
qed
next
fix i
assume i: "i  S  ide (φ i)"
have "ψ (φ i)  S"
using i assms(1)
by (metis ψ bij_betw_def ideD(1) image_eqI mem_Collect_eq)
show "C'.ide i"
using assms(2) i C'_def null_char comp_arr_ide comp_ide_arr
apply (unfold C'.ide_def, intro conjI allI impI)
apply auto[1]
by force+
qed
have dom: "i. i  S  ψ (dom (φ i))  C'.domains i"
proof -
fix i
assume i: "i  S"
have 1: "C'.ide (ψ (dom (φ i)))"
by (metis φ_ψ ψ ψ_φ ψ_def arr_dom assms(2) bij_betw_def i ide_char ide_dom
image_eqI mem_Collect_eq)
moreover have "C' i (ψ (dom (φ i)))  C'.null"
by (metis C'_def φ_ψ ψ_φ ψ_def assms(2) calculation comp_arr_dom i ide_char
null_char)
ultimately show "ψ (dom (φ i))  C'.domains i"
using C'.domains_def by simp
qed
have cod: "i. i  S  ψ (cod (φ i))  C'.codomains i"
proof -
fix i
assume i: "i  S"
have 1: "C'.ide (ψ (cod (φ i)))"
by (metis φ_ψ ψ ψ_φ ψ_def arr_cod assms(2) bij_betw_def i ide_char ide_cod
image_eqI mem_Collect_eq)
moreover have "C' (ψ (cod (φ i))) i  C'.null"
by (metis 1 C'_def φ_ψ ψ_φ ψ_def assms(2) comp_cod_arr i ide_char null_char)
ultimately show "ψ (cod (φ i))  C'.codomains i"
using C'.codomains_def by simp
qed
have arr_char: "i. C'.arr i  i  S"
by (metis (mono_tags, lifting) C'.arr_def C'.codomains_def C'.domains_def
C'_def assms(2) dom mem_Collect_eq null_char C'.cod_in_codomains C'.dom_in_domains)
have seq_char: "i j. C'.seq i j  i  S  j  S  seq (φ i) (φ j)"
using assms(1-2) C'_def arr_char null_char
apply simp
using ψ bij_betw_apply by fastforce
interpret C': category C'
proof
show "g f. C' g f  C'.null  C'.seq g f"
using C'_def null_char seq_char by fastforce
show "f. (C'.domains f  {}) = (C'.codomains f  {})"
using dom cod null_char arr_char C'.arr_def by blast
show "h g f. C'.seq h g; C'.seq (C' h g) f  C'.seq g f"
using seq_char
apply simp
using C'_def by fastforce
show "h g f. C'.seq h (C' g f); C'.seq g f  C'.seq h g"
using seq_char
apply simp
using C'_def by fastforce
show "g f h. C'.seq g f; C'.seq h g  C'.seq (C' h g) f"
using seq_char arr_char
apply simp
using C'_def by auto
show "g f h. C'.seq g f; C'.seq h g  C' (C' h g) f = C' h (C' g f)"
using seq_char arr_char C'_def comp_assoc assms(2)
apply simp by presburger
qed
have dom_char: "C'.dom = (λi. if i  S then ψ (dom (φ i)) else n)"
using dom arr_char null_char C'.dom_eqI' C'.arr_def C'.dom_def by metis
have cod_char: "C'.cod = (λi. if i  S then ψ (cod (φ i)) else n)"
using cod arr_char null_char C'.cod_eqI' C'.arr_def C'.cod_def by metis
interpret φ: "functor" C' C λi. if C'.arr i then φ i else null
using arr_char null_char dom_char cod_char seq_char φ_ψ ψ_φ ψ_def C'.not_arr_null C'_def
C'.arr_dom C'.arr_cod
apply unfold_locales
apply simp_all
by metis+
interpret ψ: "functor" C C' ψ
using ψ_def null_char arr_char
apply unfold_locales
apply simp
apply (metis (no_types, lifting) ψ bij_betw_def image_eqI mem_Collect_eq)
apply (metis (no_types, lifting) φ_ψ ψ bij_betw_def dom_char image_eqI mem_Collect_eq)
apply (metis (no_types, lifting) φ_ψ ψ bij_betw_def cod_char image_eqI mem_Collect_eq)
by (metis (no_types, lifting) C'_def φ_ψ ψ bij_betw_def seqE image_eqI mem_Collect_eq)
interpret φψ: inverse_functors C' C ψ λi. if C'.arr i then φ i else null
proof
show "ψ  (λi. if C'.arr i then φ i else null) = C'.map"
by (auto simp add: C'.is_extensional ψ.is_extensional arr_char)
show "(λi. if C'.arr i then φ i else null)  ψ = map"
qed
have "invertible_functor C' C (λi. if C'.arr i then φ i else null)"
using φψ.inverse_functors_axioms by unfold_locales auto
thus ?thesis
using arr_char by blast
qed

corollary (in category) finite_imp_ex_iso_nat_comp:
assumes "finite (Collect arr)"
shows "C' :: nat comp. isomorphic_categories C' C"
proof -
obtain n :: nat and φ where φ: "bij_betw φ {0..<n} (Collect arr)"
using assms ex_bij_betw_nat_finite by blast
obtain C' where C': "Collect (partial_composition.arr C') = {0..<n}
invertible_functor C' (⋅)
(λi. if partial_composition.arr C' i then φ i else null)"
using φ bij_induces_invertible_functor [of φ "{0..<n}"] by auto
interpret φ: invertible_functor C' C λi. if partial_composition.arr C' i then φ i else null
using C' by simp
show ?thesis
using φ.isomorphic_categories_axioms by blast
qed

end

text ‹
We now prove the result, advertised earlier in theory ConcreteCategory›,
that any category is in fact isomorphic to the concrete category formed from it in
the obvious way.
›

context category
begin

interpretation CC: concrete_category Collect ide hom id λ_ _ _ g f. g  f
using comp_arr_dom comp_cod_arr comp_assoc
by (unfold_locales, auto)

interpretation F: "functor" C CC.COMP
λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null
by (unfold_locales, auto simp add: in_homI)

interpretation G: "functor" CC.COMP C λF. if CC.arr F then CC.Map F else null
using CC.Map_in_Hom CC.seq_char
by (unfold_locales, auto)

interpretation FG: inverse_functors C CC.COMP
λF. if CC.arr F then CC.Map F else null
λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null
proof
show "(λF. if CC.arr F then CC.Map F else null)
(λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null) =
map"
using CC.arr_char map_def by fastforce
show "(λf. if arr f then CC.MkArr (dom f) (cod f) f else CC.null)
(λF. if CC.arr F then CC.Map F else null) =
CC.map"
using CC.MkArr_Map G.preserves_arr G.preserves_cod G.preserves_dom
CC.is_extensional
by auto
qed

theorem is_isomorphic_to_concrete_category:
shows
..

end

end