Theory Limit

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

chapter Limit

theory Limit
imports FreeCategory DiscreteCategory Adjunction
begin

  text‹
    This theory defines the notion of limit in terms of diagrams and cones and relates
    it to the concept of a representation of a functor.  The diagonal functor associated
    with a diagram shape @{term J} is defined and it is shown that a right adjoint to
    the diagonal functor gives limits of shape @{term J} and that a category has limits
    of shape @{term J} if and only if the diagonal functor is a left adjoint functor.
    Products and equalizers are defined as special cases of limits, and it is shown
    that a category with equalizers has limits of shape @{term J} if it has products
    indexed by the sets of objects and arrows of @{term J}.
    The existence of limits in a set category is investigated, and it is shown that
    every set category has equalizers and that a set category @{term S} has @{term I}-indexed
    products if and only if the universe of @{term S} ``admits @{term I}-indexed tupling.''
    The existence of limits in functor categories is also developed, showing that
    limits in functor categories are ``determined pointwise'' and that a functor category
    @{term "[A, B]"} has limits of shape @{term J} if @{term B} does.
    Finally, it is shown that the Yoneda functor preserves limits.

    This theory concerns itself only with limits; I have made no attempt to consider colimits.
    Although it would be possible to rework the entire development in dual form,
    it is possible that there is a more efficient way to dualize at least parts of it without
    repeating all the work.  This is something that deserves further thought.
›

  section "Representations of Functors"

  text‹
    A representation of a contravariant functor F: Cop → S›, where @{term S}
    is a set category that is the target of a hom-functor for @{term C}, consists of
    an object @{term a} of @{term C} and a natural isomorphism @{term "Φ: Y a  F"},
    where Y: C → [Cop, S]› is the Yoneda functor.
›

  locale representation_of_functor =
    C: category C +
    Cop: dual_category C +
    S: set_category S setp +
    F: "functor" Cop.comp S F +
    Hom: hom_functor C S setp φ +
    Ya: yoneda_functor_fixed_object C S setp φ a +
    natural_isomorphism Cop.comp S Ya.Y a F Φ
  for C :: "'c comp"      (infixr "" 55)
  and S :: "'s comp"      (infixr "S" 55)
  and setp :: "'s set  bool"
  and φ :: "'c * 'c  'c  's"
  and F :: "'c  's"
  and a :: 'c
  and Φ :: "'c  's"
  begin

     abbreviation Y where "Y  Ya.Y"
     abbreviation ψ where "ψ  Hom.ψ"

  end

  text‹
    Two representations of the same functor are uniquely isomorphic.
›

  locale two_representations_one_functor =
    C: category C +
    Cop: dual_category C +
    S: set_category S setp +
    F: set_valued_functor Cop.comp S setp F +
    yoneda_functor C S setp φ +
    Ya: yoneda_functor_fixed_object C S setp φ a +
    Ya': yoneda_functor_fixed_object C S setp φ a' +
    Φ: representation_of_functor C S setp φ F a Φ +
    Φ': representation_of_functor C S setp φ F a' Φ'
  for C :: "'c comp"      (infixr "" 55)
  and S :: "'s comp"      (infixr "S" 55)
  and setp :: "'s set  bool"
  and F :: "'c  's"
  and φ :: "'c * 'c  'c  's"
  and a :: 'c
  and Φ :: "'c  's"
  and a' :: 'c
  and Φ' :: "'c  's"
  begin

    interpretation Ψ: inverse_transformation Cop.comp S Y a F Φ ..
    interpretation Ψ': inverse_transformation Cop.comp S Y a' F Φ' ..
    interpretation ΦΨ': vertical_composite Cop.comp S Y a F Y a' Φ Ψ'.map ..
    interpretation Φ'Ψ: vertical_composite Cop.comp S Y a' F Y a Φ' Ψ.map ..

    lemma are_uniquely_isomorphic:
      shows "∃!φ. «φ : a  a'»  C.iso φ  map φ = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
    proof -
      interpret ΦΨ': natural_isomorphism Cop.comp S Y a Y a' ΦΨ'.map
        using Φ.natural_isomorphism_axioms Ψ'.natural_isomorphism_axioms
              natural_isomorphisms_compose
        by blast
      interpret Φ'Ψ: natural_isomorphism Cop.comp S Y a' Y a Φ'Ψ.map
        using Φ'.natural_isomorphism_axioms Ψ.natural_isomorphism_axioms
              natural_isomorphisms_compose
        by blast
      interpret ΦΨ'_Φ'Ψ: inverse_transformations Cop.comp S Y a Y a' ΦΨ'.map Φ'Ψ.map
      proof
        fix x
        assume X: "Cop.ide x"
        show "S.inverse_arrows (ΦΨ'.map x) (Φ'Ψ.map x)"
          using S.inverse_arrows_compose S.inverse_arrows_sym X Φ'Ψ.map_simp_ide
                ΦΨ'.map_simp_ide Ψ'.inverts_components Ψ.inverts_components
          by force
      qed
      have "Cop_S.inverse_arrows (Cop_S.MkArr (Y a) (Y a') ΦΨ'.map)
                                 (Cop_S.MkArr (Y a') (Y a) Φ'Ψ.map)"
      proof -
        have Ya: "functor Cop.comp S (Y a)" ..
        have Ya': "functor Cop.comp S (Y a')" ..
        have ΦΨ': "natural_transformation Cop.comp S (Y a) (Y a') ΦΨ'.map" ..
        have Φ'Ψ: "natural_transformation Cop.comp S (Y a') (Y a) Φ'Ψ.map" ..
        show ?thesis
          by (metis (no_types, lifting) Cop_S.arr_MkArr Cop_S.comp_MkArr Cop_S.ide_MkIde
              Cop_S.inverse_arrows_def Ya'.functor_axioms Ya.functor_axioms
              Φ'Ψ.natural_transformation_axioms ΦΨ'.natural_transformation_axioms
              ΦΨ'_Φ'Ψ.inverse_transformations_axioms inverse_transformations_inverse(1-2)
              mem_Collect_eq)
      qed
      hence 3: "Cop_S.iso (Cop_S.MkArr (Y a) (Y a') ΦΨ'.map)" using Cop_S.isoI by blast
      hence "f. «f : a  a'»  map f = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
        using Ya.ide_a Ya'.ide_a is_full Y_def Cop_S.iso_is_arr full_functor.is_full
              Cop_S.MkArr_in_hom ΦΨ'.natural_transformation_axioms preserves_ide
        by force
      from this obtain φ
        where φ: "«φ : a  a'»  map φ = Cop_S.MkArr (Y a) (Y a') ΦΨ'.map"
        by blast
      show ?thesis
        by (metis 3 C.in_homE φ is_faithful reflects_iso)
    qed

  end

  section "Diagrams and Cones"

  text‹
    A \emph{diagram} in a category @{term C} is a functor D: J → C›.
    We refer to the category @{term J} as the diagram \emph{shape}.
    Note that in the usual expositions of category theory that use set theory
    as their foundations, the shape @{term J} of a diagram is required to be
    a ``small'' category, where smallness means that the collection of objects
    of @{term J}, as well as each of the ``homs,'' is a set.
    However, in HOL there is no class of all sets, so it is not meaningful
    to speak of @{term J} as ``small'' in any kind of absolute sense.
    There is likely a meaningful notion of smallness of @{term J}
    \emph{relative to} @{term C} (the result below that states that a set
    category has @{term I}-indexed products if and only if its universe
    ``admits @{term I}-indexed tuples'' is suggestive of how this might
    be defined), but I haven't fully explored this idea at present.
›

  locale diagram =
    C: category C +
    J: category J +
    "functor" J C D
  for J :: "'j comp"      (infixr "J" 55)
  and C :: "'c comp"      (infixr "" 55)
  and D :: "'j  'c"
  begin

    notation J.in_hom ("«_ : _ J _»")

  end
 
  lemma comp_diagram_functor:
  assumes "diagram J C D" and "functor J' J F"
  shows "diagram J' C (D o F)"
    by (meson assms(1) assms(2) diagram_def functor.axioms(1) functor_comp)
    
  text‹
    A \emph{cone} over a diagram D: J → C› is a natural transformation
    from a constant functor to @{term D}.  The value of the constant functor is
    the \emph{apex} of the cone.
