Quelle  Functor.thy

(*  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 extensionality: "¬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 extensionality 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'"
      by (metis A.isomorphic_def B.isomorphicE assms(1-3) is_full reflects_iso)

  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 "fully_faithful_functor C C map"
      ..

  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.extensionality G.extensionality 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 "F o identity_functor.map A = F"
  proof
    interpret "functor" A B F using assms by blast
    show "∧x. (F o A.map) x = F x"
      using A.map_def extensionality by simp
  qed

  lemma comp_identity_functor [simp]:
  assumes "functor A B F"
  shows "identity_functor.map B o F = F"
  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 extensionality 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 "fully_faithful_functor A B F" and "fully_faithful_functor B C G"
  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'"
        by (simp add: F.is_embedding G.is_embedding)
    qed
  qed

  lemma full_embedding_functors_compose:
  assumes "full_embedding_functor A B F" and "full_embedding_functor B C G"
  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 "essentially_surjective_functor A B F" and "essentially_surjective_functor B C G"
  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"
        by (metis F.essentially_surjective G.B.isomorphic_transitive
            G.essentially_surjective G.preserves_isomorphic comp_def)
    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: "G o F = identity_functor.map B"
  and inv': "F o G = identity_functor.map A"
  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.extensionality FG'.G.extensionality 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 inverse_functors A B inv G
      using inv_is_inverse by simp

    lemma is_surjective_on_objects:
    shows "G ` Collect A.ide 🪙 Collect B.ide"
      by (metis (no_types, lifting) B.category_axioms B.map_simp
          CollectD CollectI F.preserves_ide category.ideD(1) image_eqI
          inv o_apply subsetI)

    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 "fully_faithful_functor A B G"
      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 "fully_faithful_functor A B G"
      ..

    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

  context full_embedding_functor
  begin

    lemma is_invertible_if_surjective_on_objects:
    assumes "F ` Collect A.ide 🪙 Collect B.ide"
    shows "invertible_functor A B F"
    and "inverse_functors A B (λy. if B.arr y then inv_into (Collect A.arr) F y else A.null) F"
    proof -
      have *: "F ` Collect A.ide = Collect B.ide"
        using assms preserves_reflects_arr by auto
      have inj: "inj_on F (Collect A.arr)"
        using is_embedding inj_on_def by blast
      have inj': "inj_on F (Collect A.ide)"
        by (simp add: inj_on_def is_embedding)
      have surj: "F ` Collect A.arr = Collect B.arr"
      proof
        show "F ` Collect A.arr ⊆ Collect B.arr"
          using preserves_reflects_arr by auto
        show "Collect B.arr ⊆ F ` Collect A.arr"
        proof
          fix g
          assume g: "g ∈ Collect B.arr"
          let ?a = "inv_into (Collect A.ide) F (B.dom g)"
          let ?a' = "inv_into (Collect A.ide) F (B.cod g)"
          have a: "A.ide ?a ∧ F ?a = B.dom g"
            using * g by (simp add: f_inv_into_f reflects_ide)
          have a': "A.ide ?a' ∧ F ?a' = B.cod g"
            using * g by (simp add: f_inv_into_f reflects_ide)
          have "«g : F ?a →<sub>B</sub> F ?a'¬"
            using g a a' by auto
          hence "∃f. «f : ?a →<sub>A</sub> ?a'¬ ∧ F f = g"
            using a a' is_full by blast
          thus "g ∈ F ` Collect A.arr" by blast
        qed
      qed
      let ?G = "λy. if B.arr y then inv_into (Collect A.arr) F y else A.null"
      show "inverse_functors A B ?G F"
      proof
        show "∧f. ¬ B.arr f ==> ?G f = A.null"
          by simp
        show 1: "∧f. B.arr f ==> A.arr (?G f)"
          using assms inj surj inv_into_into
          by (metis (full_types) mem_Collect_eq)
        show 2: "∧f. B.arr f ==> A.dom (?G f) = ?G (B.dom f)"
        proof -
          fix f
          assume f: "B.arr f"
          have "F (A.dom (?G f)) = B.dom f"
          proof -
            have "F (A.dom (?G f)) = B.dom (F (inv_into (Collect A.arr) F f))"
              using f 1 preserves_dom by simp
            also have "... = B.dom f"
              using f f_inv_into_f by (metis CollectI surj)
            finally show ?thesis by blast
          qed
          thus "A.dom (?G f) = ?G (B.dom f)"
            using f
            by (metis 1 A.arr_dom B.arr_dom inj inv_into_f_f mem_Collect_eq)
        qed
        show 3: "∧f. B.arr f ==> A.cod (?G f) = ?G (B.cod f)"
        proof -
          fix f
          assume f: "B.arr f"
          have "F (A.cod (?G f)) = B.cod f"
          proof -
            have "F (A.cod (?G f)) = B.cod (F (inv_into (Collect A.arr) F f))"
              using f 1 preserves_cod by simp
            also have "... = B.cod f"
              using f f_inv_into_f by (metis CollectI surj)
            finally show ?thesis by blast
          qed
          thus "A.cod (?G f) = ?G (B.cod f)"
            using f
            by (metis 1 A.arr_cod B.arr_cod inj inv_into_f_f mem_Collect_eq)
        qed
        fix f g
        assume fg: "B.seq g f"
        show "?G (B g f) = A (?G g) (?G f)"
          using assms fg 1 2 3 inj surj f_inv_into_f inj_on_def inv_into_into
                preserves_comp
          by (auto simp add: f_inv_into_f is_embedding)
        next
        show "F ∘ ?G = B.map"
          using inj surj f_inv_into_f A.not_arr_null B.map_def extensionality
          by (auto simp add: f_inv_into_f)
        show "?G ∘ F = A.map"
          using inj surj A.extensionality by auto
      qed
      hence "∃G. inverse_functors A B G F"
        by blast
      thus "invertible_functor A B F"
        using functor_axioms functor_def invertible_functor.intro
              invertible_functor_axioms.intro
        by blast
    qed

  end

  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 ‹⋅_A^op› 55)
    notation Bop.comp     (infixr ‹⋅_B^op› 55)

    abbreviation map
    where "map ≡ F"

    lemma is_functor:
    shows "functor Aop.comp Bop.comp map"
      using F.extensionality 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'.extensionality ψ.extensionality arr_char)
        show "(λi. if C'.arr i then φ i else null) ∘ ψ = map"
          by (auto simp add: extensionality)
      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.extensionality
        by auto
    qed

    theorem is_isomorphic_to_concrete_category:
    shows "isomorphic_categories C CC.COMP"
      ..

  end

end