Theory Category3.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 "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.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 "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 is_extensional 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 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 "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"
      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: "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.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 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 B F ?a'»"
            using g a a' by auto
          hence "f. «f : ?a A ?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 is_extensional
          by (auto simp add: f_inv_into_f)
        show "?G  F = A.map"
          using inj surj A.is_extensional 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 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"
          by (auto simp add: is_extensional)
      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 "isomorphic_categories C CC.COMP"
      ..

  end

end