›

  locale cone =
    C: category C +
    J: category J +
    D: diagram J C D +
    A: constant_functor J C a +
    natural_transformation J C A.map D χ
  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 : a  D (J.cod j)»"
      using assms by auto

    (* Suggested by Charles Staats, 12/13/2022 *)
    lemma cod_determines_component:
    assumes "J.arr j"
    shows "χ j = χ (J.cod j)"
      using assms is_natural_2 A.map_simp C.comp_arr_ide ide_apex preserves_reflects_arr
      by metis

  end

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

  lemma comp_cone_functor:
  assumes "cone J C D a χ" and "functor J' J F"
  shows "cone J' C (D o F) a (χ o F)"
  proof -
    interpret χ: cone 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 A'.map D o F χ o F
      using 1 horizontal_composite F.as_nat_trans.natural_transformation_axioms
            χ.natural_transformation_axioms
      by fastforce
    show "cone J' C (D o F) a (χ o F)" ..
  qed

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

  lemma vcomp_transformation_cone:
  assumes "cone J C D a χ"
  and "natural_transformation J C D D' τ"
  shows "cone J C D' a (vertical_composite.map J C χ τ)"
    by (meson assms cone.axioms(4-5) cone.intro diagram.intro natural_transformation.axioms(1-4)
              vertical_composite.intro vertical_composite.is_natural_transformation)

  context "functor"
  begin

    lemma preserves_diagrams:
    fixes J :: "'j comp"
    assumes "diagram J A D"
    shows "diagram J B (F o D)"
      by (meson assms diagram_def functor_axioms functor_comp functor_def)

    lemma preserves_cones:
    fixes J :: "'j comp"
    assumes "cone J A D a χ"
    shows "cone J B (F o D) (F a) (F o χ)"
    proof -
      interpret χ: cone 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 is_extensional Fa.is_extensional χ.A.is_extensional
          by (cases "χ.J.arr f", simp_all)
      qed
      interpret χ': natural_transformation J B Fa.map F o D F o χ
        using 1 horizontal_composite χ.natural_transformation_axioms
              as_nat_trans.natural_transformation_axioms
        by fastforce
      show "cone J B (F o D) (F a) (F o χ)" ..
    qed

  end

  context diagram
  begin

    abbreviation cone
    where "cone a χ  Limit.cone J C D a χ"

    abbreviation cones :: "'c  ('j  'c) set"
    where "cones a  { χ. cone a χ }"

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

    abbreviation cones_map :: "'c  ('j  'c)  ('j  'c)"
    where "cones_map f  (λχ  cones (C.cod f). λj. if J.arr j then χ j  f else C.null)"

    lemma cones_map_mapsto:
    assumes "C.arr f"
    shows "cones_map f 
             extensional (cones (C.cod f))  (cones (C.cod f)  cones (C.dom f))"
    proof
      show "cones_map f  extensional (cones (C.cod f))" by blast
      show "cones_map f  cones (C.cod f)  cones (C.dom f)"
      proof
        fix χ
        assume "χ  cones (C.cod f)"
        hence χ: "cone (C.cod f) χ" by auto
        interpret χ: cone J C D C.cod f χ using χ by auto
        interpret B: constant_functor J C C.dom f
          using assms by unfold_locales auto
        have "cone (C.dom f) (λj. if J.arr j then χ j  f else C.null)"
          using assms B.value_is_ide χ.is_natural_1 χ.is_natural_2
          apply (unfold_locales, auto)
          using χ.is_natural_1
           apply (metis C.comp_assoc)
          using χ.is_natural_2 C.comp_arr_dom
          by (metis J.arr_cod_iff_arr J.cod_cod C.comp_assoc)
        thus "(λj. if J.arr j then χ j  f else C.null)  cones (C.dom f)" by auto
      qed
    qed

    lemma cones_map_ide:
    assumes "χ  cones a"
    shows "cones_map a χ = χ"
    proof -
      interpret χ: cone J C D a χ using assms by auto
      show ?thesis
      proof
        fix j
        show "cones_map a χ j = χ j"
          using assms χ.A.value_is_ide χ.preserves_hom C.comp_arr_dom χ.is_extensional
          by (cases "J.arr j", auto)
      qed
    qed

    lemma cones_map_comp:
    assumes "C.seq f g"
    shows "cones_map (f  g) = restrict (cones_map g o cones_map f) (cones (C.cod f))"
    proof (intro restr_eqI)
      show "cones (C.cod (f  g)) = cones (C.cod f)" using assms by simp
      show "χ. χ  cones (C.cod (f  g)) 
                  (λj. if J.arr j then χ j  f  g else C.null) = (cones_map g o cones_map f) χ"
      proof -
        fix χ
        assume χ: "χ  cones (C.cod (f  g))"
        show "(λj. if J.arr j then χ j  f  g else C.null) = (cones_map g o cones_map f) χ"
        proof -
          have "((cones_map g) o (cones_map f)) χ = cones_map g (cones_map f χ)"
            by force
          also have "... = (λj. if J.arr j then
                              (λj. if J.arr j then χ j  f else C.null) j  g else C.null)"
          proof
            fix j
            have "cone (C.dom f) (cones_map f χ)"
              using assms χ cones_map_mapsto by (elim C.seqE, force)
            thus "cones_map g (cones_map f χ) j =
                  (if J.arr j then C (if J.arr j then χ j  f else C.null) g else C.null)"
              using χ assms by auto
          qed
          also have "... = (λj. if J.arr j then χ j  f  g else C.null)"
            using C.comp_assoc by fastforce
          finally show ?thesis by auto
        qed
      qed
    qed

  end

  text‹
    Changing the apex of a cone by pre-composing with an arrow @{term f} commutes
    with changing the diagram of a cone by post-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 NaturalTransformation.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χ.is_extensional 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

  text‹
    Given a diagram @{term D}, we can construct a contravariant set-valued functor,
    which takes each object @{term a} of @{term C} to the set of cones over @{term D}
    with apex @{term a}, and takes each arrow @{term f} of @{term C} to the function
    on cones over @{term D} induced by pre-composition with @{term f}.
    For this, we need to introduce a set category @{term S} whose universe is large
    enough to contain all the cones over @{term D}, and we need to have an explicit
    correspondence between cones and elements of the universe of @{term S}.
    A replete set category @{term S} equipped with an injective mapping
    @{term_type "ι :: ('j => 'c) => 's"} serves this purpose.
