Quelle  Colimit.thy

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

chapter Colimit

theory Colimit
imports Category3.Limit
begin

  text‹
 After mulling it over for a long time, I do not have any strong sense that it would be
 simpler or more useful to try to come up with some clever way of dualizing the material
 in @{theory Category3.Limit}, than just to do the dualization directly. This theory
 therefore contains (a portion of) such a direct dualization, including at least the general
 definitions of cocone and colimit, and including particular special cases of colimits
 that I have wanted to work with. I have omitted theorems about preservation of colimits
 for now.
 ›

section "Diagrams and Cocones"

  text‹
 A \emph{cocone} over a diagram ‹D: J → C› is a natural transformation
 from @{term D} to a constant functor. The value of the constant functor is
 the \emph{apex} of the cocone.
 ›

  locale cocone =
    C: category C +
    J: category J +
    D: diagram J C D +
    A: constant_functor J C a +
    natural_transformation J C D A.map χ
  for J :: "'j comp"      (infixr ‹⋅_J› 55)
  and C :: "'c comp"      (infixr ‹⋅› 55)
  and D :: "'j ==> 'c"
  and a :: 'c
  and χ :: "'j ==> 'c"
  begin

    lemma ide_apex:
    shows "C.ide a"
      using A.value_is_ide by auto

    lemma component_in_hom:
    assumes "J.arr j"
    shows "«χ j : D (J.dom j) → a¬"
      using assms by auto

    lemma dom_determines_component:
    assumes "J.arr j"
    shows "χ j = χ (J.dom j)"
      by (metis A.map_simp J.arr_dom_iff_arr J.dom_dom assms naturality1)

  end

  text‹
 A cocone over diagram @{term D} is transformed into a cocone over diagram @{term "D o F"}
 by pre-composing with @{term F}.
 ›

  lemma comp_cocone_functor:
  assumes "cocone J C D a χ" and "functor J' J F"
  shows "cocone J' C (D o F) a (χ o F)"
  proof -
    interpret χ: cocone J C D a χ using assms(1) by auto
    interpret F: "functor" J' J F using assms(2) by auto
    interpret A': constant_functor J' C a
      using χ.A.value_is_ide by unfold_locales auto
    have 1: "χ.A.map o F = A'.map"
      using χ.A.map_def A'.map_def χ.J.not_arr_null by auto
    interpret χ': natural_transformation J' C ‹D o F› A'.map ‹χ o F›
      using 1 horizontal_composite F.as_nat_trans.natural_transformation_axioms
            χ.natural_transformation_axioms
      by fastforce
    show "cocone J' C (D o F) a (χ o F)" ..
  qed

  text‹
 A cocone over diagram @{term D} can be transformed into a cocone over a diagram @{term D'}
 by pre-composing with a natural transformation from @{term D'} to @{term D}.
 ›

  lemma vcomp_transformation_cocone:
  assumes "cocone J C D a χ"
  and "natural_transformation J C D' D τ"
  shows "cocone J C D' a (vertical_composite.map J C τ χ)"
    by (meson assms(1,2) cocone.axioms(4,5) cocone.intro diagram.intro natural_transformation_def
        vertical_composite.intro vertical_composite.is_natural_transformation)

  context "functor"
  begin

    lemma preserves_cocones:
    fixes J :: "'j comp"
    assumes "cocone J A D a χ"
    shows "cocone J B (F o D) (F a) (F o χ)"
    proof -
      interpret χ: cocone J A D a χ using assms by auto
      interpret Fa: constant_functor J B ‹F a›
        using χ.ide_apex by unfold_locales auto
      have 1: "F o χ.A.map = Fa.map"
      proof
        fix f
        show "(F ∘ χ.A.map) f = Fa.map f"
          using extensionality Fa.extensionality χ.A.extensionality
          by (cases "χ.J.arr f", simp_all)
      qed
      interpret χ': natural_transformation J B ‹F o D› Fa.map ‹F o χ›
        using 1 horizontal_composite χ.natural_transformation_axioms
              as_nat_trans.natural_transformation_axioms
        by fastforce
      show "cocone J B (F o D) (F a) (F o χ)" ..
    qed

  end

  context diagram
  begin

    abbreviation cocone
    where "cocone a χ ≡ Colimit.cocone J C D a χ"

    abbreviation cocones :: "'c ==> ('j ==> 'c) set"
    where "cocones a ≡ { χ. cocone a χ }"

    text‹
 An arrow @{term "f ∈ C.hom a a'"} induces by composition a transformation from
 cocones with apex @{term a} to cocones with apex @{term a'}. This transformation
 is functorial in @{term f}.
 ›

    abbreviation cocones_map :: "'c ==> ('j ==> 'c) ==> ('j ==> 'c)"
    where "cocones_map f ≡ (λχ ∈ cocones (C.dom f). λj. if J.arr j then f ⋅ χ j else C.null)"

    lemma cocones_map_mapsto:
    assumes "C.arr f"
    shows "cocones_map f ∈
             extensional (cocones (C.dom f)) ∩ (cocones (C.dom f) → cocones (C.cod f))"
    proof
      show "cocones_map f ∈ extensional (cocones (C.dom f))" by blast
      show "cocones_map f ∈ cocones (C.dom f) → cocones (C.cod f)"
      proof
        fix χ
        assume "χ ∈ cocones (C.dom f)"
        hence χ: "cocone (C.dom f) χ" by auto
        interpret χ: cocone J C D ‹C.dom f› χ using χ by auto
        interpret B: constant_functor J C ‹C.cod f›
          using assms by unfold_locales auto
        have "cocone (C.cod f) (λj. if J.arr j then f ⋅ χ j else C.null)"
          using assms B.value_is_ide
          apply (unfold_locales, simp_all)
           apply (metis C.comp_assoc C.comp_cod_arr χ.dom_determines_component)
          by (simp add: C.comp_assoc)
        thus "(λj. if J.arr j then f ⋅ χ j else C.null) ∈ cocones (C.cod f)" by auto
      qed
    qed

    lemma cocones_map_ide:
    assumes "χ ∈ cocones a"
    shows "cocones_map a χ = χ"
    proof -
      interpret χ: cocone J C D a χ using assms by auto
      show ?thesis
        using assms χ.A.value_is_ide χ.preserves_hom C.comp_cod_arr χ.extensionality
        by auto
    qed

    lemma cocones_map_comp:
    assumes "C.seq g f"
    shows "cocones_map (g ⋅ f) = restrict (cocones_map g o cocones_map f) (cocones (C.dom f))"
    proof (intro restr_eqI)
      show "cocones (C.dom (g ⋅ f)) = cocones (C.dom f)" using assms by simp
      show "∧χ. χ ∈ cocones (C.dom (g ⋅ f)) ==>
                  (λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null) =
                  (cocones_map g o cocones_map f) χ"
      proof -
        fix χ
        assume χ: "χ ∈ cocones (C.dom (g ⋅ f))"
        show "(λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null) = (cocones_map g o cocones_map f) χ"
        proof -
          have "((cocones_map g) o (cocones_map f)) χ = cocones_map g (cocones_map f χ)"
            by force
          also have "... = (λj. if J.arr j
                                then g ⋅ (λj. if J.arr j then f ⋅ χ j else C.null) j
                                else C.null)"
          proof
            fix j
            have "cocone (C.cod f) (cocones_map f χ)"
              using assms χ cocones_map_mapsto by (elim C.seqE, force)
            thus "cocones_map g (cocones_map f χ) j =
                  (if J.arr j then g ⋅ (λj. if J.arr j then f ⋅ χ j else C.null) j else C.null)"
              using χ assms by auto
          qed
          also have "... = (λj. if J.arr j then (g ⋅ f) ⋅ χ j else C.null)"
            using C.comp_assoc by fastforce
          finally show ?thesis by auto
        qed
      qed
    qed

  end

  text‹
 Changing the apex of a cocone by post-composing with an arrow @{term f} commutes
 with changing the diagram of a cocone by pre-composing with a natural transformation.
 ›

  lemma cones_map_vcomp:
  assumes "diagram J C D" and "diagram J C D'"
  and "natural_transformation J C D D' τ"
  and "cone J C D a χ"
  and f: "partial_composition.in_hom C f a' a"
  shows "diagram.cones_map J C D' f (vertical_composite.map J C χ τ)
           = vertical_composite.map J C (diagram.cones_map J C D f χ) τ"
  proof -
    interpret D: diagram J C D using assms(1) by auto
    interpret D': diagram J C D' using assms(2) by auto
    interpret τ: natural_transformation J C D D' τ using assms(3) by auto
    interpret χ: cone J C D a χ using assms(4) by auto
    interpret τoχ: vertical_composite J C χ.A.map D D' χ τ ..
    interpret τoχ: cone J C D' a τoχ.map ..
    interpret χf: cone J C D a' ‹D.cones_map f χ›
      using f χ.cone_axioms D.cones_map_mapsto by blast
    interpret τoχf: vertical_composite J C χf.A.map D D' ‹D.cones_map f χ› τ ..
    interpret τoχ_f: cone J C D' a' ‹D'.cones_map f τoχ.map›
      using f τoχ.cone_axioms D'.cones_map_mapsto [of f] by blast
    write C (infixr ‹⋅› 55)
    show "D'.cones_map f τoχ.map = τoχf.map"
    proof (intro natural_transformation_eqI)
      show "natural_transformation J C χf.A.map D' (D'.cones_map f τoχ.map)" ..
      show "natural_transformation J C χf.A.map D' τoχf.map" ..
      show "∧j. D.J.ide j ==> D'.cones_map f τoχ.map j = τoχf.map j"
      proof -
        fix j
        assume j: "D.J.ide j"
        have "D'.cones_map f τoχ.map j = τoχ.map j ⋅ f"
          using f τoχ.cone_axioms τoχ.map_simp_2 τoχ.extensionality by auto
        also have "... = (τ j ⋅ χ (D.J.dom j)) ⋅ f"
          using j τoχ.map_simp_2 by simp
        also have "... = τ j ⋅ χ (D.J.dom j) ⋅ f"
          using D.C.comp_assoc by simp
        also have "... = τoχf.map j"
          using j f χ.cone_axioms τoχf.map_simp_2 by auto
        finally show "D'.cones_map f τoχ.map j = τoχf.map j" by auto
      qed
    qed
  qed

  section "Colimits"

  subsection "Colimit Cocones"

  text‹
 A \emph{colimit cocone} for a diagram @{term D} is a cocone @{term χ} over @{term D}
 with the couniversal property that any other cocone @{term χ'} over the diagram @{term D}
 factors uniquely through @{term χ}.
 ›

  locale colimit_cocone =
    C: category C +
    J: category J +
    D: diagram J C D +
    cocone J C D a χ
  for J :: "'j comp"      (infixr ‹⋅_J› 55)
  and C :: "'c comp"      (infixr ‹⋅› 55)
  and D :: "'j ==> 'c"
  and a :: 'c
  and χ :: "'j ==> 'c" +
  assumes is_couniversal: "cocone J C D a' χ' ==> ∃!f. «f : a → a'¬ ∧ D.cocones_map f χ = χ'"
  begin

    lemma is_cocone [simp]:
    shows "χ ∈ D.cocones a"
      using cocone_axioms by simp
    
    definition induced_arrow :: "'c ==> ('j ==> 'c) ==> 'c"
    where "induced_arrow a' χ' = (THE f. «f : a → a'¬ ∧ D.cocones_map f χ = χ')"

    lemma induced_arrowI:
    assumes χ': "χ' ∈ D.cocones a'"
    shows "«induced_arrow a' χ' : a → a'¬"
    and "D.cocones_map (induced_arrow a' χ') χ = χ'"
    proof -
      have "∃!f. «f : a → a'¬ ∧ D.cocones_map f χ = χ'"
        using assms χ' is_couniversal by simp
      hence 1: "«induced_arrow a' χ' : a → a'¬ ∧ D.cocones_map (induced_arrow a' χ') χ = χ'"
        using theI' [of "λf. «f : a → a'¬ ∧ D.cocones_map f χ = χ'"] induced_arrow_def
        by presburger
      show "«induced_arrow a' χ' : a → a'¬" using 1 by simp
      show "D.cocones_map (induced_arrow a' χ') χ = χ'" using 1 by simp
    qed

    lemma cocones_map_induced_arrow:
    shows "induced_arrow a' ∈ D.cocones a' → C.hom a a'"
    and "∧χ'. χ' ∈ D.cocones a' ==> D.cocones_map (induced_arrow a' χ') χ = χ'"
      using induced_arrowI by auto

    lemma induced_arrow_cocones_map:
    assumes "C.ide a'"
    shows "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
    and "∧f. «f : a → a'¬ ==> induced_arrow a' (D.cocones_map f χ) = f"
    proof -
      have a': "C.ide a'" using assms by (simp add: cone.ide_apex)
      have cocone_χ: "cocone J C D a χ" ..
      show "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
        using cocone_χ D.cocones_map_mapsto by blast
      fix f
      assume f: "«f : a → a'¬"
      show "induced_arrow a' (D.cocones_map f χ) = f"
      proof -
        have "D.cocones_map f χ ∈ D.cocones a'"
          using f cocone_χ D.cocones_map_mapsto by blast
        hence "∃!f'. «f' : a → a'¬ ∧ D.cocones_map f' χ = D.cocones_map f χ"
          using assms is_couniversal by auto
        thus ?thesis
          using f induced_arrow_def
                the1_equality
                  [of "λf'. «f' : a → a'¬ ∧ D.cocones_map f' χ = D.cocones_map f χ"]
          by presburger
      qed
    qed

    text‹
 For a colimit cocone @{term χ} with apex @{term a}, for each object @{term a'} the
 hom-set @{term "C.hom a a'"} is in bijective correspondence with the set of cocones
 with apex @{term a'}.
 ›

    lemma bij_betw_hom_and_cocones:
    assumes "C.ide a'"
    shows "bij_betw (λf. D.cocones_map f χ) (C.hom a a') (D.cocones a')"
    proof (intro bij_betwI)
      show "(λf. D.cocones_map f χ) ∈ C.hom a a' → D.cocones a'"
        using assms induced_arrow_cocones_map by blast
      show "induced_arrow a' ∈ D.cocones a' → C.hom a a'"
        using assms cocones_map_induced_arrow by blast
      show "∧f. f ∈ C.hom a a' ==> induced_arrow a' (D.cocones_map f χ) = f"
        using assms induced_arrow_cocones_map by blast
      show "∧χ'. χ' ∈ D.cocones a' ==> D.cocones_map (induced_arrow a' χ') χ = χ'"
        using assms cocones_map_induced_arrow by blast
    qed

    lemma induced_arrow_eqI:
    assumes "D.cocone a' χ'" and "«f : a → a'¬" and "D.cocones_map f χ = χ'"
    shows "induced_arrow a' χ' = f"
      using assms is_couniversal induced_arrow_def
            the1_equality [of "λf. f ∈ C.hom a a' ∧ D.cocones_map f χ = χ'" f]
      by simp

    lemma induced_arrow_self:
    shows "induced_arrow a χ = a"
    proof -
      have "«a : a → a¬ ∧ D.cocones_map a χ = χ"
        using ide_apex cocone_axioms D.cocones_map_ide by force
      thus ?thesis using induced_arrow_eqI cocone_axioms by auto
    qed

  end

  context diagram
  begin

    abbreviation colimit_cocone
    where "colimit_cocone a χ ≡ Colimit.colimit_cocone J C D a χ"

    text‹
 A diagram @{term D} has object @{term a} as a colimit if @{term a} is the apex
 of some colimit cocone over @{term D}.
 ›

    abbreviation has_as_colimit :: "'c ==> bool"
    where "has_as_colimit a ≡ (∃χ. colimit_cocone a χ)"

    abbreviation has_colimit
    where "has_colimit ≡ (∃a. has_as_colimit a)"

    definition some_colimit :: 'c
    where "some_colimit = (SOME a. has_as_colimit a)"

    definition some_colimit_cocone :: "'j ==> 'c"
    where "some_colimit_cocone = (SOME χ. colimit_cocone some_colimit χ)"

    lemma colimit_cocone_some_colimit_cocone:
    assumes has_colimit
    shows "colimit_cocone some_colimit some_colimit_cocone"
    proof -
      have "∃a. has_as_colimit a" using assms by simp
      hence "has_as_colimit some_colimit"
        using some_colimit_def someI_ex [of "λa. ∃χ. colimit_cocone a χ"] by simp
      thus "colimit_cocone some_colimit some_colimit_cocone"
        using assms some_colimit_cocone_def someI_ex [of "λχ. colimit_cocone some_colimit χ"]
        by simp
    qed

    lemma has_colimitE:
    assumes has_colimit
    obtains a χ where "colimit_cocone a χ"
      using assms someI_ex by blast

  end

  section "Special Kinds of Coimits"

  subsection "Coproducts"

  text‹
 A \emph{coproduct} in a category @{term C} is a colimit of a discrete diagram in @{term C}.
 ›

  context discrete_diagram
  begin

    abbreviation mkCocone
    where "mkCocone F ≡ (λj. if J.arr j then F j else C.null)"

    lemma cocone_mkCocone:
    assumes "C.ide a" and "∧j. J.arr j ==> «F j : D j → a¬"
    shows "cocone a (mkCocone F)"
    proof -
      interpret A: constant_functor J C a
         using assms(1) by unfold_locales auto
      show "cocone a (mkCocone F)"
        using assms(2) is_discrete
        apply unfold_locales
            apply auto
         apply (metis C.in_homE C.comp_cod_arr)
        using C.comp_arr_ide by fastforce
    qed

    lemma mkCocone_cocone:
    assumes "cocone a π"
    shows "mkCocone π = π"
    proof -
      interpret π: cocone J C D a π
        using assms by auto
      show "mkCocone π = π" using π.extensionality by auto
    qed

  end

  locale coproduct_cocone =
    J: category J +
    C: category C +
    D: discrete_diagram J C D +
    colimit_cocone J C D a π
  for J :: "'j comp"      (infixr ‹⋅_J› 55)
  and C :: "'c comp"      (infixr ‹⋅› 55)
  and D :: "'j ==> 'c"
  and a :: 'c
  and π :: "'j ==> 'c"
  begin

    lemma is_cocone:
    shows "D.cocone a π" ..

    lemma is_couniversal':
    assumes "C.ide b" and "∧j. J.arr j ==> «F j: D j → b¬"
    shows "∃!f. «f : a → b¬ ∧ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
    proof -
      let ?χ = "D.mkCocone F"
      interpret B: constant_functor J C b
        using assms(1) by unfold_locales auto
      have cocone_χ: "D.cocone b ?χ"
        using assms D.is_discrete D.cocone_mkCocone by blast
      interpret χ: cocone J C D b ?χ using cocone_χ by auto
      have "∃!f. «f : a → b¬ ∧ D.cocones_map f π = ?χ"
        using cocone_χ is_couniversal by force
      moreover have
           "∧f. «f : a → b¬ ==> D.cocones_map f π = ?χ ⟷ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
      proof -
        fix f
        assume f: "«f : a → b¬"
        show "D.cocones_map f π = ?χ ⟷ (∀j. J.arr j ⟶ f ⋅ π j = F j)"
        proof
          assume 1: "D.cocones_map f π = ?χ"
          show "∀j. J.arr j ⟶ f ⋅ π j = F j"
          proof -
            have "∧j. J.arr j ==> f ⋅ π j = F j"
            proof -
              fix j
              assume j: "J.arr j"
              have "f ⋅ π j = D.cocones_map f π j"
                using j f cocone_axioms by force
              also have "... = F j" using j 1 by simp
              finally show "f ⋅ π j = F j" by auto
            qed
            thus ?thesis by auto
          qed
          next
          assume 1: "∀j. J.arr j ⟶ f ⋅ π j = F j"
          show "D.cocones_map f π = ?χ"
            using 1 f is_cocone χ.extensionality D.is_discrete is_cocone cocone_χ by auto
        qed
      qed
      ultimately show ?thesis by blast
    qed

    abbreviation induced_arrow' :: "'c ==> ('j ==> 'c) ==> 'c"
    where "induced_arrow' b F ≡ induced_arrow b (D.mkCocone F)"

    lemma induced_arrowI':
    assumes "C.ide b" and "∧j. J.arr j ==> «F j : D j → b¬"
    shows "∧j. J.arr j ==> induced_arrow' b F ⋅ π j = F j"
    proof -
      interpret B: constant_functor J C b
        using assms(1) by unfold_locales auto
      interpret χ: cocone J C D b ‹D.mkCocone F›
        using assms D.cocone_mkCocone by blast
      have cocone_χ: "D.cocone b (D.mkCocone F)" ..
      hence 1: "D.cocones_map (induced_arrow' b F) π = D.mkCocone F"
        using induced_arrowI by blast
      fix j
      assume j: "J.arr j"
      have "induced_arrow' b F ⋅ π j = D.cocones_map (induced_arrow' b F) π j"
        using induced_arrowI(1) cocone_χ is_cocone extensionality by force
      also have "... = F j"
        using j 1 by auto
      finally show "induced_arrow' b F ⋅ π j = F j"
        by auto
    qed

  end

  context discrete_diagram
  begin

    lemma coproduct_coconeI:
    assumes "colimit_cocone a π"
    shows "coproduct_cocone J C D a π"
      by (meson assms discrete_diagram_axioms functor_axioms functor_def
          coproduct_cocone.intro)

  end

  context category
  begin

    definition has_as_coproduct
    where "has_as_coproduct J D a ≡ (∃π. coproduct_cocone J C D a π)"

    abbreviation has_coproduct
    where "has_coproduct J D ≡ ∃a. has_as_coproduct J D a"

    lemma coproduct_is_ide:
    assumes "has_as_coproduct J D a"
    shows "ide a"
    proof -
      obtain π where π: "coproduct_cocone J C D a π"
        using assms has_as_coproduct_def by blast
      interpret π: coproduct_cocone J C D a π
        using π by auto
      show ?thesis using π.ide_apex by auto
    qed

    text‹
 The reason why we assume @{term "I ≠ UNIV"} in the following is the same as
 for products.
 ›

    definition has_coproducts
    where "has_coproducts (I :: 'i set) ≡
             I ≠ UNIV ∧
             (∀J D. discrete_diagram J C D ∧ Collect (partial_composition.arr J) = I
                      ⟶ (∃a. has_as_coproduct J D a))"

    lemma has_coproductE:
    assumes "has_coproduct J D"
    obtains a π where "coproduct_cocone J C D a π"
      using assms has_as_coproduct_def by metis

  end

  subsection "Coequalizers"

  text‹
 An \emph{coequalizer} in a category @{term C} is a colimit of a parallel pair
 of arrows in @{term C}.
 ›

  context parallel_pair_diagram
  begin

    definition mkCocone
    where " mkCocone e ≡ λj. if J.arr j then if j = J.One then e else e ⋅ f0 else C.null"

    abbreviation is_coequalized_by
    where "is_coequalized_by e ≡ C.seq e f0 ∧ e ⋅ f0 = e ⋅ f1"

    abbreviation has_as_coequalizer
    where "has_as_coequalizer e ≡ colimit_cocone (C.cod e) (mkCocone e)"

    lemma cocone_mkCocone:
    assumes "is_coequalized_by e"
    shows "cocone (C.cod e) (mkCocone e)"
    proof -
      interpret E: constant_functor J.comp C ‹C.cod e›
        using assms by unfold_locales auto
      show "cocone (C.cod e) (mkCocone e)"
      proof (unfold_locales)
        show "∧j. ¬ J.arr j ==> mkCocone e j = C.null"
          using assms mkCocone_def by auto
        show "∧j. J.arr j ==> C.arr (mkCocone e j)"
          using assms mkCocone_def by auto
        show "∧j. J.arr j ==> mkCocone e (J.cod j) ⋅ map j = mkCocone e j"
          using assms mkCocone_def C.comp_arr_dom extensionality map_def is_parallel
          apply auto
          using parallel_pair.arr_char by auto
        show "∧j. J.arr j ==> E.map j ⋅ mkCocone e (J.dom j) = mkCocone e j"
          using assms mkCocone_def C.comp_cod_arr
          apply auto[1]
          using parallel_pair.arr_char by fastforce
      qed
    qed

    lemma is_coequalized_by_cocone:
    assumes "cocone a χ"
    shows "is_coequalized_by (χ (J.One))"
    proof -
      interpret χ: cocone J.comp C map a χ
        using assms by auto
      show ?thesis
        by (metis (no_types, lifting) J.arr_char J.cod_char J.dom_char χ.cocone_axioms
            χ.naturality2 χ.preserves_arr cocone.dom_determines_component map_simp(3-4))
    qed

    lemma mkCocone_cocone:
    assumes "cocone a χ"
    shows "mkCocone (χ J.One) = χ"
    proof -
      interpret χ: cocone J.comp C map a χ
        using assms by auto
      have 1: "is_coequalized_by (χ J.One)"
        using assms is_coequalized_by_cocone by blast
      show ?thesis
      proof
        fix j
        have "j = J.One ==> mkCocone (χ J.One) j = χ j"
          using mkCocone_def χ.extensionality by simp 
        moreover have "j = J.Zero ∨ j = J.j0 ∨ j = J.j1 ==> mkCocone (χ J.One) j = χ j"
          using J.arr_char J.cod_char J.dom_char J.seq_char mkCocone_def
                χ.naturality1 χ.naturality2 χ.A.map_simp map_def
          by (metis (lifting) map_simp(3))
        ultimately have "J.arr j ==> mkCocone (χ J.One) j = χ j"
          using J.arr_char by auto
        thus "mkCocone (χ J.One) j = χ j"
          using mkCocone_def χ.extensionality by fastforce
      qed
    qed

  end

  locale coequalizer_cocone =
    J: parallel_pair +
    C: category C +
    D: parallel_pair_diagram C f0 f1 +
    colimit_cocone J.comp C D.map "C.cod e" "D.mkCocone e"
  for C :: "'c comp"      (infixr ‹⋅› 55)
  and f0 :: 'c
  and f1 :: 'c
  and e :: 'c
  begin

    lemma coequalizes:
    shows "D.is_coequalized_by e"
    proof
      show "C.seq e f0"
      proof (intro C.seqI)
        show "C.arr e" using ide_apex C.arr_cod_iff_arr by fastforce
        show "C.arr f0"
          using D.map_simp D.preserves_arr J.arr_char by metis
        show "C.dom e = C.cod f0"
          using J.arr_char J.ide_char D.mkCocone_def D.map_simp preserves_dom by force
      qed
      show "e ⋅ f0 = e ⋅ f1"
        using D.map_simp D.mkCocone_def J.arr_char naturality by force
    qed

    lemma is_couniversal':
    assumes "D.is_coequalized_by e'"
    shows "∃!h. «h : C.cod e → C.cod e'¬ ∧ h ⋅ e = e'"
    proof -
      have "D.cocone (C.cod e') (D.mkCocone e')"
        using assms D.cocone_mkCocone by blast
      moreover have 0: "D.cocone (C.cod e) (D.mkCocone e)" ..
      ultimately have 1: "∃!h. «h : C.cod e → C.cod e'¬ ∧
                               D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
        using is_couniversal [of "C.cod e'" "D.mkCocone e'"] by auto
      have 2: "∧h. «h : C.cod e → C.cod e'¬ ==>
                    D.cocones_map h (D.mkCocone e) = D.mkCocone e' ⟷ h ⋅ e = e'"
      proof -
        fix h
        assume h: "«h : C.cod e → C.cod e'¬"
        show "D.cocones_map h (D.mkCocone e) = D.mkCocone e' ⟷ h ⋅ e = e'"
        proof
          assume 3: "D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
          show "h ⋅ e = e'"
          proof -
            have "e' = D.mkCocone e' J.One"
              using D.mkCocone_def J.arr_char by simp
            also have "... = D.cocones_map h (D.mkCocone e) J.One"
              using 3 by simp
            also have "... = h ⋅ e"
              using 0 h D.mkCocone_def J.arr_char by auto
            finally show ?thesis by auto
          qed
          next
          assume e': "h ⋅ e = e'"
          show "D.cocones_map h (D.mkCocone e) = D.mkCocone e'"
          proof
            fix j
            have "¬J.arr j ==> D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
              using h cocone_axioms D.mkCocone_def by auto
            moreover have "j = J.One ==> D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
              using h e' is_cocone D.mkCocone_def J.arr_char [of J.One] by force
            moreover have
                "J.arr j ∧ j ≠ J.One ==> D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j"
              using C.comp_assoc D.mkCocone_def is_cocone e' h by auto
            ultimately show "D.cocones_map h (D.mkCocone e) j = D.mkCocone e' j" by blast
          qed
        qed
      qed
      thus ?thesis using 1 by blast
    qed

    lemma induced_arrowI':
    assumes "D.is_coequalized_by e'"
    shows "«induced_arrow (C.cod e') (D.mkCocone e') : C.cod e → C.cod e'¬"
    and "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
    proof -
      interpret A': constant_functor J.comp C ‹C.cod e'›
        using assms by (unfold_locales, auto)
      have cocone: "D.cocone (C.cod e') (D.mkCocone e')"
        using assms D.cocone_mkCocone [of e'] by blast
      have "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e =
              D.cocones_map (induced_arrow (C.cod e') (D.mkCocone e')) (D.mkCocone e) J.One"
        using cocone induced_arrowI(1) D.mkCocone_def J.arr_char is_cocone by force
      also have "... = e'"
      proof -
        have "D.cocones_map (induced_arrow (C.cod e') (D.mkCocone e')) (D.mkCocone e) =
              D.mkCocone e'"
          using cocone induced_arrowI by blast
        thus ?thesis
          using J.arr_char D.mkCocone_def by simp
      qed
      finally have 1: "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
        by auto
      show "«induced_arrow (C.cod e') (D.mkCocone e') : C.cod e → C.cod e'¬"
        using 1 cocone induced_arrowI by simp
      show "induced_arrow (C.cod e') (D.mkCocone e') ⋅ e = e'"
        using 1 cocone induced_arrowI by simp
    qed

  end

  context category
  begin

    definition has_as_coequalizer
    where "has_as_coequalizer f0 f1 e ≡
           par f0 f1 ∧ parallel_pair_diagram.has_as_coequalizer C f0 f1 e"

    definition has_coequalizers
    where "has_coequalizers = (∀f0 f1. par f0 f1 ⟶ (∃e. has_as_coequalizer f0 f1 e))"

    lemma has_as_coequalizerI [intro]:
    assumes "par f g" and "seq e f" and "e ⋅ f = e ⋅ g"
    and "∧e'. [seq e' f; e' ⋅ f = e' ⋅ g] ==> ∃!h. h ⋅ e = e'"
    shows "has_as_coequalizer f g e"
    proof (unfold has_as_coequalizer_def, intro conjI)
      show "arr f" and "arr g" and "dom f = dom g" and "cod f = cod g"
        using assms(1) by auto
      interpret J: parallel_pair .
      interpret D: parallel_pair_diagram C f g
        using assms(1) by unfold_locales
      show "D.has_as_coequalizer e"
      proof -
        let ?χ = "D.mkCocone e"
        let ?a = "cod e"
        interpret χ: cocone J.comp C D.map ?a ?χ
           using assms(2-3) D.cocone_mkCocone [of e] by simp
        interpret χ: colimit_cocone J.comp C D.map ?a ?χ
        proof
          fix a' χ'
          assume χ': "D.cocone a' χ'"
          interpret χ': cocone J.comp C D.map a' χ'
            using χ' by blast
          have 0: "seq (χ' J.One) f"
            using J.ide_char J.arr_char χ'.preserves_hom
            by (meson D.is_coequalized_by_cocone χ')
          have 1: "∃!h. h ⋅ e = χ' J.One"
            using assms 0 χ' D.is_coequalized_by_cocone by blast
          obtain h where h: "h ⋅ e = χ' J.One"
            using 1 by blast
          have 2: "D.is_coequalized_by e"
            using assms(2-3) by blast
          have "∃h. «h : cod e → a'¬ ∧ D.cocones_map h (D.mkCocone e) = χ'"
          proof 
            show "«h : cod e → a'¬ ∧ D.cocones_map h (D.mkCocone e) = χ'"
            proof
              show 3: "«h : cod e → a'¬"
                using h χ'.preserves_cod
                by (metis (no_types, lifting) χ'.A.map_simp χ'.preserves_reflects_arr
                    0 cod_comp seqE in_homI J.cod_simp(2))
              show "D.cocones_map h (D.mkCocone e) = χ'"
              proof
                fix j
                have "D.cocone (dom h) (D.mkCocone e)"
                  using 2 3 D.cocone_mkCocone by auto
                thus "D.cocones_map h (D.mkCocone e) j = χ' j"
                  using h 2 3 D.cocone_mkCocone [of e] J.arr_char D.mkCocone_def comp_assoc
                  apply (cases "J.arr j")
                   apply simp_all
                   apply (metis (no_types, lifting) D.mkCocone_cocone χ')
                  using χ'.extensionality
                  by presburger
              qed
            qed
          qed
          moreover have "∧h'. «h' : cod e → a'¬ ∧
                              D.cocones_map h' (D.mkCocone e) = χ' ==> h' = h"
          proof (elim conjE)
            fix h'
            assume h': "«h' : cod e → a'¬"
            assume eq: "D.cocones_map h' (D.mkCocone e) = χ'"
            have "h' ⋅ e = χ' J.One"
              using 0 D.mkCocone_def χ.cocone_axioms eq h' by fastforce
            moreover have "∃!h. h ⋅ e = χ' J.One"
              using assms(2,4) 1 seqI by blast
            ultimately show "h' = h"
              using h by auto
          qed
          ultimately show "∃!h. «h : cod e → a'¬ ∧ D.cocones_map h (D.mkCocone e) = χ'"
            by blast
        qed
        show "D.has_as_coequalizer e"
          using assms χ.colimit_cocone_axioms by blast
      qed
    qed

    lemma has_as_coequalizerE [elim]:
    assumes "has_as_coequalizer f g e"
    and "[seq e f; e ⋅ f = e ⋅ g; ∧e'. [seq e' f; e' ⋅ f = e' ⋅ g] ==> ∃!h. h ⋅ e = e'] ==> T"
    shows T
    proof -
      interpret D: parallel_pair_diagram C f g
        using assms has_as_coequalizer_def parallel_pair_diagram_axioms_def
        by (metis category_axioms parallel_pair_diagram_def)
      have "D.has_as_coequalizer e"
        using assms has_as_coequalizer_def by blast
      interpret coequalizer_cocone C f g e
        by (simp add: ‹D.has_as_coequalizer e› category_axioms coequalizer_cocone_def
            D.parallel_pair_diagram_axioms)
      show T
        by (metis (lifting) HOL.ext assms(2) cod_comp coequalizes in_homI is_couniversal' seqE)
    qed

  end

end