Theory CategoryWithPullbacks

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

chapter "Category with Pullbacks"

theory CategoryWithPullbacks
imports Limit
begin

text ‹
  \sloppypar
  In this chapter, we give a traditional definition of pullbacks in a category as
  limits of cospan diagrams and we define a locale category_with_pullbacks› that
  is satisfied by categories in which every cospan diagram has a limit.
  These definitions build on the general definition of limit that we gave in
  @{theory Category3.Limit}.  We then define a locale elementary_category_with_pullbacks›
  that axiomatizes categories equipped with chosen functions that assign to each cospan
  a corresponding span of ``projections'', which enjoy the familiar universal property
  of a pullback.  After developing consequences of the axioms, we prove that the two
  locales are in agreement, in the sense that every interpretation of
  category_with_pullbacks› extends to an interpretation of
  elementary_category_with_pullbacks›, and conversely, the underlying category of
  an interpretation of elementary_category_with_pullbacks› always yields an interpretation
  of category_with_pullbacks›.
›

  section "Commutative Squares"

  context category
  begin

    text ‹
      The following provides some useful technology for working with commutative squares.
    ›

    definition commutative_square
    where "commutative_square f g h k  cospan f g  span h k  dom f = cod h  f  h = g  k"

    lemma commutative_squareI [intro, simp]:
    assumes "cospan f g" and "span h k" and "dom f = cod h" and "f  h = g  k"
    shows "commutative_square f g h k"
      using assms commutative_square_def by auto

    lemma commutative_squareE [elim]:
    assumes "commutative_square f g h k"
    and " arr f; arr g; arr h; arr k; cod f = cod g; dom h = dom k; dom f = cod h;
           dom g = cod k; f  h = g  k   T"
    shows T
      using assms commutative_square_def
      by (metis (mono_tags, lifting) seqE seqI)

    lemma commutative_square_comp_arr:
    assumes "commutative_square f g h k" and "seq h l"
    shows "commutative_square f g (h  l) (k  l)"
      using assms
      apply (elim commutative_squareE, intro commutative_squareI, auto)
      using comp_assoc by metis

    lemma arr_comp_commutative_square:
    assumes "commutative_square f g h k" and "seq l f"
    shows "commutative_square (l  f) (l  g) h k"
      using assms comp_assoc
      by (elim commutative_squareE, intro commutative_squareI, auto)

  end

  section "Cospan Diagrams"

  (* TODO: Rework the ugly development of equalizers into this form. *)

  text ‹
    The ``shape'' of a cospan diagram is a category having two non-identity arrows
    with distinct domains and a common codomain.
  ›

  locale cospan_shape
  begin

    datatype Arr = Null | AA | BB | TT | AT | BT

    fun comp
    where "comp AA AA = AA"
        | "comp AT AA = AT"
        | "comp TT AT = AT"
        | "comp BB BB = BB"
        | "comp BT BB = BT"
        | "comp TT BT = BT"
        | "comp TT TT = TT"
        | "comp _ _ = Null"

    interpretation partial_composition comp
    proof
      show "∃!n. f. comp n f = n  comp f n = n"
      proof
        show "f. comp Null f = Null  comp f Null = Null" by simp
        show "n. f. comp n f = n  comp f n = n  n = Null"
          by (metis comp.simps(8))
      qed
    qed

    lemma null_char:
    shows "null = Null"
    proof -
      have "f. comp Null f = Null  comp f Null = Null" by simp
      thus ?thesis
        using null_def ex_un_null theI [of "λn. f. comp n f = n  comp f n = n"]
        by (metis partial_magma.null_is_zero(2) partial_magma_axioms)
    qed

    lemma ide_char:
    shows "ide f  f = AA  f = BB  f = TT"
    proof
      show "ide f  f = AA  f = BB  f = TT"
        using ide_def null_char by (cases f, simp_all)
      show "f = AA  f = BB  f = TT  ide f"
      proof -
        have 1: "f g. f = AA  f = BB  f = TT 
                       comp f f  Null 
                       (comp g f  Null  comp g f = g) 
                       (comp f g  Null  comp f g = g)"
        proof -
          fix f g
          show "f = AA  f = BB  f = TT 
                  comp f f  Null 
                  (comp g f  Null  comp g f = g) 
                  (comp f g  Null  comp f g = g)"
            by (cases f; cases g, auto)
        qed
        assume f: "f = AA  f = BB  f = TT"
        show "ide f"
          using f 1 ide_def null_char by simp
      qed
    qed

    fun Dom
    where "Dom AA = AA"
        | "Dom BB = BB"
        | "Dom TT = TT"
        | "Dom AT = AA"
        | "Dom BT = BB"
        | "Dom _ = Null"

    fun Cod
    where "Cod AA = AA"
        | "Cod BB = BB"
        | "Cod TT = TT"
        | "Cod AT = TT"
        | "Cod BT = TT"
        | "Cod _ = Null"

    lemma domains_char':
    shows "domains f = (if f = Null then {} else {Dom f})"
      using domains_def ide_char null_char
      by (cases f, auto)

    lemma codomains_char':
    shows "codomains f = (if f = Null then {} else {Cod f})"
      using codomains_def ide_char null_char
      by (cases f, auto)

    lemma arr_char:
    shows "arr f  f  Null"
      using arr_def domains_char' codomains_char' by simp

    lemma seq_char:
    shows "seq g f  (f = AA  (g = AA  g = AT)) 
                       (f = BB  (g = BB  g = BT)) 
                       (f = AT  g = TT) 
                       (f = BT  g = TT) 
                       (f = TT  g = TT)"
      using arr_char null_char
      by (cases f; cases g, simp_all)

    interpretation category comp
    proof
      fix f g h
      show "comp g f  null  seq g f"
        using null_char arr_char seq_char by simp
      show "domains f  {}  codomains f  {}"
        using domains_char' codomains_char' by auto
      show "seq h g  seq (comp h g) f  seq g f"
        using seq_char arr_char
        by (cases g; cases h; simp_all)
      show "seq h (comp g f)  seq g f  seq h g"
        using seq_char arr_char
        by (cases f; cases g; simp_all)
      show "seq g f  seq h g  seq (comp h g) f"
        using seq_char arr_char
        by (cases f; simp_all; cases g; simp_all; cases h; auto)
      show "seq g f  seq h g  comp (comp h g) f = comp h (comp g f)"
       using seq_char
       by (cases f; simp_all; cases g; simp_all; cases h; auto)
    qed

    lemma is_category:
    shows "category comp"
      ..

    lemma dom_char:
    shows "dom = Dom"
      using dom_def domains_char domains_char' null_char by fastforce

    lemma cod_char:
    shows "cod = Cod"
      using cod_def codomains_char codomains_char' null_char by fastforce

  end

  sublocale cospan_shape  category comp
    using is_category by auto

  locale cospan_diagram =
    J: cospan_shape +
    C: category C
  for C :: "'c comp"      (infixr "" 55)
  and f0 :: 'c
  and f1 :: 'c +
  assumes is_cospan: "C.cospan f0 f1"
  begin

    no_notation J.comp   (infixr "" 55)
    notation J.comp      (infixr "J" 55)

    fun map
    where "map J.AA = C.dom f0"
        | "map J.BB = C.dom f1"
        | "map J.TT = C.cod f0"
        | "map J.AT = f0"
        | "map J.BT = f1"
        | "map _ = C.null"

  end

  sublocale cospan_diagram  diagram J.comp C map
  proof
    show "f. ¬ J.arr f  map f = C.null"
      using J.arr_char by simp
    fix f
    assume f: "J.arr f"
    show "C.arr (map f)"
      using f J.arr_char is_cospan by (cases f, simp_all)
    show "C.dom (map f) = map (J.dom f)"
      using f J.arr_char J.dom_char is_cospan by (cases f, simp_all)
    show "C.cod (map f) = map (J.cod f)"
      using f J.arr_char J.cod_char is_cospan by (cases f, simp_all)
    next
    fix f g
    assume fg: "J.seq g f"
    show "map (g J f) = map g  map f"
      using fg J.seq_char J.null_char J.not_arr_null is_cospan
      apply (cases f; cases g, simp_all)
      using C.comp_arr_dom C.comp_cod_arr by auto
  qed

  section "Category with Pullbacks"

  text ‹
    A \emph{pullback} in a category @{term C} is a limit of a cospan diagram in @{term C}.
  ›

  context cospan_diagram
  begin

    definition mkCone
    where "mkCone p0 p1  λj. if j = J.AA then p0
                               else if j = J.BB then p1
                               else if j = J.AT then f0  p0
                               else if j = J.BT then f1  p1
                               else if j = J.TT then f0  p0
                               else C.null"

    abbreviation is_rendered_commutative_by
    where "is_rendered_commutative_by p0 p1  C.seq f0 p0  f0  p0 = f1  p1"

    abbreviation has_as_pullback
    where "has_as_pullback p0 p1  limit_cone (C.dom p0) (mkCone p0 p1)"

    lemma cone_mkCone:
    assumes "is_rendered_commutative_by p0 p1"
    shows "cone (C.dom p0) (mkCone p0 p1)"
    proof -
      interpret E: constant_functor J.comp C C.dom p0
        apply unfold_locales using assms by auto
      show "cone (C.dom p0) (mkCone p0 p1)"
      proof
        fix f
        show "¬ J.arr f  mkCone p0 p1 f = C.null"
          using mkCone_def J.arr_char by simp
        assume f: "J.arr f"
        show "C.dom (mkCone p0 p1 f) = E.map (J.dom f)"
          using assms f mkCone_def J.arr_char J.dom_char
          apply (cases f, simp_all)
          by (metis C.dom_comp)+
        show "C.cod (mkCone p0 p1 f) = map (J.cod f)"
          using assms f mkCone_def J.arr_char J.cod_char is_cospan
          by (cases f, auto)
        show "map f  mkCone p0 p1 (J.dom f) = mkCone p0 p1 f"
          using assms f mkCone_def J.arr_char J.dom_char C.comp_ide_arr is_cospan
          by (cases f, auto)
        show "mkCone p0 p1 (J.cod f)  E.map f = mkCone p0 p1 f"
          using assms f mkCone_def J.arr_char J.cod_char C.comp_arr_dom
          apply (cases f, auto)
             apply (metis C.dom_comp C.seqE)
          by (metis C.dom_comp)+
      qed
    qed

    lemma is_rendered_commutative_by_cone:
    assumes "cone a χ"
    shows "is_rendered_commutative_by (χ J.AA) (χ J.BB)"
    proof -
      interpret χ: cone J.comp C map a χ
        using assms by auto
      show ?thesis
      proof
        show "C.seq f0 (χ J.AA)"
          by (metis C.seqI J.cod_char J.seq_char χ.preserves_cod χ.preserves_reflects_arr
              J.seqE is_cospan J.Cod.simps(1) map.simps(1))
        show "f0  χ J.AA = f1  χ J.BB"
          by (metis J.cod_char J.dom_char χ.A.map_simp χ.naturality
              J.Cod.simps(4-5) J.Dom.simps(4-5) J.comp.simps(2,5) J.seq_char map.simps(4-5))
      qed
    qed

    lemma mkCone_cone:
    assumes "cone a χ"
    shows "mkCone (χ J.AA) (χ J.BB) = χ"
    proof -
      interpret χ: cone J.comp C map a χ
        using assms by auto
      have 1: "is_rendered_commutative_by (χ J.AA) (χ J.BB)"
        using assms is_rendered_commutative_by_cone by blast
      interpret mkCone_χ: cone J.comp C map C.dom (χ J.AA) mkCone (χ J.AA) (χ J.BB)
        using assms cone_mkCone 1 by auto
      show ?thesis
      proof -
        have "j. j = J.AA  mkCone (χ J.AA) (χ J.BB) j = χ j"
          using mkCone_def χ.is_extensional by simp
        moreover have "j. j = J.BB  mkCone (χ J.AA) (χ J.BB) j = χ j"
          using mkCone_def χ.is_extensional by simp
        moreover have "j. j = J.TT  mkCone (χ J.AA) (χ J.BB) j = χ j"
          using 1 mkCone_def χ.is_extensional χ.A.map_simp χ.preserves_comp_1
                cospan_shape.seq_char χ.is_natural_2
          apply simp
          by (metis J.seqE J.comp.simps(5) map.simps(5))
        ultimately have "j. J.ide j  mkCone (χ J.AA) (χ J.BB) j = χ j"
          using J.ide_char by auto
        thus "mkCone (χ J.AA) (χ J.BB) = χ"
          using mkCone_def NaturalTransformation.eqI [of J.comp C]
                χ.natural_transformation_axioms mkCone_χ.natural_transformation_axioms
                J.ide_char
          by simp
      qed
    qed

    lemma cone_iff_commutative_square:
    shows "cone (C.dom h) (mkCone h k)  C.commutative_square f0 f1 h k"
      using cone_mkCone mkCone_def J.arr_char J.ide_char is_rendered_commutative_by_cone
            is_cospan C.commutative_square_def cospan_shape.Arr.simps(11)
            C.dom_comp C.seqE C.seqI
      apply (intro iffI)
      by (intro C.commutative_squareI) metis+

    lemma cones_map_mkCone_eq_iff:
    assumes "is_rendered_commutative_by p0 p1" and "is_rendered_commutative_by p0' p1'"
    and "«h : C.dom p0'  C.dom p0»"
    shows "cones_map h (mkCone p0 p1) = mkCone p0' p1'  p0  h = p0'  p1  h = p1'"
    proof -
      interpret χ: cone J.comp C map C.dom p0 mkCone p0 p1
        using assms(1) cone_mkCone [of p0 p1] by blast
      interpret χ': cone J.comp C map C.dom p0' mkCone p0' p1'
        using assms(2) cone_mkCone [of p0' p1'] by blast
      show ?thesis
      proof
        assume 3: "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
        show "p0  h = p0'  p1  h = p1'"
        proof
          show "p0  h = p0'"
          proof -
            have "p0' = mkCone p0' p1' J.AA"
              using mkCone_def J.arr_char by simp
            also have "... = cones_map h (mkCone p0 p1) J.AA"
              using 3 by simp
            also have "... = p0  h"
              using assms mkCone_def J.arr_char χ.cone_axioms by auto
            finally show ?thesis by auto
          qed
          show "p1  h = p1'"
          proof -
            have "p1' = mkCone p0' p1' J.BB"
              using mkCone_def J.arr_char by simp
            also have "... = cones_map h (mkCone p0 p1) J.BB"
              using 3 by simp
            also have "... = p1  h"
              using assms mkCone_def J.arr_char χ.cone_axioms by auto
            finally show ?thesis by auto
          qed
        qed
        next
        assume 4: "p0  h = p0'  p1  h = p1'"
        show "cones_map h (mkCone p0 p1) = mkCone p0' p1'"
        proof
          fix j
          have "¬ J.arr j  cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
            using assms χ.cone_axioms mkCone_def J.arr_char by auto
          moreover have "J.arr j  cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
            using assms 4 χ.cone_axioms mkCone_def J.arr_char C.comp_assoc
            by fastforce
          ultimately show "cones_map h (mkCone p0 p1) j = mkCone p0' p1' j"
            using J.arr_char J.Dom.cases by blast
        qed
      qed
    qed

  end

  locale pullback_cone =
    J: cospan_shape +
    C: category C +
    D: cospan_diagram C f0 f1 +
    limit_cone J.comp C D.map C.dom p0 D.mkCone p0 p1
  for C :: "'c comp"      (infixr "" 55)
  and f0 :: 'c
  and f1 :: 'c
  and p0 :: 'c
  and p1 :: 'c
  begin

    (* TODO: Equalizer should be simplifiable in the same way. *)
    lemma renders_commutative:
    shows "D.is_rendered_commutative_by p0 p1"
      using D.mkCone_def D.cospan_diagram_axioms cone_axioms
            cospan_diagram.is_rendered_commutative_by_cone
      by fastforce

    lemma is_universal':
    assumes "D.is_rendered_commutative_by p0' p1'"
    shows "∃!h. «h : C.dom p0'  C.dom p0»  p0  h = p0'  p1  h = p1'"
    proof -
      have "D.cone (C.dom p0') (D.mkCone p0' p1')"
        using assms D.cone_mkCone by blast
      hence 1: "∃!h. «h : C.dom p0'  C.dom p0» 
                     D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1'"
        using is_universal by simp
      have 2: "h. «h : C.dom p0'  C.dom p0» 
                    D.cones_map h (D.mkCone p0 p1) = D.mkCone p0' p1' 
                    p0  h = p0'  p1  h = p1'"
        using assms D.cones_map_mkCone_eq_iff [of p0 p1 p0' p1'] renders_commutative
        by fastforce
      thus ?thesis using 1 by blast
    qed

    lemma induced_arrowI':
    assumes "D.is_rendered_commutative_by p0' p1'"
    shows "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0'  C.dom p0»"
    and "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
    and "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
    proof -
      interpret A': constant_functor J.comp C C.dom p0'
        using assms by (unfold_locales, auto)
      have cone: "D.cone (C.dom p0') (D.mkCone p0' p1')"
        using assms D.cone_mkCone [of p0' p1'] by blast
      show 1: "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') = p0'"
      proof -
        have "p0  induced_arrow (C.dom p0') (D.mkCone p0' p1') =
                D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
                            (D.mkCone p0 p1) J.AA"
          using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
        also have "... = p0'"
        proof -
          have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
                            (D.mkCone p0 p1) =
                D.mkCone p0' p1'"
            using cone induced_arrowI by blast
          thus ?thesis
            using J.arr_char D.mkCone_def by simp
        qed
        finally show ?thesis by auto
      qed
      show 2: "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') = p1'"
      proof -
        have "p1  induced_arrow (C.dom p1') (D.mkCone p0' p1') =
              D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
                          (D.mkCone p0 p1) J.BB"
        proof -
          have "C.dom p0' = C.dom p1'"
            using assms by (metis C.dom_comp)
          thus ?thesis
            using cone induced_arrowI(1) D.mkCone_def J.arr_char is_cone by force
        qed
        also have "... = p1'"
        proof -
          have "D.cones_map (induced_arrow (C.dom p0') (D.mkCone p0' p1'))
                            (D.mkCone p0 p1) =
                D.mkCone p0' p1'"
            using cone induced_arrowI by blast
          thus ?thesis
            using J.arr_char D.mkCone_def by simp
        qed
        finally show ?thesis by auto
      qed
      show "«induced_arrow (C.dom p0') (D.mkCone p0' p1') : C.dom p0'  C.dom p0»"
        using 1 cone induced_arrowI by simp
    qed

  end

  context category
  begin

    definition has_as_pullback
    where "has_as_pullback f0 f1 p0 p1 
           cospan f0 f1  cospan_diagram.has_as_pullback C f0 f1 p0 p1"

    definition has_pullbacks
    where "has_pullbacks = (f0 f1. cospan f0 f1  (p0 p1. has_as_pullback f0 f1 p0 p1))"

    lemma has_as_pullbackI [intro]:
    assumes "cospan f g" and "commutative_square f g p q"
    and "h k. commutative_square f g h k  ∃!l. p  l = h  q  l = k"
    shows "has_as_pullback f g p q"
    proof (unfold has_as_pullback_def, intro conjI)
      show "arr f" and "arr g" and "cod f = cod g"
        using assms(1) by auto
      interpret J: cospan_shape .
      interpret D: cospan_diagram C f g
        using assms(1-2) by unfold_locales auto
      show "D.has_as_pullback p q"
      proof -
        have 1: "D.is_rendered_commutative_by p q"
          using assms ide_in_hom by blast
        let  = "D.mkCone p q"
        let ?a = "dom p"
        interpret χ: cone J.comp C D.map ?a 
           using assms(2) D.cone_mkCone 1 by auto
        interpret χ: limit_cone J.comp C D.map ?a 
        proof
          fix x χ'
          assume χ': "D.cone x χ'"
          interpret χ': cone J.comp C D.map x χ'
            using χ' by simp
          have 2: "D.is_rendered_commutative_by (χ' J.AA) (χ' J.BB)"
            using χ' D.is_rendered_commutative_by_cone [of x χ'] by blast
          have 3: "∃!l. p  l = χ' J.AA  q  l = χ' J.BB"
            using assms(1,3) 2 χ'.preserves_hom J.arr_char J.ide_char by simp
          obtain l where l: "p  l = χ' J.AA  q  l = χ' J.BB"
            using 3 by blast
          have "«l : x  ?a»"
            using l 2 χ'.preserves_hom J.arr_char J.ide_char χ'.component_in_hom
                  χ'.is_extensional χ'.preserves_reflects_arr comp_in_homE null_is_zero(2) in_homE
            by metis
          moreover have "D.cones_map l (D.mkCone p q) = χ'"
            using l D.cones_map_mkCone_eq_iff [of p q "χ' J.AA" "χ' J.BB" l]
            by (metis (no_types, lifting) 1 2 D.mkCone_cone χ' calculation dom_comp in_homE seqE)
          ultimately have "l. «l : x  ?a»  D.cones_map l (D.mkCone p q) = χ'"
            by blast
          moreover have "l'. «l' : x  ?a»; D.cones_map l' (D.mkCone p q) = χ'  l' = l"
          proof -
            fix l'
            assume l': "«l' : x  ?a»"
            assume eq: "D.cones_map l' (D.mkCone p q) = χ'"
            have "p  l' = χ' J.AA  q  l' = χ' J.BB"
              using l' eq J.arr_char χ.cone_axioms D.mkCone_def by auto
            thus "l' = l"
              using 3 l by blast
          qed
          ultimately show "∃!l. «l : x  ?a»  D.cones_map l (D.mkCone p q) = χ'"
            by blast
        qed
        show "D.has_as_pullback p q"
          using assms χ.limit_cone_axioms by blast
      qed
    qed

    lemma pullbacks_are_isomorphic:
    assumes "has_as_pullback f g h k" and "has_as_pullback f g h' k'"
    shows "isomorphic (dom h) (dom h')"
      using assms limits_are_isomorphic(1)
      unfolding has_as_pullback_def by blast

    lemma has_as_pullbackE [elim]:
    assumes "has_as_pullback f g p q"
    and "cospan f g; commutative_square f g p q;
          h k. commutative_square f g h k  ∃!l. p  l = h  q  l = k  T"
    shows T
    proof -
      interpret J: cospan_shape .
      interpret D: cospan_diagram C f g
        using assms(1) has_as_pullback_def
        by (meson category_axioms cospan_diagram.intro cospan_diagram_axioms.intro)
      have 1: "h k. commutative_square f g h k  D.cone (dom h) (D.mkCone h k)"
        using D.cone_iff_commutative_square by presburger
      let  = "D.mkCone p q"
      interpret χ: limit_cone J.comp C D.map dom p 
        using assms(1) has_as_pullback_def D.cone_mkCone by blast
      have "cospan f g"
        using D.is_cospan by blast
      moreover have csq: "commutative_square f g p q"
        using 1 χ.cone_axioms by blast
      moreover have "h k. commutative_square f g h k  ∃!l. p  l = h  q  l = k"
      proof -
        fix h k
        assume 2: "commutative_square f g h k"
        let ?χ' = "D.mkCone h k"
        interpret χ': cone J.comp C D.map dom h ?χ'
          using 1 2 by blast
        have 3: "∃!l. «l : dom h  dom p»  D.cones_map l  = ?χ'"
          using 1 2 χ.is_universal [of "dom h" "D.mkCone h k"] by blast
        obtain l where l: "«l : dom h  dom p»  D.cones_map l  = ?χ'"
          using 3 by blast
        have "p  l = h  q  l = k"
        proof
          have "p  l = D.cones_map l  J.AA"
            using χ.cone_axioms D.mkCone_def J.seq_char in_homE
            apply simp
            by (metis J.seqE l)
          also have "... = h"
            using l χ'.cone_axioms D.mkCone_def J.seq_char in_homE by simp
          finally show "p  l = h" by blast
          have "q  l = D.cones_map l  J.BB"
            using χ.cone_axioms D.mkCone_def J.seq_char in_homE
            apply simp
            by (metis J.seqE l)
          also have "... = k"
            using l χ'.cone_axioms D.mkCone_def J.seq_char in_homE by simp
          finally show "q  l = k" by blast
        qed
        moreover have "l'. p  l' = h  q  l' = k  l' = l"
        proof -
          fix l'
          assume 1: "p  l' = h  q  l' = k"
          have 2: "«l' : dom h  dom p»"
            using 1
            by (metis χ'.ide_apex arr_dom_iff_arr arr_iff_in_hom ideD(1) seqE dom_comp)
          moreover have "D.cones_map l'  = ?χ'"
            using D.cones_map_mkCone_eq_iff
            by (meson 1 2 csq D.cone_iff_commutative_square χ'.cone_axioms
                      commutative_squareE seqI)
          ultimately show "l' = l"
            using l χ.is_universal χ'.cone_axioms by blast
        qed
        ultimately show "∃!l. p  l = h  q  l = k" by blast
      qed
      ultimately show T
        using assms(2) by blast
    qed

  end

  locale category_with_pullbacks =
    category +
  assumes has_pullbacks: has_pullbacks

  section "Elementary Category with Pullbacks"

  text ‹
    An \emph{elementary category with pullbacks} is a category equipped with a specific
    way of mapping each cospan to a span such that the resulting square commutes and
    such that the span is universal for that property.  It is useful to assume that the
    functions, mapping a cospan to the two projections of the pullback, are extensional;
    that is, they yield @{term null} when applied to arguments that do not form a cospan.
  ›

  locale elementary_category_with_pullbacks =
    category C
  for C :: "'a comp"                              (infixr "" 55)
  and prj0 :: "'a  'a  'a"                    ("𝗉0[_, _]")
  and prj1 :: "'a  'a  'a"                    ("𝗉1[_, _]") +
  assumes prj0_ext: "¬ cospan f g  𝗉0[f, g] = null"
  and prj1_ext: "¬ cospan f g  𝗉1[f, g] = null"
  and pullback_commutes [intro]: "cospan f g  commutative_square f g 𝗉1[f, g] 𝗉0[f, g]"
  and universal: "commutative_square f g h k  ∃!l. 𝗉1[f, g]  l = h  𝗉0[f, g]  l = k"
  begin

    lemma pullback_commutes':
    assumes "cospan f g"
    shows "f  𝗉1[f, g] = g  𝗉0[f, g]"
      using assms commutative_square_def by blast

    lemma prj0_in_hom':
    assumes "cospan f g"
    shows "«𝗉0[f, g] : dom 𝗉0[f, g]  dom g»"
      using assms pullback_commutes
      by (metis category.commutative_squareE category_axioms in_homI)

    lemma prj1_in_hom':
    assumes "cospan f g"
    shows "«𝗉1[f, g] : dom 𝗉0[f, g]  dom f»"
      using assms pullback_commutes
      by (metis category.commutative_squareE category_axioms in_homI)

    text ‹
      The following gives us a notation for the common domain of the two projections
      of a pullback.
    ›

    definition pbdom        (infix "↓↓" 51)
    where "f ↓↓ g  dom 𝗉0[f, g]"

    lemma pbdom_in_hom [intro]:
    assumes "cospan f g"
    shows "«f ↓↓ g : f ↓↓ g  f ↓↓ g»"
      unfolding pbdom_def
      using assms prj0_in_hom'
      by (metis arr_dom_iff_arr arr_iff_in_hom cod_dom dom_dom in_homE)

    lemma ide_pbdom [simp]:
    assumes "cospan f g"
    shows "ide (f ↓↓ g)"
      using assms ide_in_hom by auto[1]

    lemma prj0_in_hom [intro, simp]:
    assumes "cospan f g" and "a = f ↓↓ g" and "b = dom g"
    shows "«𝗉0[f, g] : a  b»"
      unfolding pbdom_def
      using assms prj0_in_hom' by (simp add: pbdom_def)

    lemma prj1_in_hom [intro, simp]:
    assumes "cospan f g" and "a = f ↓↓ g" and "b = dom f"
    shows "«𝗉1[f, g] : a  b»"
      unfolding pbdom_def
      using assms prj1_in_hom' by (simp add: pbdom_def)

    lemma prj0_simps [simp]:
    assumes "cospan f g"
    shows "arr 𝗉0[f, g]" and "dom 𝗉0[f, g] = f ↓↓ g" and "cod 𝗉0[f, g] = dom g"
      using assms prj0_in_hom by (blast, blast, blast)

    lemma prj0_simps_arr [iff]:
    shows "arr 𝗉0[f, g]  cospan f g"
    proof
      show "cospan f g  arr 𝗉0[f, g]"
        using prj0_in_hom by auto
      show "arr 𝗉0[f, g]  cospan f g"
        using prj0_ext not_arr_null by metis
    qed

    lemma prj1_simps [simp]:
    assumes "cospan f g"
    shows "arr 𝗉1[f, g]" and "dom 𝗉1[f, g] = f ↓↓ g" and "cod 𝗉1[f, g] = dom f"
      using assms prj1_in_hom by (blast, blast, blast)

    lemma prj1_simps_arr [iff]:
    shows "arr 𝗉1[f, g]  cospan f g"
    proof
      show "cospan f g  arr 𝗉1[f, g]"
        using prj1_in_hom by auto
      show "arr 𝗉1[f, g]  cospan f g"
        using prj1_ext not_arr_null by metis
    qed

    lemma span_prj:
    assumes "cospan f g"
    shows "span 𝗉0[f, g] 𝗉1[f, g]"
      using assms by simp

    text ‹
      We introduce a notation for tupling, which produces the induced arrow into a pullback.
      In our notation, the ``$0$-side'', which we regard as the input, occurs on the right,
      and the ``$1$-side'', which we regard as the output, occurs on the left.
    ›

    definition tuple         ("_ _, _ _")
    where "h f, g k  if commutative_square f g h k then
                           THE l. 𝗉0[f, g]  l = k  𝗉1[f, g]  l = h
                         else null"

    lemma tuple_in_hom [intro]:
    assumes "commutative_square f g h k"
    shows "«h f, g k : dom h  f ↓↓ g»"
    proof
      have 1: "𝗉0[f, g]  h f, g k = k  𝗉1[f, g]  h f, g k = h"
        unfolding tuple_def
        using assms universal theI [of "λl. 𝗉0[f, g]  l = k  𝗉1[f, g]  l = h"]
        apply simp
        by meson
      show "arr h f, g k"
        using assms 1
        apply (elim commutative_squareE)
        by (metis (no_types, lifting) seqE)
      show "dom h f, g k = dom h"
        using assms 1
        apply (elim commutative_squareE)
        by (metis (no_types, lifting) dom_comp)
      show "cod h f, g k = f ↓↓ g"
        unfolding pbdom_def
        using assms 1
        apply (elim commutative_squareE)
        by (metis seqE)
    qed

    lemma tuple_is_extensional:
    assumes "¬ commutative_square f g h k"
    shows "h f, g k = null"
      unfolding tuple_def
      using assms by simp

    lemma tuple_simps [simp]:
    assumes "commutative_square f g h k"
    shows "arr h f, g k" and "dom h f, g k = dom h" and "cod h f, g k = f ↓↓ g"
      using assms tuple_in_hom apply blast
      using assms tuple_in_hom apply blast
      using assms tuple_in_hom by blast

    lemma prj_tuple [simp]:
    assumes "commutative_square f g h k"
    shows "𝗉0[f, g]  h f, g k = k" and "𝗉1[f, g]  h f, g k = h"
    proof -
      have 1: "𝗉0[f, g]  h f, g k = k  𝗉1[f, g]  h f, g k = h"
        unfolding tuple_def
        using assms universal theI [of "λl. 𝗉0[f, g]  l = k  𝗉1[f, g]  l = h"]
        apply simp
        by meson
      show "𝗉0[f, g]  h f, g k = k" using 1 by simp
      show "𝗉1[f, g]  h f, g k = h" using 1 by simp
    qed

    lemma tuple_prj:
    assumes "cospan f g" and "seq 𝗉1[f, g] h"
    shows "𝗉1[f, g]  h f, g 𝗉0[f, g]  h = h"
    proof -
      have 1: "commutative_square f g (𝗉1[f, g]  h) (𝗉0[f, g]  h)"
        using assms pullback_commutes
        by (simp add: commutative_square_comp_arr)
      have "𝗉0[f, g]  𝗉1[f, g]  h f, g 𝗉0[f, g]  h = 𝗉0[f, g]  h"
        using assms 1 by simp
      moreover have "𝗉1[f, g]  𝗉1[f, g]  h f, g 𝗉0[f, g]  h = 𝗉1[f, g]  h"
        using assms 1 by simp
      ultimately show ?thesis
        unfolding tuple_def
        using assms 1 universal [of f g "𝗉1[f, g]  h" "𝗉0[f, g]  h"]
              theI_unique [of "λl. 𝗉0[f, g]  l = 𝗉0[f, g]  h  𝗉1[f, g]  l = 𝗉1[f, g]  h" h]
        by auto
    qed

    lemma tuple_prj_spc [simp]:
    assumes "cospan f g"
    shows "𝗉1[f, g] f, g 𝗉0[f, g] = f ↓↓ g"
    proof -
      have "𝗉1[f, g] f, g 𝗉0[f, g] = 𝗉1[f, g]  (f ↓↓ g) f, g 𝗉0[f, g]  (f ↓↓ g)"
        using assms comp_arr_dom by simp
      thus ?thesis
        using assms tuple_prj by simp
    qed

    lemma prj_joint_monic:
    assumes "cospan f g" and "seq 𝗉1[f, g] h" and "seq 𝗉1[f, g] h'"
    and "𝗉0[f, g]  h = 𝗉0[f, g]  h'" and "𝗉1[f, g]  h = 𝗉1[f, g]  h'"
    shows "h = h'"
    proof -
      have "h = 𝗉1[f, g]  h f, g 𝗉0[f, g]  h"
        using assms tuple_prj [of f g h] by simp
      also have "... = 𝗉1[f, g]  h' f, g 𝗉0[f, g]  h'"
        using assms by simp
      also have "... = h'"
        using assms tuple_prj [of f g h'] by simp
      finally show ?thesis by blast
    qed

    text ‹
      The pullback of an identity along an arbitrary arrow is an isomorphism.
    ›

    lemma iso_pullback_ide:
    assumes "cospan μ ν" and "ide μ"
    shows "iso 𝗉0[μ, ν]"
    proof -
      have "inverse_arrows 𝗉0[μ, ν] ν μ, ν dom ν"
      proof
        show 1: "ide (𝗉0[μ, ν]  ν μ, ν dom ν)"
          using assms comp_arr_dom comp_cod_arr prj_tuple(1) by simp
        show "ide (ν μ, ν dom ν  𝗉0[μ, ν])"
        proof -
          have "ν μ, ν dom ν  𝗉0[μ, ν] = (μ ↓↓ ν)"
          proof -
            have "𝗉0[μ, ν]  ν μ, ν dom ν  𝗉0[μ, ν] = 𝗉0[μ, ν]  (μ ↓↓ ν)"
            proof -
              have "𝗉0[μ, ν]  ν μ, ν dom ν  𝗉0[μ, ν] = (𝗉0[μ, ν]  ν μ, ν dom ν)  𝗉0[μ, ν]"
                using assms 1 comp_reduce by blast
              also have "... = 𝗉0[μ, ν]  (μ ↓↓ ν)"
                using assms prj_tuple(1) pullback_commutes comp_arr_dom comp_cod_arr by simp
              finally show ?thesis by blast
            qed
            moreover have "𝗉1[μ, ν]  ν μ, ν dom ν  𝗉0[μ, ν] = 𝗉1[μ, ν]  (μ ↓↓ ν)"
            proof -
              have "𝗉1[μ, ν]  ν μ, ν dom ν  𝗉0[μ, ν] = (𝗉1[μ, ν]  ν μ, ν dom ν)  𝗉0[μ, ν]"
                using assms(2) comp_assoc by simp
              also have "... = ν  𝗉0[μ, ν]"
                using assms comp_arr_dom comp_cod_arr prj_tuple(2) by fastforce
              also have "... = μ  𝗉1[μ, ν]"
                using assms pullback_commutes commutative_square_def by simp
              also have "... = 𝗉1[μ, ν]  (μ ↓↓ ν)"
                using assms comp_arr_dom comp_cod_arr pullback_commutes commutative_square_def
                by simp
              finally show ?thesis by simp
            qed
            ultimately show ?thesis
              using assms prj0_in_hom prj1_in_hom comp_arr_dom prj1_simps(1-2) prj_joint_monic
              by metis
          qed
          thus ?thesis
            using assms by auto
        qed
      qed
      thus ?thesis by auto
    qed

    lemma comp_tuple_arr:
    assumes "commutative_square f g h k" and "seq h l"
    shows "h f, g k  l = h  l f, g k  l"
    proof -
      have "𝗉0[f, g]  h f, g k  l = 𝗉0[f, g]  h  l f, g k  l"
      proof -
        have "𝗉0[f, g]  h f, g k  l = (𝗉0[f, g]  h f, g k)  l"
          using comp_assoc by simp
        also have "... = 𝗉0[f, g]  h  l f, g k  l"
          using assms commutative_square_comp_arr by auto
        finally show ?thesis by blast
      qed
      moreover have "𝗉1[f, g]  h f, g k  l = 𝗉1[f, g]  h  l f, g k  l"
      proof -
        have "𝗉1[f, g]  h f, g k  l = (𝗉1[f, g]  h f, g k)  l"
          using comp_assoc by simp
        also have "... = 𝗉1[f, g]  h  l f, g k  l"
          using assms commutative_square_comp_arr by auto
        finally show ?thesis by blast
      qed
      moreover have "seq 𝗉1[f, g] (h f, g k  l)"
        using assms tuple_in_hom prj1_in_hom by fastforce
      ultimately show ?thesis
        using assms prj_joint_monic [of f g "h f, g k  l" "h  l f, g k  l"]
        by auto
    qed

    lemma pullback_arr_cod:
    assumes "arr f"
    shows "inverse_arrows 𝗉1[f, cod f] dom f f, cod f f"
    and "inverse_arrows 𝗉0[cod f, f] f cod f, f dom f"
    proof -
      show "inverse_arrows 𝗉1[f, cod f] dom f f, cod f f"
      proof
        show "ide (dom f f, cod f f  𝗉1[f, cod f])"
        proof -
          have "dom f f, cod f f  𝗉1[f, cod f] = f ↓↓ cod f"
          proof -
            have "𝗉0[f, cod f]  dom f f, cod f f  𝗉1[f, cod f] = 𝗉0[f, cod f]  (f ↓↓ cod f)"
            proof -
              have "𝗉0[f, cod f]  dom f f, cod f f  𝗉1[f, cod f] =
                    (𝗉0[f, cod f]  dom f f, cod f f)  𝗉1[f, cod f]"
                using comp_assoc by simp
              also have "... = 𝗉0[f, cod f]  (f ↓↓ cod f)"
                using assms pullback_commutes [of f "cod f"] comp_arr_dom comp_cod_arr
                by auto
              finally show ?thesis by blast
            qed
            moreover
            have "𝗉1[f, cod f]  dom f f, cod f f  𝗉1[f, cod f] = 𝗉1[f, cod f]  (f ↓↓ cod f)"
            proof -
              have "𝗉1[f, cod f]  dom f f, cod f f  𝗉1[f, cod f] =
                    (𝗉1[f, cod f]  dom f f, cod f f)  𝗉1[f, cod f]"
                using assms comp_assoc by presburger
              also have "... = 𝗉1[f, cod f]  (f ↓↓ cod f)"
                using assms comp_arr_dom comp_cod_arr by simp
              finally show ?thesis by blast
            qed
            ultimately show ?thesis
              using assms
                    prj_joint_monic
                      [of f "cod f" "dom f f, cod f f  𝗉1[f, cod f]" "f ↓↓ cod f"]
              by simp
          qed
          thus ?thesis
            using assms arr_cod cod_cod prj1_simps_arr by simp
        qed
        show "ide (𝗉1[f, cod f]  dom f f, cod f f)"
          using assms comp_arr_dom comp_cod_arr by fastforce
      qed
      show "inverse_arrows 𝗉0[cod f, f] f cod f, f dom f"
      proof
        show "ide (𝗉0[cod f, f]  f cod f, f dom f)"
          using assms comp_arr_dom comp_cod_arr by simp
        show "ide (f cod f, f dom f  𝗉0[cod f, f])"
        proof -
          have "f cod f, f dom f  𝗉0[cod f, f] = cod f ↓↓ f"
          proof -
            have "𝗉0[cod f, f]  f cod f, f dom f  𝗉0[cod f, f] = 𝗉0[cod f, f]  (cod f ↓↓ f)"
            proof -
              have "𝗉0[cod f, f]  f cod f, f dom f  𝗉0[cod f, f] =
                    (𝗉0[cod f, f]  f cod f, f dom f)  𝗉0[cod f, f]"
                using comp_assoc by simp
              also have "... = dom f  𝗉0[cod f, f]"
                using assms comp_arr_dom comp_cod_arr by simp
              also have "... = 𝗉0[cod f, f]  (cod f ↓↓ f)"
                using assms comp_arr_dom comp_cod_arr by simp
              finally show ?thesis
                using prj0_in_hom by blast
            qed
            moreover
            have "𝗉1[cod f, f]  f cod f, f dom f  𝗉0[cod f, f] = 𝗉1[cod f, f]  (cod f ↓↓ f)"
            proof -
              have "𝗉1[cod f, f]  f cod f, f dom f  𝗉0[cod f, f] =
                    (𝗉1[cod f, f]  f cod f, f dom f)  𝗉0[cod f, f]"
                using comp_assoc by simp
              also have "... = 𝗉1[cod f, f]  (cod f ↓↓ f)"
                using assms pullback_commutes [of "cod f" f] comp_arr_dom comp_cod_arr
                by auto
              finally show ?thesis by blast
            qed
            ultimately show ?thesis
              using assms prj_joint_monic [of "cod f" f "f cod f, f dom f  𝗉0[cod f, f]"]
              by simp
          qed
          thus ?thesis using assms by simp
        qed
      qed
    qed

    text ‹
      The pullback of a monomorphism along itself is automatically symmetric: the left
      and right projections are equal.
    ›

    lemma pullback_mono_self:
    assumes "mono f"
    shows "𝗉0[f, f] = 𝗉1[f, f]"
    proof -
      have "f  𝗉0[f, f] = f  𝗉1[f, f]"
        using assms pullback_commutes [of f f]
        by (metis commutative_squareE mono_implies_arr)
      thus ?thesis
        using assms monoE [of f "𝗉1[f, f]" "𝗉0[f, f]"]
        by (metis mono_implies_arr prj0_simps(1,3) seqI)
    qed

    lemma pullback_iso_self:
    assumes "iso f"
    shows "𝗉0[f, f] = 𝗉1[f, f]"
      using assms pullback_mono_self iso_is_section section_is_mono by simp

    lemma pullback_ide_self [simp]:
    assumes "ide a"
    shows "𝗉0[a, a] = 𝗉1[a, a]"
      using assms pullback_iso_self ide_is_iso by blast

  end

  section "Agreement between the Definitions"

  text ‹
    It is very easy to write locale assumptions that have unintended consequences
    or that are even inconsistent.  So, to keep ourselves honest, we don't just accept the
    definition of ``elementary category with pullbacks'', but in fact we formally establish
    the sense in which it agrees with our standard definition of ``category with pullbacks'',
    which is given in terms of limit cones.
    This is extra work, but it ensures that we didn't make a mistake.
  ›

  context category_with_pullbacks
  begin

    definition some_prj1  ("𝗉1?[_, _]")
    where "𝗉1?[f, g]  if cospan f g then
                         fst (SOME x. cospan_diagram.has_as_pullback C f g (fst x) (snd x))
                       else null"

    definition some_prj0  ("𝗉0?[_, _]")
    where "𝗉0?[f, g]  if cospan f g then
                         snd (SOME x. cospan_diagram.has_as_pullback C f g (fst x) (snd x))
                       else null"

    lemma prj_yields_pullback:
    assumes "cospan f g"
    shows "cospan_diagram.has_as_pullback C f g 𝗉1?[f, g] 𝗉0?[f, g]"
    proof -
      have "x. cospan_diagram.has_as_pullback C f g (fst x) (snd x)"
        using assms has_pullbacks has_pullbacks_def has_as_pullback_def by simp
      thus ?thesis
        using assms has_pullbacks has_pullbacks_def some_prj0_def some_prj1_def
              someI_ex [of "λx. cospan_diagram.has_as_pullback C f g (fst x) (snd x)"]
        by simp
    qed

    interpretation elementary_category_with_pullbacks C some_prj0 some_prj1
    proof
      show "f g. ¬ cospan f g  𝗉0?[f, g] = null"
        using some_prj0_def by auto
      show "f g. ¬ cospan f g  𝗉1?[f, g] = null"
        using some_prj1_def by auto
      show "f g. cospan f g  commutative_square f g 𝗉1?[f, g] 𝗉0?[f, g]"
      proof
        fix f g
        assume fg: "cospan f g"
        show "cospan f g" by fact
        interpret J: cospan_shape .
        interpret D: cospan_diagram C f g
          using fg by (unfold_locales, auto)
        let  = "D.mkCone 𝗉1?[f, g] 𝗉0?[f, g]"
        interpret χ: limit_cone J.comp C D.map dom 𝗉1?[f, g] 
          using fg prj_yields_pullback by auto
        have 1: "𝗉1?[f, g] =  J.AA  𝗉0?[f, g] =  J.BB"
          using D.mkCone_def by simp
        show "span 𝗉1?[f, g] 𝗉0?[f, g]"
        proof -
          have "arr 𝗉1?[f, g]  arr 𝗉0?[f, g]"
            using 1 J.arr_char J.seq_char
            by (metis J.seqE χ.preserves_reflects_arr)
          moreover have "dom 𝗉1?[f, g] = dom 𝗉0?[f, g]"
            using 1 D.is_rendered_commutative_by_cone χ.cone_axioms J.seq_char
            by (metis J.cod_eqI J.seqE χ.A.map_simp χ.preserves_dom J.ide_char)
          ultimately show ?thesis by simp
        qed
        show "dom f = cod 𝗉1?[f, g]"
          using 1 fg χ.preserves_cod [of J.BB] J.cod_char D.mkCone_def
          by (metis D.map.simps(1) D.preserves_cod J.seqE χ.preserves_cod cod_dom J.seq_char)
        show "f  𝗉1?[f, g] = g  𝗉0?[f, g]"
          using 1 fg D.is_rendered_commutative_by_cone χ.cone_axioms by force
      qed
      show "f g h k. commutative_square f g h k  ∃!l. 𝗉1?[f, g]  l = h  𝗉0?[f, g]  l = k"
      proof -
        fix f g h k
        assume fghk: "commutative_square f g h k"
        interpret J: cospan_shape .
        interpret D: cospan_diagram C f g
          using fghk by (unfold_locales, auto)
        let  = "D.mkCone 𝗉1?[f, g] 𝗉0?[f, g]"
        interpret χ: limit_cone J.comp C D.map dom 𝗉1?[f, g] 
          using fghk prj_yields_pullback by auto
        interpret χ: pullback_cone C f g 𝗉1?[f, g] 𝗉0?[f, g] ..
        have 1: "𝗉1?[f, g] =  J.AA  𝗉0?[f, g] =  J.BB"
          using D.mkCone_def by simp
        show "∃!l. 𝗉1?[f, g]  l = h  𝗉0?[f, g]  l = k"
        proof
          let ?l = "SOME l. 𝗉1?[f, g]  l = h  𝗉0?[f, g]  l = k"
          show "𝗉1?[f, g]  ?l = h  𝗉0?[f, g]  ?l = k"
             using fghk χ.is_universal' χ.renders_commutative
                   someI_ex [of "λl. 𝗉1?[f, g]  l = h  𝗉0?[f, g]  l = k"]
             by blast
          thus "l. 𝗉1?[f, g]  l = h  𝗉0?[f, g]  l = k  l = ?l"
            using fghk χ.is_universal' χ.renders_commutative limit_cone_def
            by (metis (no_types, lifting) in_homI seqE commutative_squareE dom_comp seqI)
        qed
      qed
    qed

    proposition extends_to_elementary_category_with_pullbacks:
    shows "elementary_category_with_pullbacks C some_prj0 some_prj1"
      ..

  end

  context elementary_category_with_pullbacks
  begin

    interpretation category_with_pullbacks C
    proof
      show "has_pullbacks"
      proof (unfold has_pullbacks_def)
        have "f g. cospan f g  p0 p1. has_as_pullback f g p0 p1"
        proof -
          fix f g
          assume fg: "cospan f g"
          have "has_as_pullback f g 𝗉1[f, g] 𝗉0[f, g]"
            using fg has_as_pullbackI pullback_commutes universal by presburger
          thus "p0 p1. has_as_pullback f g p0 p1" by blast
        qed
        thus "f g. cospan f g  (p0 p1. has_as_pullback f g p0 p1)"
          by simp
      qed
    qed

    proposition is_category_with_pullbacks:
    shows "category_with_pullbacks C"
      ..

  end

  sublocale elementary_category_with_pullbacks  category_with_pullbacks
    using is_category_with_pullbacks by auto

end