›
  locale cones_functor =
    C: category C +
    Cop: dual_category C +
    J: category J +
    D: diagram J C D +
    S: replete_concrete_set_category S UNIV ι
  for J :: "'j comp"      (infixr "J" 55)
  and C :: "'c comp"      (infixr "" 55)
  and D :: "'j  'c"
  and S :: "'s comp"      (infixr "S" 55)
  and ι :: "('j  'c)  's"
  begin

    notation S.in_hom     ("«_ : _ S _»")

    abbreviation 𝗈 where "𝗈  S.DN"

    definition map :: "'c  's"
    where "map = (λf. if C.arr f then
                        S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom f))
                                (ι o D.cones_map f o 𝗈)
                      else S.null)"

    lemma map_simp [simp]:
    assumes "C.arr f"
    shows "map f = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom f))
                           (ι o D.cones_map f o 𝗈)"
      using assms map_def by auto

    lemma arr_map:
    assumes "C.arr f"
    shows "S.arr (map f)"
    proof -
      have "ι o D.cones_map f o 𝗈  ι ` D.cones (C.cod f)  ι ` D.cones (C.dom f)"
        using assms D.cones_map_mapsto by force
      thus ?thesis using assms S.UP_mapsto by auto
    qed

    lemma map_ide:
    assumes "C.ide a"
    shows "map a = S.mkIde (ι ` D.cones a)"
    proof -
      have "map a = S.mkArr (ι ` D.cones a) (ι ` D.cones a) (ι o D.cones_map a o 𝗈)"
        using assms map_simp by force
      also have "... = S.mkArr (ι ` D.cones a) (ι ` D.cones a) (λx. x)"
        using S.UP_mapsto D.cones_map_ide by force
      also have "... = S.mkIde (ι ` D.cones a)"
        using assms S.mkIde_as_mkArr S.UP_mapsto by blast
      finally show ?thesis by auto
    qed

    lemma map_preserves_dom:
    assumes "Cop.arr f"
    shows "map (Cop.dom f) = S.dom (map f)"
      using assms arr_map map_ide by auto

    lemma map_preserves_cod:
    assumes "Cop.arr f"
    shows "map (Cop.cod f) = S.cod (map f)"
      using assms arr_map map_ide by auto

    lemma map_preserves_comp:
    assumes "Cop.seq g f"
    shows "map (g op f) = map g S map f"
    proof -
      have "map (g op f) = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
                                   ((ι o D.cones_map g o 𝗈) o (ι o D.cones_map f o 𝗈))"
      proof -
        have 1: "S.arr (map (g op f))"
          using assms arr_map [of "C f g"] by simp
        have "map (g op f) = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
                                     (ι o D.cones_map (C f g) o 𝗈)"
          using assms map_simp [of "C f g"] by simp
        also have "... = S.mkArr (ι ` D.cones (C.cod f)) (ι ` D.cones (C.dom g))
                                 ((ι o D.cones_map g o 𝗈) o (ι o D.cones_map f o 𝗈))"
          using assms 1 calculation D.cones_map_mapsto D.cones_map_comp by auto
        finally show ?thesis by blast
      qed
      also have "... = map g S map f"
        using assms arr_map [of f] arr_map [of g] map_simp S.comp_mkArr by auto
      finally show ?thesis by auto
    qed

    lemma is_functor:
    shows "functor Cop.comp S map"
      apply (unfold_locales)
      using map_def arr_map map_preserves_dom map_preserves_cod map_preserves_comp
      by auto
    
  end

  sublocale cones_functor  "functor" Cop.comp S map using is_functor by auto
  sublocale cones_functor  set_valued_functor Cop.comp S λA. A  S.Univ map ..

  section Limits

  subsection "Limit Cones"

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

  locale limit_cone =
    C: category C +
    J: category J +
    D: diagram J C D +
    cone 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_universal: "cone J C D a' χ'  ∃!f. «f : a'  a»  D.cones_map f χ = χ'"
  begin

    definition induced_arrow :: "'c  ('j  'c)  'c"
    where "induced_arrow a' χ' = (THE f. «f : a'  a»  D.cones_map f χ = χ')"

    lemma induced_arrowI:
    assumes χ': "χ'  D.cones a'"
    shows "«induced_arrow a' χ' : a'  a»"
    and "D.cones_map (induced_arrow a' χ') χ = χ'"
    proof -
      have "∃!f. «f : a'  a»  D.cones_map f χ = χ'"
        using assms χ' is_universal by simp
      hence 1: "«induced_arrow a' χ' : a'  a»  D.cones_map (induced_arrow a' χ') χ = χ'"
        using theI' [of "λf. «f : a'  a»  D.cones_map f χ = χ'"] induced_arrow_def
        by presburger
      show "«induced_arrow a' χ' : a'  a»" using 1 by simp
      show "D.cones_map (induced_arrow a' χ') χ = χ'" using 1 by simp
    qed

    lemma cones_map_induced_arrow:
    shows "induced_arrow a'  D.cones a'  C.hom a' a"
    and "χ'. χ'  D.cones a'  D.cones_map (induced_arrow a' χ') χ = χ'"
      using induced_arrowI by auto

    lemma induced_arrow_cones_map:
    assumes "C.ide a'"
    shows "(λf. D.cones_map f χ)  C.hom a' a  D.cones a'"
    and "f. «f : a'  a»  induced_arrow a' (D.cones_map f χ) = f"
    proof -
      have a': "C.ide a'" using assms by (simp add: cone.ide_apex)
      have cone_χ: "cone J C D a χ" ..
      show "(λf. D.cones_map f χ)  C.hom a' a  D.cones a'"
        using cone_χ D.cones_map_mapsto by blast
      fix f
      assume f: "«f : a'  a»"
      show "induced_arrow a' (D.cones_map f χ) = f"
      proof -
        have "D.cones_map f χ  D.cones a'"
          using f cone_χ D.cones_map_mapsto by blast
        hence "∃!f'. «f' : a'  a»  D.cones_map f' χ = D.cones_map f χ"
          using assms is_universal by auto
        thus ?thesis
          using f induced_arrow_def
                the1_equality [of "λf'. «f' : a'  a»  D.cones_map f' χ = D.cones_map f χ"]
          by presburger
      qed
    qed

    text‹
      For a limit cone @{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 cones
      with apex @{term a'}.
›

    lemma bij_betw_hom_and_cones:
    assumes "C.ide a'"
    shows "bij_betw (λf. D.cones_map f χ) (C.hom a' a) (D.cones a')"
    proof (intro bij_betwI)
      show "(λf. D.cones_map f χ)  C.hom a' a  D.cones a'"
        using assms induced_arrow_cones_map by blast
      show "induced_arrow a'  D.cones a'  C.hom a' a"
        using assms cones_map_induced_arrow by blast
      show "f. f  C.hom a' a  induced_arrow a' (D.cones_map f χ) = f"
        using assms induced_arrow_cones_map by blast
      show "χ'. χ'  D.cones a'  D.cones_map (induced_arrow a' χ') χ = χ'"
        using assms cones_map_induced_arrow by blast
    qed

    lemma induced_arrow_eqI:
    assumes "D.cone a' χ'" and "«f : a'  a»" and "D.cones_map f χ = χ'"
    shows "induced_arrow a' χ' = f"
      using assms is_universal induced_arrow_def
            the1_equality [of "λf. f  C.hom a' a  D.cones_map f χ = χ'" f]
      by simp

    lemma induced_arrow_self:
    shows "induced_arrow a χ = a"
    proof -
      have "«a : a  a»  D.cones_map a χ = χ"
        using ide_apex cone_axioms D.cones_map_ide by force
      thus ?thesis using induced_arrow_eqI cone_axioms by auto
    qed

  end

  context diagram
  begin

    abbreviation limit_cone
    where "limit_cone a χ  Limit.limit_cone J C D a χ"

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

    abbreviation has_as_limit :: "'c  bool"
    where "has_as_limit a  (χ. limit_cone a χ)"

    abbreviation has_limit
    where "has_limit  (a χ. limit_cone a χ)"

    definition some_limit :: 'c
    where "some_limit = (SOME a. χ. limit_cone a χ)"

    definition some_limit_cone :: "'j  'c"
    where "some_limit_cone = (SOME χ. limit_cone some_limit χ)"

    lemma limit_cone_some_limit_cone:
    assumes has_limit
    shows "limit_cone some_limit some_limit_cone"
    proof -
      have "a. has_as_limit a" using assms by simp
      hence "has_as_limit some_limit"
        using some_limit_def someI_ex [of "λa. χ. limit_cone a χ"] by simp
      thus "limit_cone some_limit some_limit_cone"
        using assms some_limit_cone_def someI_ex [of "λχ. limit_cone some_limit χ"]
        by simp
    qed

    lemma ex_limitE:
    assumes "a. has_as_limit a"
    obtains a χ where "limit_cone a χ"
      using assms someI_ex by blast

  end

  subsection "Limits by Representation"

  text‹
    A limit for a diagram D can also be given by a representation (a, Φ)›
    of the cones functor.
›

  locale representation_of_cones_functor =
    C: category C +
    Cop: dual_category C +
    J: category J +
    D: diagram J C D +
    S: replete_concrete_set_category S UNIV ι +
    Cones: cones_functor J C D S ι +
    Hom: hom_functor C S λA. A  S.Univ φ +
    representation_of_functor C S S.setp φ Cones.map a Φ
  for J :: "'j comp"      (infixr "J" 55)
  and C :: "'c comp"      (infixr "" 55)
  and D :: "'j  'c"
  and S :: "'s comp"      (infixr "S" 55)
  and φ :: "'c * 'c  'c  's"
  and ι :: "('j  'c)  's"
  and a :: 'c
  and Φ :: "'c  's"

  subsection "Putting it all Together"

  text‹
    A ``limit situation'' combines and connects the ways of presenting a limit.
›

  locale limit_situation =
    C: category C +
    Cop: dual_category C +
    J: category J +
    D: diagram J C D +
    S: replete_concrete_set_category S UNIV ι +
    Cones: cones_functor J C D S ι +
    Hom: hom_functor C S S.setp φ +
    Φ: representation_of_functor C S S.setp φ Cones.map a Φ +
    χ: limit_cone J C D a χ
  for J :: "'j comp"      (infixr "J" 55)
  and C :: "'c comp"      (infixr "" 55)
  and D :: "'j  'c"
  and S :: "'s comp"      (infixr "S" 55)
  and φ :: "'c * 'c  'c  's"
  and ι :: "('j  'c)  's"
  and a :: 'c
  and Φ :: "'c  's"
  and χ :: "'j  'c" +
  assumes χ_in_terms_of_Φ: "χ = S.DN (S.Fun (Φ a) (φ (a, a) a))"
  and Φ_in_terms_of_χ:
     "Cop.ide a'  Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a')
                                    (λx. ι (D.cones_map (Hom.ψ (a', a) x) χ))"

  text (in limit_situation) ‹
    The assumption @{prop χ_in_terms_of_Φ} states that the universal cone @{term χ} is obtained
    by applying the function @{term "S.Fun (Φ a)"} to the identity @{term a} of
    @{term[source=true] C} (after taking into account the necessary coercions).
›

  text (in limit_situation) ‹
    The assumption @{prop Φ_in_terms_of_χ} states that the component of @{term Φ} at @{term a'}
    is the arrow of @{term[source=true] S} corresponding to the function that takes an arrow
    @{term "f  C.hom a' a"} and produces the cone with vertex @{term a'} obtained
    by transforming the universal cone @{term χ} by @{term f}.
›

  subsection "Limit Cones Induce Limit Situations"

  text‹
    To obtain a limit situation from a limit cone, we need to introduce a set category
    that is large enough to contain the hom-sets of @{term C} as well as the cones
    over @{term D}.  We use the category of all @{typ "('c + ('j  'c))"}-sets for this.
›

  context limit_cone
  begin

    interpretation Cop: dual_category C ..
    interpretation CopxC: product_category Cop.comp C ..
    interpretation S: replete_setcat TYPE('c + ('j  'c)) .

    notation S.comp      (infixr "S" 55)

    interpretation Sr: replete_concrete_set_category S.comp UNIV S.UP o Inr
      apply unfold_locales
      using S.UP_mapsto
       apply auto[1]
      using S.inj_UP inj_Inr inj_compose
      by metis

    interpretation Cones: cones_functor J C D S.comp S.UP o Inr ..

    interpretation Hom: hom_functor C S.comp S.setp λ_. S.UP o Inl
      apply (unfold_locales)
      using S.UP_mapsto
        apply auto[1]
      using S.inj_UP injD inj_onI inj_Inl inj_compose
       apply (metis (no_types, lifting))
      using S.UP_mapsto
      by auto

    interpretation Y: yoneda_functor C S.comp S.setp λ_. S.UP o Inl ..
    interpretation Ya: yoneda_functor_fixed_object C S.comp S.setp λ_. S.UP o Inl a
      apply (unfold_locales) using ide_apex by auto

    abbreviation inl :: "'c  'c + ('j  'c)" where "inl  Inl"
    abbreviation inr :: "('j  'c)  'c + ('j  'c)" where "inr  Inr"
    abbreviation ι where "ι  S.UP o inr"
    abbreviation 𝗈 where "𝗈  Cones.𝗈"
    abbreviation φ where "φ  λ_. S.UP o inl"
    abbreviation ψ where "ψ  Hom.ψ"
    abbreviation Y where "Y  Y.Y"

    lemma Ya_ide:
    assumes a': "C.ide a'"
    shows "Y a a' = S.mkIde (Hom.set (a', a))"
      using assms ide_apex Y.Y_simp Hom.map_ide by simp

    lemma Ya_arr:
    assumes g: "C.arr g"
    shows "Y a g = S.mkArr (Hom.set (C.cod g, a)) (Hom.set (C.dom g, a))
                           (φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a))"
      using ide_apex g Y.Y_ide_arr [of a g "C.dom g" "C.cod g"] by auto

    lemma is_cone [simp]:
    shows "χ  D.cones a"
      using cone_axioms by simp
    
    text‹
      For each object @{term a'} of @{term[source=true] C} we have a function mapping
      @{term "C.hom a' a"} to the set of cones over @{term D} with apex @{term a'},
      which takes @{term "f  C.hom a' a"} to χf›, where χf› is the cone obtained by
      composing @{term χ} with @{term f} (after accounting for coercions to and from the
      universe of @{term S}).  The corresponding arrows of @{term S} are the
      components of a natural isomorphism from @{term "Y a"} to Cones›.
›

    definition Φo :: "'c  ('c + ('j  'c)) setcat.arr"
    where
      "Φo a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (λx. ι (D.cones_map (ψ (a', a) x) χ))"

    lemma Φo_in_hom:
    assumes a': "C.ide a'"
    shows "«Φo a' : S.mkIde (Hom.set (a', a)) S S.mkIde (ι ` D.cones a')»"
    proof -
      have " «S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (λx. ι (D.cones_map (ψ (a', a) x) χ)) :
                 S.mkIde (Hom.set (a', a)) S S.mkIde (ι ` D.cones a')»"
      proof -
        have "(λx. ι (D.cones_map (ψ (a', a) x) χ))  Hom.set (a', a)  ι ` D.cones a'"
        proof
          fix x
          assume x: "x  Hom.set (a', a)"
          hence "«ψ (a', a) x : a'  a»"
            using ide_apex a' Hom.ψ_mapsto by auto
          hence "D.cones_map (ψ (a', a) x) χ  D.cones a'"
            using ide_apex a' x D.cones_map_mapsto is_cone by force
          thus "ι (D.cones_map (ψ (a', a) x) χ)  ι ` D.cones a'" by simp
        qed
        moreover have "Hom.set (a', a)  S.Univ"
          using ide_apex a' Hom.set_subset_Univ by auto
        moreover have "ι ` D.cones a'  S.Univ"
          using S.UP_mapsto by auto
        ultimately show ?thesis using S.mkArr_in_hom by simp
      qed
      thus ?thesis using Φo_def [of a'] by auto
    qed

    interpretation Φ: transformation_by_components Cop.comp S.comp Y a Cones.map Φo
    proof
      fix a'
      assume A': "Cop.ide a'"
      show "«Φo a' : Y a a' S Cones.map a'»"
        using A' Ya_ide Φo_in_hom Cones.map_ide by auto
      next
      fix g
      assume g: "Cop.arr g"
      show "Φo (Cop.cod g) S Y a g = Cones.map g S Φo (Cop.dom g)"
      proof -
        let ?A = "Hom.set (C.cod g, a)"
        let ?B = "Hom.set (C.dom g, a)"
        let ?B' = "ι ` D.cones (C.cod g)"
        let ?C = "ι ` D.cones (C.dom g)"
        let ?F = "φ (C.dom g, a) o Cop.comp g o ψ (C.cod g, a)"
        let ?F' = "ι o D.cones_map g o 𝗈"
        let ?G = "λx. ι (D.cones_map (ψ (C.dom g, a) x) χ)"
        let ?G' = "λx. ι (D.cones_map (ψ (C.cod g, a) x) χ)"
        have "S.arr (Y a g)  Y a g = S.mkArr ?A ?B ?F"
          using ide_apex g Ya.preserves_arr Ya_arr by fastforce
        moreover have "S.arr (Φo (Cop.cod g))"
          using g Φo_in_hom [of "Cop.cod g"] by auto
        moreover have "Φo (Cop.cod g) = S.mkArr ?B ?C ?G"
          using g Φo_def [of "C.dom g"] by auto
        moreover have "S.seq (Φo (Cop.cod g)) (Y a g)"
          using ide_apex g Φo_in_hom [of "Cop.cod g"] by auto
        ultimately have 1: "S.seq (Φo (Cop.cod g)) (Y a g) 
                            Φo (Cop.cod g) S Y a g = S.mkArr ?A ?C (?G o ?F)"
          using S.comp_mkArr [of ?A ?B ?F ?C ?G] by argo

        have "Cones.map g = S.mkArr (ι ` D.cones (C.cod g)) (ι ` D.cones (C.dom g)) ?F'"
          using g Cones.map_simp by fastforce
        moreover have "Φo (Cop.dom g) = S.mkArr ?A ?B' ?G'"
          using g Φo_def by fastforce
        moreover have "S.seq (Cones.map g) (Φo (Cop.dom g))"
          using g Cones.preserves_hom [of g "C.cod g" "C.dom g"] Φo_in_hom [of "Cop.dom g"]
          by force
        ultimately have
          2: "S.seq (Cones.map g) (Φo (Cop.dom g)) 
              Cones.map g S Φo (Cop.dom g) = S.mkArr ?A ?C (?F' o ?G')"
          using S.seqI' [of "Φo (Cop.dom g)" "Cones.map g"] S.comp_mkArr by auto

        have "Φo (Cop.cod g) S Y a g = S.mkArr ?A ?C (?G o ?F)"
          using 1 by auto
        also have "... = S.mkArr ?A ?C (?F' o ?G')"
        proof (intro S.mkArr_eqI')
          show "S.arr (S.mkArr ?A ?C (?G o ?F))" using 1 by force
          show "x. x  ?A  (?G o ?F) x = (?F' o ?G') x"
          proof -
            fix x
            assume x: "x  ?A"
            hence 1: "«ψ (C.cod g, a) x : C.cod g  a»"
              using ide_apex g Hom.ψ_mapsto [of "C.cod g" a] by auto
            have "(?G o ?F) x = ι (D.cones_map (ψ (C.dom g, a)
                                  (φ (C.dom g, a) (ψ (C.cod g, a) x  g))) χ)"
            proof - (* Why is it so balky with this proof? *)
              have "(?G o ?F) x = ?G (?F x)" by simp
              also have "... = ι (D.cones_map (ψ (C.dom g, a)
                                     (φ (C.dom g, a) (ψ (C.cod g, a) x  g))) χ)"
                by (metis Cop.comp_def comp_apply)
              finally show ?thesis by auto
            qed
            also have "... = ι (D.cones_map (ψ (C.cod g, a) x  g) χ)"
            proof -
              have "«ψ (C.cod g, a) x  g : C.dom g  a»" using g 1 by auto
              thus ?thesis using Hom.ψ_φ by presburger
            qed
            also have "... = ι (D.cones_map g (D.cones_map (ψ (C.cod g, a) x) χ))"
              using g x 1 is_cone D.cones_map_comp [of "ψ (C.cod g, a) x" g] by fastforce
            also have "... = ι (D.cones_map g (𝗈 (ι (D.cones_map (ψ (C.cod g, a) x) χ))))"
              using 1 is_cone D.cones_map_mapsto Sr.DN_UP by auto
            also have "... = (?F' o ?G') x" by simp
            finally show "(?G o ?F) x = (?F' o ?G') x" by auto
          qed
        qed
        also have "... = Cones.map g S Φo (Cop.dom g)"
          using 2 by auto
        finally show ?thesis by auto
      qed
    qed

    interpretation Φ: set_valued_transformation Cop.comp S.comp S.setp
                        Y a Cones.map Φ.map ..
                                            
    interpretation Φ: natural_isomorphism Cop.comp S.comp Y a Cones.map Φ.map
    proof
      fix a'
      assume a': "Cop.ide a'"
      show "S.iso (Φ.map a')"
      proof -
        let ?F = "λx. ι (D.cones_map (ψ (a', a) x) χ)"
        have bij: "bij_betw ?F (Hom.set (a', a)) (ι ` D.cones a')"
        proof -
          have "x x'.  x  Hom.set (a', a); x'  Hom.set (a', a);
                         ι (D.cones_map (ψ (a', a) x) χ) = ι (D.cones_map (ψ (a', a) x') χ) 
                             x = x'"
          proof -
            fix x x'
            assume x: "x  Hom.set (a', a)" and x': "x'  Hom.set (a', a)"
            and xx': "ι (D.cones_map (ψ (a', a) x) χ) = ι (D.cones_map (ψ (a', a) x') χ)"
            have ψx: "«ψ (a', a) x : a'  a»" using x ide_apex a' Hom.ψ_mapsto by auto
            have ψx': "«ψ (a', a) x' : a'  a»" using x' ide_apex a' Hom.ψ_mapsto by auto
            have 1: "∃!f. «f : a'  a»  ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
            proof -
              have "D.cones_map (ψ (a', a) x) χ  D.cones a'"
                using ψx a' is_cone D.cones_map_mapsto by force
              hence 2: "∃!f. «f : a'  a»  D.cones_map f χ = D.cones_map (ψ (a', a) x) χ"
                using a' is_universal by simp
              show "∃!f. «f : a'  a»  ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
              proof -
                have "f. ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)
                              D.cones_map f χ = D.cones_map (ψ (a', a) x) χ"
                proof -
                  fix f :: 'c
                  have "D.cones_map f χ = D.cones_map (ψ (a', a) x) χ
                            ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ)"
                    by simp
                  thus "(ι (D.cones_map f χ) = ι (D.cones_map (ψ (a', a) x) χ))
                            = (D.cones_map f χ = D.cones_map (ψ (a', a) x) χ)"
                    by (meson Sr.inj_UP injD)
                qed
                thus ?thesis using 2 by auto
              qed
            qed
            have 2: "∃!x''. x''  Hom.set (a', a) 
                            ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
            proof -
              from 1 obtain f'' where
                  f'': "«f'' : a'  a»  ι (D.cones_map f'' χ) = ι (D.cones_map (ψ (a', a) x) χ)"
                by blast
              have "φ (a', a) f''  Hom.set (a', a) 
                    ι (D.cones_map (ψ (a', a) (φ (a', a) f'')) χ) = ι (D.cones_map (ψ (a', a) x) χ)"
              proof
                show "φ (a', a) f''  Hom.set (a', a)" using f'' Hom.set_def by auto
                show "ι (D.cones_map (ψ (a', a) (φ (a', a) f'')) χ) =
                         ι (D.cones_map (ψ (a', a) x) χ)"
                  using f'' Hom.ψ_φ by presburger
              qed
              moreover have
                 "x''. x''  Hom.set (a', a) 
                         ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)
                              x'' = φ (a', a) f''"
              proof -
                fix x''
                assume x'': "x''  Hom.set (a', a) 
                             ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
                hence "«ψ (a', a) x'' : a'  a» 
                       ι (D.cones_map (ψ (a', a) x'') χ) = ι (D.cones_map (ψ (a', a) x) χ)"
                  using ide_apex a' Hom.set_def Hom.ψ_mapsto [of a' a] by auto
                hence "φ (a', a) (ψ (a', a) x'') = φ (a', a) f''"
                  using 1 f'' by auto
                thus "x'' = φ (a', a) f''"
                  using ide_apex a' x'' Hom.φ_ψ by simp
              qed
              ultimately show ?thesis
                using ex1I [of "λx'. x'  Hom.set (a', a) 
                                     ι (D.cones_map (ψ (a', a) x') χ) =
                                        ι (D.cones_map (ψ (a', a) x) χ)"
                               "φ (a', a) f''"]
                by simp
            qed
            thus "x = x'" using x x' xx' by auto
          qed
          hence "inj_on ?F (Hom.set (a', a))"
            using inj_onI [of "Hom.set (a', a)" ?F] by auto 
          moreover have "?F ` Hom.set (a', a) = ι ` D.cones a'"
          proof
            show "?F ` Hom.set (a', a)  ι ` D.cones a'"
            proof
              fix X'
              assume X': "X'  ?F ` Hom.set (a', a)"
              from this obtain x' where x': "x'  Hom.set (a', a)  ?F x' = X'" by blast
              show "X'  ι ` D.cones a'"
              proof -
                have "X' = ι (D.cones_map (ψ (a', a) x') χ)" using x' by blast
                hence "X' = ι (D.cones_map (ψ (a', a) x') χ)" using x' by force
                moreover have "«ψ (a', a) x' : a'  a»"
                  using ide_apex a' x' Hom.set_def Hom.ψ_φ by auto
                ultimately show ?thesis
                  using x' is_cone D.cones_map_mapsto by force
              qed
            qed
            show "ι ` D.cones a'  ?F ` Hom.set (a', a)"
            proof
              fix X'
              assume X': "X'  ι ` D.cones a'"
              hence "𝗈 X'  𝗈 ` ι ` D.cones a'" by simp
              with Sr.DN_UP have "𝗈 X'  D.cones a'"
                by auto
              hence "∃!f. «f : a'  a»  D.cones_map f χ = 𝗈 X'"
                using a' is_universal by simp
              from this obtain f where "«f : a'  a»  D.cones_map f χ = 𝗈 X'"
                by auto
              hence f: "«f : a'  a»  ι (D.cones_map f χ) = X'"
                using X' Sr.UP_DN by auto
              have "X' = ?F (φ (a', a) f)"
                using f Hom.ψ_φ by presburger
              thus "X'  ?F ` Hom.set (a', a)"
                using f Hom.set_def by force
            qed
          qed
          ultimately show ?thesis
            using bij_betw_def [of ?F "Hom.set (a', a)" "ι ` D.cones a'"] inj_on_def by auto
        qed
        let ?f = "S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
        have iso: "S.iso ?f"
        proof -
          have "?F  Hom.set (a', a)  ι ` D.cones a'"
            using bij bij_betw_imp_funcset by fast
          hence 1: "S.arr ?f"
            using ide_apex a' Hom.set_subset_Univ S.UP_mapsto by auto
          thus ?thesis using bij S.iso_char S.set_mkIde by fastforce
        qed
        moreover have "?f = Φ.map a'"
          using a' Φo_def by force
        finally show ?thesis by auto
      qed
    qed

    interpretation R: representation_of_functor C S.comp S.setp φ Cones.map a Φ.map ..

    lemma χ_in_terms_of_Φ:
    shows "χ = 𝗈 (Φ.FUN a (φ (a, a) a))"
    proof -
      have "Φ.FUN a (φ (a, a) a) = 
              (λx  Hom.set (a, a). ι (D.cones_map (ψ (a, a) x) χ)) (φ (a, a) a)"
        using ide_apex S.Fun_mkArr Φ.map_simp_ide Φo_def Φ.preserves_reflects_arr [of a]
        by simp
      also have "... = ι (D.cones_map a χ)"
      proof -
        have "(λx  Hom.set (a, a). ι (D.cones_map (ψ (a, a) x) χ)) (φ (a, a) a)
                 = ι (D.cones_map (ψ (a, a) (φ (a, a) a)) χ)"
        proof -
          have "φ (a, a) a  Hom.set (a, a)"
            using ide_apex Hom.φ_mapsto by fastforce
          thus ?thesis
            using restrict_apply' [of "φ (a, a) a" "Hom.set (a, a)"] by blast
        qed
        also have "... = ι (D.cones_map a χ)"
        proof -
          have "ψ (a, a) (φ (a, a) a) = a"
            using ide_apex Hom.ψ_φ [of a a a] by fastforce
          thus ?thesis by metis
        qed
        finally show ?thesis by auto
      qed
      finally have "Φ.FUN a (φ (a, a) a) = ι (D.cones_map a χ)" by auto
      also have "... = ι χ"
        using ide_apex D.cones_map_ide [of χ a] is_cone by simp
      finally have "Φ.FUN a (φ (a, a) a) = ι χ" by blast
      hence "𝗈 (Φ.FUN a (φ (a, a) a)) = 𝗈 (ι χ)" by simp
      thus ?thesis using is_cone Sr.DN_UP by simp
    qed

    abbreviation Hom
    where "Hom  Hom.map"

    abbreviation Φ
    where "Φ  Φ.map"

    lemma induces_limit_situation:
    shows "limit_situation J C D S.comp φ ι a Φ χ"
      using χ_in_terms_of_Φ Φo_def by unfold_locales auto

    no_notation S.comp      (infixr "S" 55)

  end

  sublocale limit_cone  limit_situation J C D replete_setcat.comp φ ι a Φ χ
    using induces_limit_situation by auto

  subsection "Representations of the Cones Functor Induce Limit Situations"

  context representation_of_cones_functor
  begin

    interpretation Φ: set_valued_transformation Cop.comp S S.setp Y a Cones.map Φ ..
    interpretation Ψ: inverse_transformation Cop.comp S Y a Cones.map Φ ..
    interpretation Ψ: set_valued_transformation Cop.comp S S.setp
                        Cones.map Y a Ψ.map ..

    abbreviation 𝗈
    where "𝗈  Cones.𝗈"

    abbreviation χ
    where "χ  𝗈 (S.Fun (Φ a) (φ (a, a) a))"

    lemma Cones_SET_eq_ι_img_cones:
    assumes "C.ide a'"
    shows "Cones.SET a' = ι ` D.cones a'"
    proof -
      have "ι ` D.cones a'  S.Univ" using S.UP_mapsto by auto
      thus ?thesis using assms Cones.map_ide S.set_mkIde by auto
    qed

    lemma ιχ:
    shows "ι χ = S.Fun (Φ a) (φ (a, a) a)"
    proof -
      have "S.Fun (Φ a) (φ (a, a) a)  Cones.SET a"
        using Ya.ide_a Hom.φ_mapsto S.Fun_mapsto [of "Φ a"] Hom.set_map by fastforce
      thus ?thesis
        using Ya.ide_a Cones_SET_eq_ι_img_cones by auto
    qed

    interpretation χ: cone J C D a χ
    proof -
      have "ι χ  ι ` D.cones a"
        using Ya.ide_a ιχ S.Fun_mapsto [of "Φ a"] Hom.φ_mapsto Hom.set_map
              Cones_SET_eq_ι_img_cones by fastforce
      thus "D.cone a χ"
        by (metis (no_types, lifting) S.DN_UP UNIV_I f_inv_into_f inv_into_into mem_Collect_eq)
    qed

    lemma cone_χ:
    shows "D.cone a χ" ..

    lemma Φ_FUN_simp:
    assumes a': "C.ide a'" and x: "x  Hom.set (a', a)"
    shows "Φ.FUN a' x = Cones.FUN (ψ (a', a) x) (ι χ)"
    proof -
      have ψx: "«ψ (a', a) x : a'  a»"
        using Ya.ide_a a' x Hom.ψ_mapsto by blast
      have φa: "φ (a, a) a  Hom.set (a, a)" using Ya.ide_a Hom.φ_mapsto by fastforce
      have "Φ.FUN a' x = (Φ.FUN a' o Ya.FUN (ψ (a', a) x)) (φ (a, a) a)"
      proof -
        have "φ (a', a) (a  ψ (a', a) x) = x"
          using Ya.ide_a a' x ψx Hom.φ_ψ C.comp_cod_arr by fastforce
        moreover have "S.arr (S.mkArr (Hom.set (a, a)) (Hom.set (a', a))
                             (φ (a', a)  Cop.comp (ψ (a', a) x)  ψ (a, a)))"
          by (metis C.arrI Cop.arr_char Ya.Y_ide_arr(2) Ya.preserves_arr χ.ide_apex ψx)
        ultimately show ?thesis
          using Ya.ide_a a' x Ya.Y_ide_arr ψx φa C.ide_in_hom by auto
      qed
      also have "... = (Cones.FUN (ψ (a', a) x) o Φ.FUN a) (φ (a, a) a)"
      proof -
        have "(Φ.FUN a' o Ya.FUN (ψ (a', a) x)) (φ (a, a) a)
                = S.Fun (Φ a' S Y a (ψ (a', a) x)) (φ (a, a) a)"
          using ψx a' φa Ya.ide_a Ya.map_simp Hom.set_map by (elim C.in_homE, auto)
        also have "... = S.Fun (S (Cones.map (ψ (a', a) x)) (Φ a)) (φ (a, a) a)"
          using ψx is_natural_1 [of "ψ (a', a) x"] is_natural_2 [of "ψ (a', a) x"] by auto
        also have "... = (Cones.FUN (ψ (a', a) x) o Φ.FUN a) (φ (a, a) a)"
        proof -
          have "S.seq (Cones.map (ψ (a', a) x)) (Φ a)"
            using Ya.ide_a ψx Cones.map_preserves_dom [of "ψ (a', a) x"]
            apply (intro S.seqI)
              apply auto[2]
            by fastforce
          thus ?thesis
            using Ya.ide_a φa Hom.set_map by auto
        qed
        finally show ?thesis by simp
      qed
      also have "... = Cones.FUN (ψ (a', a) x) (ι χ)" using ιχ by simp
      finally show ?thesis by auto
    qed

    lemma χ_is_universal:
    assumes "D.cone a' χ'"
    shows "«ψ (a', a) (Ψ.FUN a' (ι χ')) : a'  a»"
    and "D.cones_map (ψ (a', a) (Ψ.FUN a' (ι χ'))) χ = χ'"
    and " «f' : a'  a»; D.cones_map f' χ = χ'   f' = ψ (a', a) (Ψ.FUN a' (ι χ'))"
    proof -
      interpret χ': cone J C D a' χ' using assms by auto
      have a': "C.ide a'" using χ'.ide_apex by simp
      have ιχ': "ι χ'  Cones.SET a'" using assms a' Cones_SET_eq_ι_img_cones by auto
      let ?f = "ψ (a', a) (Ψ.FUN a' (ι χ'))"
      have A: "Ψ.FUN a' (ι χ')  Hom.set (a', a)"
      proof -
        have "Ψ.FUN a'  Cones.SET a'  Ya.SET a'"
          using a' Ψ.preserves_hom [of a' a' a'] S.Fun_mapsto [of "Ψ.map a'"] by fastforce
        thus ?thesis using a' ιχ' Ya.ide_a Hom.set_map by auto
      qed
      show f: "«?f : a'  a»" using A a' Ya.ide_a Hom.ψ_mapsto [of a' a] by auto
      have E: "f. «f : a'  a»  Cones.FUN f (ι χ) = Φ.FUN a' (φ (a', a) f)"
      proof -
        fix f
        assume f: "«f : a'  a»"
        have "φ (a', a) f  Hom.set (a', a)"
          using a' Ya.ide_a f Hom.φ_mapsto by auto
        thus "Cones.FUN f (ι χ) = Φ.FUN a' (φ (a', a) f)"
          using a' f Φ_FUN_simp by simp
      qed
      have I: "Φ.FUN a' (Ψ.FUN a' (ι χ')) = ι χ'"
      proof -
        have "Φ.FUN a' (Ψ.FUN a' (ι χ')) =
              compose (Ψ.DOM a') (Φ.FUN a') (Ψ.FUN a') (ι χ')"
          using a' ιχ' Cones.map_ide Ψ.preserves_hom [of a' a' a'] by force
        also have "... = (λx  Ψ.DOM a'. x) (ι χ')"
          using a' Ψ.inverts_components S.inverse_arrows_char by force
        also have "... = ι χ'"
          using a' ιχ' Cones.map_ide Ψ.preserves_hom [of a' a' a'] by force
        finally show ?thesis by auto
      qed
      show : "D.cones_map ?f χ = χ'"
      proof -
        have "D.cones_map ?f χ = (𝗈 o Cones.FUN ?f o ι) χ"
          using f Cones.preserves_arr [of ?f] cone_χ
          by (cases "D.cone a χ", auto)
        also have "... = χ'"
           using f Ya.ide_a a' A E I by auto
        finally show ?thesis by auto
      qed
      show " «f' : a'  a»; D.cones_map f' χ = χ'   f' = ?f"
      proof -
        assume f': "«f' : a'  a»" and f'χ: "D.cones_map f' χ = χ'"
        show "f' = ?f"
        proof -
          have 1: "φ (a', a) f'  Hom.set (a', a)  φ (a', a) ?f  Hom.set (a', a)"
            using Ya.ide_a a' f f' Hom.φ_mapsto by auto
          have "S.iso (Φ a')" using χ'.ide_apex components_are_iso by auto
          hence 2: "S.arr (Φ a')  bij_betw (Φ.FUN a') (Hom.set (a', a)) (Cones.SET a')"
            using Ya.ide_a a' S.iso_char Hom.set_map by auto
          have "Φ.FUN a' (φ (a', a) f') = Φ.FUN a' (φ (a', a) ?f)"
          proof -
            have "Φ.FUN a' (φ (a', a) ?f) = ι χ'"
              using A I Hom.φ_ψ Ya.ide_a a' by simp
            also have "... = Cones.FUN f' (ι χ)"
              using f f' A E cone_χ Cones.preserves_arr  f'χ by (elim C.in_homE, auto)
            also have "... = Φ.FUN a' (φ (a', a) f')"
              using f' E by simp
            finally show ?thesis by argo
          qed
          moreover have "inj_on (Φ.FUN a') (Hom.set (a', a))"
            using 2 bij_betw_imp_inj_on by blast
          ultimately have 3: "φ (a', a) f' = φ (a', a) ?f"
            using 1 inj_on_def [of "Φ.FUN a'" "Hom.set (a', a)"] by blast
          show ?thesis
          proof -
            have "f' = ψ (a', a) (φ (a', a) f')"
              using Ya.ide_a a' f' Hom.ψ_φ by simp
            also have "... = ψ (a', a) (Ψ.FUN a' (ι χ'))"
              using Ya.ide_a a' Hom.ψ_φ A 3 by simp
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    interpretation χ: limit_cone J C D a χ
    proof
      show "a' χ'. D.cone a' χ'  ∃!f. «f : a'  a»  D.cones_map f χ = χ'"
      proof -
        fix a' χ'
        assume 1: "D.cone a' χ'"
        show "∃!f. «f : a'  a»  D.cones_map f χ = χ'"
        proof
          show "«ψ (a', a) (Ψ.FUN a' (ι χ')) : a'  a» 
                D.cones_map (ψ (a', a) (Ψ.FUN a' (ι χ'))) χ = χ'"
            using 1 χ_is_universal by blast
          show "f. «f : a'  a»  D.cones_map f χ = χ'  f = ψ (a', a) (Ψ.FUN a' (ι χ'))"
            using 1 χ_is_universal by blast
        qed
      qed
    qed

    lemma χ_is_limit_cone:
    shows "D.limit_cone a χ" ..

    lemma induces_limit_situation:
    shows "limit_situation J C D S φ ι a Φ χ"
    proof
      show "χ = χ" by simp
      fix a'
      assume a': "Cop.ide a'"
      let ?F = "λx. ι (D.cones_map (ψ (a', a) x) χ)"
      show "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
      proof -
        have 1: "«Φ a' : S.mkIde (Hom.set (a', a)) S S.mkIde (ι ` D.cones a')»"
          using a' Cones.map_ide Ya.ide_a by auto
        moreover have "Φ.DOM a' = Hom.set (a', a)"
          using 1 Hom.set_subset_Univ a' Ya.ide_a Hom.set_map by simp
        moreover have "Φ.COD a' = ι ` D.cones a'"
          using a' Cones_SET_eq_ι_img_cones by fastforce
        ultimately have 2: "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (Φ.FUN a')"
          using S.mkArr_Fun [of "Φ a'"] by fastforce
        also have "... = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F"
        proof
          show "S.arr (S.mkArr (Hom.set (a', a)) (ι ` D.cones a') (Φ.FUN a'))"
            using 1 2 by auto
          show "x. x  Hom.set (a', a)  Φ.FUN a' x = ?F x"
          proof -
            fix x
            assume x: "x  Hom.set (a', a)"
            hence ψx: "«ψ (a', a) x : a'  a»"
              using a' Ya.ide_a Hom.ψ_mapsto by auto
            show "Φ.FUN a' x = ?F x"
            proof -
              have "Φ.FUN a' x = Cones.FUN (ψ (a', a) x) (ι χ)"
                using a' x Φ_FUN_simp by simp
              also have "... = restrict (ι o D.cones_map (ψ (a', a) x) o 𝗈) (ι ` D.cones a) (ι χ)"
                using ψx Cones.map_simp Cones.preserves_arr [of "ψ (a', a) x"] S.Fun_mkArr
                by (elim C.in_homE, auto)
              also have "... = ?F x" using cone_χ by simp
              ultimately show ?thesis by simp
            qed
          qed
        qed
        finally show "Φ a' = S.mkArr (Hom.set (a', a)) (ι ` D.cones a') ?F" by auto
      qed
    qed

  end

  sublocale representation_of_cones_functor  limit_situation J C D S φ ι a Φ χ
    using induces_limit_situation by auto

  section "Categories with Limits"

  context category
  begin

    text‹
      A category @{term[source=true] C} has limits of shape @{term J} if every diagram of shape
      @{term J} admits a limit cone.
›

    definition has_limits_of_shape
    where "has_limits_of_shape J  D. diagram J C D  (a χ. limit_cone J C D a χ)"

    text‹
      A category has limits at a type @{typ 'j} if it has limits of shape @{term J}
      for every category @{term J} whose arrows are of type @{typ 'j}.
›

    definition has_limits
    where "has_limits (_ :: 'j)  J :: 'j comp. category J  has_limits_of_shape J"

    text‹
      Whether a category has limits of shape J› truly depends only on the ``shape''
      (\emph{i.e.}~isomorphism class) of J› and not on details of its construction.
    ›

    lemma has_limits_preserved_by_isomorphism:
    assumes "has_limits_of_shape J" and "isomorphic_categories J J'"
    shows "has_limits_of_shape J'"
    proof -
      interpret J: category J
        using assms(2) isomorphic_categories_def isomorphic_categories_axioms_def by auto
      interpret J': category J'
        using assms(2) isomorphic_categories_def isomorphic_categories_axioms_def by auto
      from assms(2) obtain φ ψ where IF: "inverse_functors J' J φ ψ"
        using isomorphic_categories_def isomorphic_categories_axioms_def
              inverse_functors_sym
        by blast
      interpret IF: inverse_functors J' J φ ψ using IF by auto
      have ψφ: "ψ o φ = J.map" using IF.inv by metis
      have φψ: "φ o ψ = J'.map" using IF.inv' by metis
      have "D'. diagram J' C D'  a χ. limit_cone J' C D' a χ"
      proof -
        fix D'
        assume D': "diagram J' C D'"
        interpret D': diagram J' C D' using D' by auto
        interpret D: composite_functor J J' C φ D' ..
        interpret D: diagram J C D' o φ ..
        have D: "diagram J C (D' o φ)" ..
        from assms(1) obtain a χ where χ: "D.limit_cone a χ"
          using D has_limits_of_shape_def by blast
        interpret χ: limit_cone J C D' o φ a χ using χ by auto
        interpret A': constant_functor J' C a
          using χ.ide_apex by (unfold_locales, auto)
        have χoψ: "cone J' C (D' o φ o ψ) a (χ o ψ)"
          using comp_cone_functor IF.G.functor_axioms χ.cone_axioms by fastforce
        hence χoψ: "cone J' C D' a (χ o ψ)"
          using φψ by (metis D'.functor_axioms Fun.comp_assoc comp_functor_identity)
        interpret χoψ: cone J' C D' a χ o ψ using χoψ by auto
        interpret χoψ: limit_cone J' C D' a χ o ψ
        proof
          fix a' χ'
          assume χ': "D'.cone a' χ'"
          interpret χ': cone J' C D' a' χ' using χ' by auto
          have χ'oφ: "cone J C (D' o φ) a' (χ' o φ)"
            using χ' comp_cone_functor IF.F.functor_axioms by fastforce
          interpret χ'oφ: cone J C D' o φ a' χ' o φ using χ'oφ by auto
          have "cone J C (D' o φ) a' (χ' o φ)" ..
          hence 1: "∃!f. «f : a'  a»  D.cones_map f χ = χ' o φ"
            using χ.is_universal by simp
          show "∃!f. «f : a'  a»  D'.cones_map f (χ o ψ) = χ'"
          proof
            let ?f = "THE f. «f : a'  a»  D.cones_map f χ = χ' o φ"
            have f: "«?f : a'  a»  D.cones_map ?f χ = χ' o φ"
              using 1 theI' [of "λf. «f : a'  a»  D.cones_map f χ = χ' o φ"] by blast
            have f_in_hom: "«?f : a'  a»" using f by blast
            have "D'.cones_map ?f (χ o ψ) = χ'"
            proof
              fix j'
              have "¬J'.arr j'  D'.cones_map ?f (χ o ψ) j' = χ' j'"
              proof -
                assume j': "¬J'.arr j'"
                have "D'.cones_map ?f (χ o ψ) j' = null"
                  using j' f_in_hom χoψ by fastforce
                thus ?thesis
                  using j' χ'.is_extensional by simp
              qed
              moreover have "J'.arr j'  D'.cones_map ?f (χ o ψ) j' = χ' j'"
              proof -
                assume j': "J'.arr j'"
                have "D'.cones_map ?f (χ o ψ) j' = χ (ψ j')  ?f"
                  using j' f χoψ by fastforce
                also have "... = D.cones_map ?f χ (ψ j')"
                  using j' f_in_hom χ χ.is_cone by fastforce
                also have "... = χ' j'"
                  using j' f χ φψ Fun.comp_def J'.map_simp by metis
                finally show "D'.cones_map ?f (χ o ψ) j' = χ' j'" by auto
              qed
              ultimately show "D'.cones_map ?f (χ o ψ) j' = χ' j'" by blast
            qed
            thus "«?f : a'  a»  D'.cones_map ?f (χ o ψ) = χ'" using f by auto
            fix f'
            assume f': "«f' : a'  a»  D'.cones_map f' (χ o ψ) = χ'"
            have "D.cones_map f' χ = χ' o φ"
            proof
              fix j
              have "¬J.arr j  D.cones_map f' χ j = (χ' o φ) j"
                using f' χ χ'oφ.is_extensional χ.is_cone mem_Collect_eq restrict_apply by auto
              moreover have "J.arr j  D.cones_map f' χ j = (χ' o φ) j"
              proof -
                assume j: "J.arr j"
                have "D.cones_map f' χ j = C (χ j) f'"
                  using j f' χ.is_cone by auto
                also have "... = C ((χ o ψ) (φ j)) f'"
                  using j f' ψφ by (metis comp_apply J.map_simp)
                also have "... = D'.cones_map f' (χ o ψ) (φ j)"
                  using j f' χoψ by fastforce
                also have "... = (χ' o φ) j"
                  using j f' by auto
                finally show "D.cones_map f' χ j = (χ' o φ) j" by auto
              qed
              ultimately show "D.cones_map f' χ j = (χ' o φ) j" by blast
            qed
            hence "«f' : a'  a»  D.cones_map f' χ = χ' o φ"
              using f' by auto
            moreover have "P x x'. (∃!x. P x)  P x  P x'  x = x'"
              by auto
            ultimately show "f' = ?f" using 1 f by blast
          qed
        qed
        have "limit_cone J' C D' a (χ o ψ)" ..
        thus "a χ. limit_cone J' C D' a χ" by blast
      qed
      thus ?thesis using has_limits_of_shape_def by auto
    qed

  end

  subsection "Diagonal Functors"

  text‹
    The existence of limits can also be expressed in terms of adjunctions: a category @{term C}
    has limits of shape @{term J} if the diagonal functor taking each object @{term a}
    in @{term C} to the constant-@{term a} diagram and each arrow f ∈ C.hom a a'›
    to the constant-@{term f} natural transformation between diagrams is a left adjoint functor.
›

  locale diagonal_functor =
    C: category C +
    J: category J +
    J_C: functor_category J C
  for J :: "'j comp"      (infixr "J" 55)
  and C :: "'c comp"      (infixr "" 55)
  begin

    notation J.in_hom     ("«_ : _ J _»")
    notation J_C.comp     (infixr "[J,C]" 55)
    notation J_C.in_hom   ("«_ : _ [J,C] _»")

    definition map :: "'c  ('j, 'c) J_C.arr"
    where "map f = (if C.arr f then J_C.MkArr (constant_functor.map J C (C.dom f))
                                              (constant_functor.map J C (C.cod f))
                                              (constant_transformation.map J C f)
                               else J_C.null)"

    lemma is_functor:
    shows "functor C J_C.comp map"
    proof
      fix f
      show "¬ C.arr f  local.map f = J_C.null"
        using map_def by simp
      assume f: "C.arr f"
      interpret Dom_f: constant_functor J C C.dom f
        using f by (unfold_locales, auto)
      interpret Cod_f: constant_functor J C C.cod f
        using f by (unfold_locales, auto)
      interpret Fun_f: constant_transformation J C f
        using f by (unfold_locales, auto)
      show 1: "J_C.arr (map f)"
        using f map_def by (simp add: Fun_f.natural_transformation_axioms)
      show "J_C.dom (map f) = map (C.dom f)"
      proof -
        have "constant_transformation J C (C.dom f)"
          using f by unfold_locales auto
        hence "constant_transformation.map J C (C.dom f) = Dom_f.map"
          using Dom_f.map_def constant_transformation.map_def [of J C "C.dom f"] by auto
        thus ?thesis using f 1 by (simp add: map_def J_C.dom_char)
      qed
      show "J_C.cod (map f) = map (C.cod f)"
      proof -
        have "constant_transformation J C (C.cod f)"
          using f by unfold_locales auto
        hence "constant_transformation.map J C (C.cod f) = Cod_f.map"
          using Cod_f.map_def constant_transformation.map_def [of J C "C.cod f"] by auto
        thus ?thesis using f 1 by (simp add: map_def J_C.cod_char)
      qed
      next
      fix f g
      assume g: "C.seq g f"
      have f: "C.arr f" using g by auto
      interpret Dom_f: constant_functor J C C.dom f
        using f by unfold_locales auto
      interpret Cod_f: constant_functor J C C.cod f
        using f by unfold_locales auto
      interpret Fun_f: constant_transformation J C f
        using f by unfold_locales auto
      interpret Cod_g: constant_functor J C C.cod g
        using g by unfold_locales auto
      interpret Fun_g: constant_transformation J C g
        using g by unfold_locales auto
      interpret Fun_g: natural_transformation J C Cod_f.map Cod_g.map Fun_g.map
        apply unfold_locales
        using f g C.seqE [of g f] C.comp_arr_dom C.comp_cod_arr Fun_g.is_extensional by auto
      interpret Fun_fg: vertical_composite
                          J C Dom_f.map Cod_f.map Cod_g.map Fun_f.map Fun_g.map ..
      have 1: "J_C.arr (map f)"
        using f map_def by (simp add: Fun_f.natural_transformation_axioms)
      show "map (g  f) = map g [J,C] map f"
      proof -
        have "map (C g f) = J_C.MkArr Dom_f.map Cod_g.map
                                      (constant_transformation.map J C (C g f))"
          using f g map_def by simp
        also have "... = J_C.MkArr Dom_f.map Cod_g.map (λj. if J.arr j then C g f else C.null)"
        proof -
          have "constant_transformation J C (g  f)"
            using g by unfold_locales auto
          thus ?thesis using constant_transformation.map_def by metis
        qed
        also have "... = J_C.comp (J_C.MkArr Cod_f.map Cod_g.map Fun_g.map)
                                  (J_C.MkArr Dom_f.map Cod_f.map Fun_f.map)"
        proof -
          have "J_C.MkArr Cod_f.map Cod_g.map Fun_g.map [J,C]
                J_C.MkArr Dom_f.map Cod_f.map Fun_f.map
                  = J_C.MkArr Dom_f.map Cod_g.map Fun_fg.map"
            using J_C.comp_char J_C.comp_MkArr Fun_f.natural_transformation_axioms
                  Fun_g.natural_transformation_axioms
            by blast
          also have "... = J_C.MkArr Dom_f.map Cod_g.map
                                     (λj. if J.arr j then g  f else C.null)"
            using Fun_fg.is_extensional Fun_fg.map_simp_2 by auto
          finally show ?thesis by auto
        qed
        also have "... = map g [J,C] map f"
          using f g map_def by fastforce
        finally show ?thesis by auto
      qed
    qed

    sublocale "functor" C J_C.comp map
      using is_functor by auto

    text‹
      The objects of [J, C]› correspond bijectively to diagrams of shape @{term J}
      in @{term C}.
›

    lemma ide_determines_diagram:
    assumes "J_C.ide d"
    shows "diagram J C (J_C.Map d)" and "J_C.MkIde (J_C.Map d) = d"
    proof -
      interpret δ: natural_transformation J C J_C.Map d J_C.Map d J_C.Map d
        using assms J_C.ide_char J_C.arr_MkArr by fastforce
      interpret D: "functor" J C J_C.Map d ..
      show "diagram J C (J_C.Map d)" ..
      show "J_C.MkIde (J_C.Map d) = d"
        using assms J_C.ide_char by (metis J_C.ideD(1) J_C.MkArr_Map)
    qed

    lemma diagram_determines_ide:
    assumes "diagram J C D"
    shows "J_C.ide (J_C.MkIde D)" and "J_C.Map (J_C.MkIde D) = D"
    proof -
      interpret D: diagram J C D using assms by auto
      show "J_C.ide (J_C.MkIde D)" using J_C.ide_char
        using D.functor_axioms J_C.ide_MkIde by auto
      thus "J_C.Map (J_C.MkIde D) = D"
        using J_C.in_homE by simp
    qed

    lemma bij_betw_ide_diagram:
    shows "bij_betw J_C.Map (Collect J_C.ide) (Collect (diagram J C))"
    proof (intro bij_betwI)
      show "J_C.Map  Collect J_C.ide  Collect (diagram J C)"
        using ide_determines_diagram by blast
      show "J_C.MkIde  Collect (diagram J C)  Collect J_C.ide"
        using diagram_determines_ide by blast
      show "d. d  Collect J_C.ide  J_C.MkIde (J_C.Map d) = d"
        using ide_determines_diagram by blast
      show "D. D  Collect (diagram J C)  J_C.Map (J_C.MkIde D) = D"
        using diagram_determines_ide by blast
    qed

    text‹
      Arrows from from the diagonal functor correspond bijectively to cones.
›

    lemma arrow_determines_cone:
    assumes "J_C.ide d" and "arrow_from_functor C J_C.comp map a d x"
    shows "cone J C (J_C.Map d) a (J_C.Map x)"
    and "J_C.MkArr (constant_functor.map J C a) (J_C.Map d) (J_C.Map x) = x"
    proof -
      interpret D: diagram J C J_C.Map d
        using assms ide_determines_diagram by auto
      interpret x: arrow_from_functor C J_C.comp map a d x
        using assms by auto
      interpret A: constant_functor J C a
        using x.arrow by (unfold_locales, auto)
      interpret α: constant_transformation J C a
        using x.arrow by (unfold_locales, auto)
      have Dom_x: "J_C.Dom x = A.map"
        using J_C.in_hom_char map_def x.arrow by force
      have Cod_x: "J_C.Cod x = J_C.Map d"
        using x.arrow by auto
      interpret χ: natural_transformation J C A.map J_C.Map d J_C.Map x
        using x.arrow J_C.arr_char [of x] Dom_x Cod_x by force
      show "D.cone a (J_C.Map x)" ..
      show "J_C.MkArr A.map (J_C.Map d) (J_C.Map x) = x"
        using x.arrow Dom_x Cod_x χ.natural_transformation_axioms
        by (intro J_C.arr_eqI, auto)
    qed

    lemma cone_determines_arrow:
    assumes "J_C.ide d" and "cone J C (J_C.Map d) a χ"
    shows "arrow_from_functor C J_C.comp map a d
             (J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ)"
    and "J_C.Map (J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ) = χ"
    proof -
       interpret χ: cone J C J_C.Map d a χ using assms(2) by auto
       let ?x = "J_C.MkArr χ.A.map (J_C.Map d) χ"
       interpret x: arrow_from_functor C J_C.comp map a d ?x
       proof
         have "«J_C.MkArr χ.A.map (J_C.Map d) χ :
                  J_C.MkIde χ.A.map [J,C] J_C.MkIde (J_C.Map d)»"
           using χ.natural_transformation_axioms by auto
         moreover have "J_C.MkIde χ.A.map = map a"
           using χ.A.value_is_ide map_def χ.A.map_def C.ide_char
           by (metis (no_types, lifting) J_C.dom_MkArr preserves_arr preserves_dom)
         moreover have "J_C.MkIde (J_C.Map d) = d"
           using assms ide_determines_diagram(2) by simp
         ultimately show "C.ide a  «J_C.MkArr χ.A.map (J_C.Map d) χ : map a [J,C] d»"
           using χ.A.value_is_ide by simp
       qed
       show "arrow_from_functor C J_C.comp map a d ?x" ..
       show "J_C.Map (J_C.MkArr (constant_functor.map J C a) (J_C.Map d) χ) = χ"
         by (simp add: χ.natural_transformation_axioms)
    qed

    text‹
      Transforming a cone by composing at the apex with an arrow @{term g} corresponds,
      via the preceding bijections, to composition in [J, C]› with the image of @{term g}
      under the diagonal functor.
›

    lemma cones_map_is_composition:
    assumes "«g : a'  a»" and "cone J C D a χ"
    shows "J_C.MkArr (constant_functor.map J C a') D (diagram.cones_map J C D g χ)
             = J_C.MkArr (constant_functor.map J C a) D χ [J,C] map g"
    proof -
      interpret A: constant_transformation J C a
        using assms(1) by (unfold_locales, auto)
      interpret χ: cone J C D a χ using assms(2) by auto
      have cone_χ: "cone J C D a χ" ..
      interpret A': constant_transformation J C a'
        using assms(1) by (unfold_locales, auto)
      let ?χ' = "χ.D.cones_map g χ"
      interpret χ': cone J C D a' ?χ'
        using assms(1) cone_χ χ.D.cones_map_mapsto by blast
      let ?x = "J_C.MkArr χ.A.map D χ"
      let ?x' = "J_C.MkArr χ'.A.map D ?χ'"
      show "?x' = J_C.comp ?x (map g)"
      proof (intro J_C.arr_eqI)
        have x: "J_C.arr ?x"
          using χ.natural_transformation_axioms J_C.arr_char [of ?x] by simp
        show x': "J_C.arr ?x'"
          using χ'.natural_transformation_axioms J_C.arr_char [of ?x'] by simp
        have 3: "«?x : map a [J,C] J_C.MkIde D»"
          using χ.D.diagram_axioms arrow_from_functor.arrow cone_χ cone_determines_arrow(1)
                diagram_determines_ide(1)
          by fastforce
        have 4: "«?x' : map a' [J,C] J_C.MkIde D»"
          by (metis (no_types, lifting) J_C.Dom.simps(1) J_C.Dom_cod J_C.Map_cod
              J_C.cod_MkArr χ'.cone_axioms arrow_from_functor.arrow category.ide_cod
              cone_determines_arrow(1) functor_def is_functor x)
        have seq_xg: "J_C.seq ?x (map g)"
          using assms(1) 3 preserves_hom [of g] by (intro J_C.seqI', auto)
        show 2: "J_C.seq ?x (map g)"
          using seq_xg J_C.seqI' by blast
        show "J_C.Dom ?x' = J_C.Dom (?x [J,C] map g)"
        proof -
          have "J_C.Dom ?x' = J_C.Dom (J_C.dom ?x')"
            using x' J_C.Dom_dom by simp
          also have "... = J_C.Dom (map a')"
            using 4 by force
          also have "... = J_C.Dom (J_C.dom (?x [J,C] map g))"
            using assms(1) 2 by auto
          also have "... = J_C.Dom (?x [J,C] map g)"
            using seq_xg J_C.Dom_dom J_C.seqI' by blast
          finally show ?thesis by auto
        qed
        show "J_C.Cod ?x' = J_C.Cod (?x [J,C] map g)"
        proof -
          have "J_C.Cod ?x' = J_C.Cod (J_C.cod ?x')"
            using x' J_C.Cod_cod by simp
          also have "... = J_C.Cod (J_C.MkIde D)"
            using 4 by force
          also have "... = J_C.Cod (J_C.cod (?x [J,C] map g))"
            using 2 3 J_C.cod_comp J_C.in_homE by metis
          also have "... = J_C.Cod (?x [J,C] map g)"
            using seq_xg J_C.Cod_cod J_C.seqI' by blast
          finally show ?thesis by auto
        qed
        show "J_C.Map ?x' = J_C.Map (?x [J,C] map g)"
        proof -
          interpret g: constant_transformation J C g
            apply unfold_locales using assms(1) by auto
          interpret χog: vertical_composite J C A'.map χ.A.map D g.map χ
            using assms(1) C.comp_arr_dom C.comp_cod_arr A'.is_extensional g.is_extensional
            apply (unfold_locales, auto)
            by (elim J.seqE, auto)
          have "J_C.Map (?x [J,C] map g) = χog.map"
            using assms(1) 2 J_C.comp_char map_def by auto
          also have "... = J_C.Map ?x'"
            using x' χog.map_def J_C.arr_char [of ?x'] natural_transformation.is_extensional
                  assms(1) cone_χ χog.map_simp_2
            by fastforce
          finally show ?thesis by auto
        qed
      qed
    qed

    text‹
      Coextension along an arrow from a functor is equivalent to a transformation of cones.
›

    lemma coextension_iff_cones_map:
    assumes x: "arrow_from_functor C J_C.comp map a d x"
    and g: "«g : a'  a