Theory SpanBicategory

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

section "Span Bicategories"

text ‹
  In this section we construct the bicategory Span(C)›, where C› is a category with pullbacks.
  The $0$-cells of Span(C)› are the objects of C›, the $1$-cells of Span(C)› are pairs
  (f0, f1)› of arrows of C› having a common domain, and the $2$-cells of Span(C)›
  are ``arrows of spans''.  An arrow of spans from (f0, f1)› to (g0, g1)› is
  an arrow «u: dom f0 → dom g0»› of C›, such that g0 ⋅ u = f0 and g1 ⋅ u = f1.

  In the present development, a \emph{span} is formalized as a structure ⦇Leg0 = f0, Leg1 = f1⦈›,
  where f0 and f1 are arrows of C› with a common domain, which we call the \emph{apex} of
  the span.
  An \emph{arrow of spans}  is formalized as a structure ⦇Chn = u, Dom = S, Cod = T⦈›,
  where S› and T› are spans, and «u : S.apex → T.apex»› satisfies Leg0 T ⋅ u = Leg0 S›
  and Leg1 T ⋅ u = Leg1 S›.  We refer to the arrow u› as the \emph{chine} of the arrow of spans.

  Arrows of spans inherit a composition from that of C›; this is ``vertical composition''.
  Spans may be composed via pullback in C›; this ``horizontal composition'' extends to
  arrows of spans, so that it is functorial with respect to vertical composition.
  These two compositions determine a bicategory, as we shall show.
›

theory SpanBicategory
imports Bicategory InternalAdjunction Category3.FreeCategory Category3.CategoryWithPullbacks
begin

subsection "Spans"

  record 'a span_data =
    Leg0 :: 'a
    Leg1 :: 'a

  locale span_in_category =
    C: category +
  fixes S :: "'a span_data" (structure)
  assumes is_span: "C.span (Leg0 S) (Leg1 S)"
  begin

    abbreviation leg0
    where "leg0  Leg0 S"

    abbreviation leg1
    where "leg1  Leg1 S"

    abbreviation src
    where "src  C.cod leg0"

    abbreviation trg
    where "trg  C.cod leg1"

    definition apex
    where "apex  C.dom leg0"

    lemma ide_apex [simp]:
    shows "C.ide apex"
      using is_span apex_def by simp

    lemma leg_in_hom [intro]:
    shows "«leg0 : apex  src»"
    and "«leg1 : apex  trg»"
      using is_span apex_def by auto

    lemma leg_simps [simp]:
    shows "C.arr leg0" and "C.dom leg0 = apex"
    and "C.arr leg1" and "C.dom leg1 = apex"
      using leg_in_hom by auto

  end

  record 'a arrow_of_spans_data =
    Chn :: 'a
    Dom :: "'a span_data"
    Cod :: "'a span_data"

  locale arrow_of_spans =
    C: category C +
    dom: span_in_category C Dom μ +
    cod: span_in_category C Cod μ
  for C :: "'a comp"  (infixr "" 55)
  and μ :: "'a arrow_of_spans_data" (structure) +
  assumes chine_in_hom [intro]: "«Chn μ : dom.apex  cod.apex»"
  and leg0_commutes [simp]: "cod.leg0  Chn μ = dom.leg0"
  and leg1_commutes [simp]: "cod.leg1  (Chn μ) = dom.leg1"
  begin

    abbreviation chine
    where "chine  Chn μ"

    lemma chine_simps [simp]:
    shows "C.arr chine" and "C.dom chine = dom.apex" and "C.cod chine = cod.apex"
      using chine_in_hom by auto

    lemma cod_src_eq_dom_src [simp]:
    shows "cod.src = dom.src"
      using dom.is_span cod.is_span
      by (metis C.cod_comp leg0_commutes)

    lemma cod_trg_eq_dom_trg [simp]:
    shows "cod.trg = dom.trg"
      using dom.is_span cod.is_span
      by (metis C.cod_comp leg1_commutes)

    abbreviation dsrc
    where "dsrc  dom.src"

    abbreviation dtrg
    where "dtrg  dom.trg"

  end

  locale identity_arrow_of_spans =
    arrow_of_spans +
  assumes chine_is_identity [simp]: "C.ide (Chn μ)"
  begin

    abbreviation apex
    where "apex  dom.apex"

    abbreviation leg0
    where "leg0  dom.leg0"

    abbreviation leg1
    where "leg1  dom.leg1"

    lemma chine_eq_apex [simp]:
    shows "chine = apex"
      using chine_is_identity C.ideD(2) chine_simps(2) by presburger

    lemma cod_simps [simp]:
    shows "cod.apex = apex" and "cod.leg0 = leg0" and "cod.leg1 = leg1"
      using chine_is_identity chine_simps(3) C.comp_arr_ide leg0_commutes leg1_commutes
      by force+

  end

  subsection "The Vertical Category of Spans"

  text ‹
    The following locale constructs the category of spans and arrows of spans in
    an underlying category C, which is not yet assumed to have pullbacks.
    The composition is vertical composition of arrows of spans, to which we will
    later add horizontal composition to obtain a bicategory.
  ›

  locale span_vertical_category =
    C: category
  begin

    abbreviation Null
    where "Null  Chn = C.null,
                   Dom = Leg0 = C.null, Leg1 = C.null,
                   Cod = Leg0 = C.null, Leg1 = C.null"

    lemma not_arr_Null:
    shows "¬ arrow_of_spans C Null"
      unfolding arrow_of_spans_def arrow_of_spans_axioms_def
      by auto

    text ‹
      Arrows of spans are composed simply by composing their chines.
    ›

    definition vcomp
    where "vcomp ν μ  if arrow_of_spans C μ  arrow_of_spans C ν  Dom ν = Cod μ
                       then Chn = Chn ν  Chn μ, Dom = Dom μ, Cod = Cod ν
                       else Null"

    notation vcomp        (infixr "" 55)

    (*
     * TODO: The reason why the this and the subsequent category interpretation are declared
     * as V: is that subsequently proved facts with the same names as the partial_magma and
     * category locales silently override the latter, resulting in problems proving things.
     * The presence of the extra "V" is only an issue up until a later sublocale declaration
     * inherits everything from horizontal_homs.  I wish I could say that I completely
     * understood the inheritance and overriding rules for locales.
     *)
    interpretation V: partial_composition vcomp
      using not_arr_Null vcomp_def
      apply unfold_locales
      by (metis (no_types, opaque_lifting))

    lemma is_partial_composition:
    shows "partial_magma vcomp"
      ..

    lemma null_char:
    shows "V.null = Null"
      using V.null_def vcomp_def not_arr_Null
      by (metis (no_types, lifting) V.null_is_zero(2))

    text ‹
      Identities are arrows of spans whose chines are identities of C.
    ›

    lemma ide_char:
    shows "V.ide μ  arrow_of_spans C μ  C.ide (Chn μ)"
    proof
      show "V.ide μ  arrow_of_spans C μ  C.ide (Chn μ)"
      proof
        assume 0: "V.ide μ"
        have 1: "vcomp μ μ  Null  (ν. (ν  μ  Null  ν  μ = ν) 
                                          (μ  ν  Null  μ  ν = ν))"
          using 0 V.ide_def null_char by simp
        show μ: "arrow_of_spans C μ"
          using 1 vcomp_def by metis
        interpret μ: arrow_of_spans C μ
          using μ by auto
        show "C.ide (Chn μ)"
        proof -
          have "μ.chine  μ.chine  C.null"
            using 1 vcomp_def
            by (metis C.in_homE C.not_arr_null C.seqI μ.chine_in_hom)
          moreover have "f. f  Chn μ  C.null  f  Chn μ = f"
          proof -
            fix f
            assume "f  μ.chine  C.null"
            hence f: "«f : μ.cod.apex  C.cod f»"
              using C.ext C.in_homI by force
            let ?cod_μ = "Chn = C.cod μ.chine, Dom = Cod μ, Cod = Cod μ"
            interpret cod_μ: arrow_of_spans C ?cod_μ
              using C.ide_in_hom μ.cod.ide_apex μ.chine_in_hom C.comp_arr_dom
              by (unfold_locales, auto)
            have "?cod_μ  μ = ?cod_μ"
              by (metis (no_types, opaque_lifting) "1" C.not_arr_null
                  μ.cod.span_in_category_axioms arrow_of_spans_data.select_convs(2)
                  cod_μ.arrow_of_spans_axioms span_data.select_convs(1)
                  span_in_category.leg_simps(1) vcomp_def)
            thus "f  μ.chine = f"
              using C.comp_arr_ide C.comp_cod_arr μ cod_μ.arrow_of_spans_axioms f vcomp_def
              by auto
          qed
          moreover have "f. μ.chine  f  C.null  μ.chine  f = f"
            by (metis C.comp_cod_arr C.comp_ide_arr C.ext C.ide_char' calculation(1-2))
          ultimately show "C.ide μ.chine"
            unfolding C.ide_def by simp
        qed
      qed
      show "arrow_of_spans C μ  C.ide (Chn μ)  V.ide μ"
      proof -
        assume μ: "arrow_of_spans C μ  C.ide (Chn μ)"
        interpret μ: arrow_of_spans C μ
          using μ by auto
        have 1: "Dom μ = Cod μ"
          using μ identity_arrow_of_spans.cod_simps(2) identity_arrow_of_spans.cod_simps(3)
                identity_arrow_of_spans.intro identity_arrow_of_spans_axioms.intro
          by fastforce
        show "V.ide μ"
        proof -
          have "μ  μ  V.null"
            using μ 1 vcomp_def by (simp add: C.ide_def null_char)
          moreover have "ν. vcomp ν μ  V.null  vcomp ν μ = ν"
          proof -
            fix ν :: "'a arrow_of_spans_data"
            assume ν: "ν  μ  V.null"
            have 2: "arrow_of_spans C ν  Dom ν = Cod μ"
              using ν 1 vcomp_def by (metis V.null_is_zero(2))
            interpret ν: arrow_of_spans C ν
              using 2 by auto
            show "ν  μ = ν"
              unfolding vcomp_def
              using μ 1 2 C.comp_arr_ide by simp
          qed
          moreover have "ν. μ  ν  V.null  μ  ν = ν"
          proof -
            fix ν :: "'a arrow_of_spans_data"
            assume ν: "μ  ν  V.null"
            have 2: "arrow_of_spans C ν  Dom μ = Cod ν"
              using ν 1 vcomp_def by (metis V.null_is_zero(1))
            interpret ν: arrow_of_spans C ν
              using 2 by auto
            show "μ  ν = ν"
              unfolding vcomp_def
              using μ 1 2 C.comp_ide_arr by simp
          qed
          ultimately show ?thesis
            unfolding V.ide_def by blast
        qed
      qed
    qed

    lemma has_domain_char:
    shows "V.domains μ  {}  arrow_of_spans C μ"
    proof
      show "V.domains μ  {}  arrow_of_spans C μ"
        using V.domains_def null_char vcomp_def by fastforce
      show "arrow_of_spans C μ  V.domains μ  {}"
      proof -
        assume μ: "arrow_of_spans C μ"
        interpret μ: arrow_of_spans C μ
          using μ by auto
        let ?dom_μ = "Chn = μ.dom.apex, Dom = Dom μ, Cod = Dom μ"
        interpret dom_μ: arrow_of_spans C ?dom_μ
          using C.comp_arr_dom by (unfold_locales, auto)
        have "?dom_μ  V.domains μ"
        proof -
          have "V.ide ?dom_μ"
            using ide_char dom_μ.arrow_of_spans_axioms by simp
          moreover have "μ  ?dom_μ  V.null"
            using μ vcomp_def μ.cod.span_in_category_axioms dom_μ.arrow_of_spans_axioms
                  null_char span_in_category.leg_simps(1)
            by fastforce
          ultimately show ?thesis
            unfolding V.domains_def by blast
        qed
        thus "V.domains μ  {}" by blast
      qed
    qed

    lemma has_codomain_char:
    shows "V.codomains μ  {}  arrow_of_spans C μ"
    proof
      show "V.codomains μ  {}  arrow_of_spans C μ"
        using V.codomains_def null_char vcomp_def by fastforce
      show "arrow_of_spans C μ  V.codomains μ  {}"
      proof -
        assume μ: "arrow_of_spans C μ"
        interpret μ: arrow_of_spans C μ
          using μ by auto
        let ?cod_f = "Chn = μ.cod.apex, Dom = Cod μ, Cod = Cod μ"
        interpret cod_f: arrow_of_spans C ?cod_f
          using C.comp_arr_dom by (unfold_locales, auto)
        have "?cod_f  V.codomains μ"
        proof -
          have "V.ide ?cod_f"
            using ide_char cod_f.arrow_of_spans_axioms by simp
          moreover have "?cod_f  μ  V.null"
            using μ vcomp_def μ.cod.span_in_category_axioms cod_f.arrow_of_spans_axioms
                  null_char span_in_category.leg_simps(1)
            by fastforce
          ultimately show ?thesis
            unfolding V.codomains_def by blast
        qed
        thus "V.codomains μ  {}" by blast
      qed
    qed

    lemma arr_char:
    shows "V.arr μ  arrow_of_spans C μ"
      unfolding V.arr_def
      using has_domain_char has_codomain_char by simp

    lemma seq_char:
    shows "V.seq ν μ  arrow_of_spans C μ  arrow_of_spans C ν  Dom ν = Cod μ"
    proof
      show "V.seq ν μ  arrow_of_spans C μ  arrow_of_spans C ν  Dom ν = Cod μ"
        using vcomp_def by (metis V.not_arr_null null_char)
      show "arrow_of_spans C μ  arrow_of_spans C ν  Dom ν = Cod μ  V.seq ν μ"
      proof -
        assume 1: "arrow_of_spans C μ  arrow_of_spans C ν  Dom ν = Cod μ"
        interpret μ: arrow_of_spans C μ
          using 1 by auto
        interpret ν: arrow_of_spans C ν
          using 1 by auto
        show "V.seq ν μ"
        proof -
          let ?νμ = "Chn = Chn ν  Chn μ, Dom = Dom μ, Cod = Cod ν"
          have "ν  μ = ?νμ"
            using 1 vcomp_def by metis
          moreover have "V.arr ?νμ"
          proof -
            interpret Dom: span_in_category C Dom ?νμ
              by (simp add: μ.dom.span_in_category_axioms)
            interpret Cod: span_in_category C Cod ?νμ
              by (simp add: ν.cod.span_in_category_axioms)
            have "arrow_of_spans C ?νμ"
              using 1 μ.chine_in_hom ν.chine_in_hom C.comp_reduce
              by (unfold_locales, cases ?νμ, auto)
            thus ?thesis
              using arr_char by blast
          qed
          ultimately show ?thesis by simp
        qed
      qed
    qed

    interpretation V: category vcomp
    proof
      show "μ. (V.domains μ  {}) = (V.codomains μ  {})"
        using has_domain_char has_codomain_char by simp
      show "ν μ. ν  μ  V.null  V.seq ν μ"
        using seq_char vcomp_def null_char by metis
      show "π ν μ. V.seq π ν  V.seq (π  ν) μ  V.seq ν μ"
        using seq_char vcomp_def by (metis arrow_of_spans_data.select_convs(2))
      show "π ν μ. V.seq π (ν  μ)  V.seq ν μ  V.seq π ν"
        using seq_char vcomp_def by (metis arrow_of_spans_data.select_convs(3))
      show "ν μ π. V.seq ν μ  V.seq π ν  V.seq (π  ν) μ"
        using seq_char vcomp_def by (metis arr_char arrow_of_spans_data.select_convs(2))
      show "ν μ π. V.seq ν μ  V.seq π ν  (π  ν)  μ = π  ν  μ"
      proof -
        fix μ ν π
        assume μν: "V.seq ν μ" and νπ: "V.seq π ν"
        interpret μ: arrow_of_spans C μ
          using μν seq_char by auto
        interpret ν: arrow_of_spans C ν
          using μν seq_char by auto
        interpret π: arrow_of_spans C π
          using νπ seq_char by auto
        show "(π  ν)  μ = π  ν  μ"
          unfolding vcomp_def
          using μν νπ seq_char μ.chine_in_hom ν.chine_in_hom π.chine_in_hom
          by (simp add: C.comp_assoc, metis arr_char vcomp_def)
      qed
    qed

    lemma is_category:
    shows "category vcomp"
      ..

    lemma dom_char:
    shows "V.dom = (λμ. if V.arr μ then
                          Chn = span_in_category.apex C (Dom μ), Dom = Dom μ, Cod = Dom μ
                        else V.null)"
    proof
      fix μ
      have "¬ V.arr μ  V.dom μ = V.null"
        by (simp add: V.arr_def V.dom_def)
      moreover have "V.arr μ  V.dom μ = Chn = span_in_category.apex C (Dom μ),
                                            Dom = Dom μ, Cod = Dom μ"
        by (metis V.comp_arr_dom V.comp_ide_self V.ideD(1) V.ide_dom arrow_of_spans_data.cases
            arrow_of_spans_data.select_convs(1-3) ide_char identity_arrow_of_spans.chine_eq_apex
            identity_arrow_of_spans_axioms.intro identity_arrow_of_spans_def seq_char)
      ultimately show "V.dom μ = (if V.arr μ then
                                     Chn = span_in_category.apex C (Dom μ),
                                      Dom = Dom μ, Cod = Dom μ
                                  else V.null)"
        by argo
    qed

    lemma cod_char:
    shows "V.cod = (λμ. if V.arr μ then
                          Chn = span_in_category.apex C (Cod μ), Dom = Cod μ, Cod = Cod μ
                        else V.null)"
    proof
      fix μ
      have "¬ V.arr μ  V.cod μ = V.null"
        by (simp add: V.arr_def V.cod_def)
      moreover have "V.arr μ  V.cod μ = Chn = span_in_category.apex C (Cod μ),
                                            Dom = Cod μ, Cod = Cod μ"
        by (metis V.arr_cod V.comp_cod_arr V.dom_cod dom_char span_vertical_category.seq_char
                  span_vertical_category_axioms)
      ultimately show "V.cod μ = (if V.arr μ then
                                    Chn = span_in_category.apex C (Cod μ),
                                     Dom = Cod μ, Cod = Cod μ
                                  else V.null)"
        by argo
    qed

    lemma vcomp_char:
    shows "vcomp = (λν μ. if V.seq ν μ then
                             Chn = Chn ν  Chn μ, Dom = Dom μ, Cod = Cod ν
                           else V.null)"
      by (meson V.ext seq_char vcomp_def)

    lemma vcomp_eq:
    assumes "V.seq ν μ"
    shows "ν  μ = Chn = Chn ν  Chn μ, Dom = Dom μ, Cod = Cod ν"
      using assms vcomp_char by meson

    lemma Chn_vcomp:
    assumes "V.seq ν μ"
    shows "Chn (ν  μ) = Chn ν  Chn μ"
      using assms vcomp_eq [of ν μ] by simp

    lemma ide_char':
    shows "V.ide μ  identity_arrow_of_spans C μ"
      using arr_char ide_char identity_arrow_of_spans_axioms_def identity_arrow_of_spans_def
            identity_arrow_of_spans.axioms(1) identity_arrow_of_spans.chine_is_identity
      by metis

    lemma Chn_in_hom:
    assumes "V.in_hom τ f g"
    shows "C.in_hom (Chn τ) (Chn f) (Chn g)"
      by (metis arr_char arrow_of_spans.chine_in_hom arrow_of_spans_data.select_convs(1)
                assms category.in_homE is_category span_vertical_category.cod_char
                span_vertical_category.dom_char span_vertical_category_axioms)

    abbreviation mkIde
    where "mkIde f0 f1 
           Chn = C.dom f0, Dom = Leg0 = f0, Leg1 = f1, Cod = Leg0 = f0, Leg1 = f1"

    lemma ide_mkIde:
    assumes "C.span f0 f1"
    shows "V.ide (mkIde f0 f1)"
    proof -
      interpret f: span_in_category C Leg0 = f0, Leg1 = f1
        using assms by (unfold_locales, auto)
      interpret ff: arrow_of_spans C mkIde f0 f1
        using assms f.apex_def C.comp_arr_dom
        by (unfold_locales, auto)
      show ?thesis
        using assms ff.arrow_of_spans_axioms ide_char by simp
    qed

    abbreviation mkObj
    where "mkObj a  mkIde a a"

    lemma ide_mkObj:
    assumes "C.ide a"
    shows "V.ide (mkObj a)"
      using assms ide_mkIde [of a a] by auto

    lemma inverse_arrows:
    assumes "V.arr μ" and "C.iso (Chn μ)"
    shows "V.inverse_arrows μ Chn = C.inv (Chn μ), Dom = Cod μ, Cod = Dom μ"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      let  = "Chn = C.inv (Chn μ), Dom = Cod μ, Cod = Dom μ"
      interpret ν: arrow_of_spans C 
        using assms C.invert_side_of_triangle(2) [of μ.dom.leg0 μ.cod.leg0 μ.chine]
              C.invert_side_of_triangle(2) [of μ.dom.leg1 μ.cod.leg1 μ.chine]
        by (unfold_locales, auto)
      show "V.inverse_arrows μ "
      proof
        show "V.ide (  μ)"
          by (metis C.invert_side_of_triangle(1) Chn_vcomp μ.arrow_of_spans_axioms
                    μ.chine_simps(1) μ.chine_simps(2) μ.dom.ide_apex ν.arrow_of_spans_axioms
                    arr_char select_convs(1-2) assms(2) C.comp_arr_dom ide_char seq_char)
        thus "V.ide (μ  )"
          by (metis C.comp_inv_arr' C.inv_inv C.iso_inv_iso V.ide_compE μ.cod.ide_apex
                    ν.chine_simps(2) arr_char select_convs(1-2) assms(2) ide_char
                    Chn_vcomp)
      qed
    qed

    lemma iso_char:
    shows "V.iso μ  V.arr μ  C.iso (Chn μ)"
    proof
      show "V.iso μ  V.arr μ  C.iso (Chn μ)"
        using vcomp_eq ide_char
        by (metis C.iso_iff_section_and_retraction C.retractionI C.sectionI Chn_vcomp
            V.arr_cod V.arr_dom V.comp_arr_inv' V.comp_inv_arr' V.ide_cod V.ide_dom
            V.iso_is_arr)
      show "V.arr μ  C.iso (Chn μ)  V.iso μ"
        using inverse_arrows by auto
    qed

    lemma inv_eq:
    assumes "V.iso μ"
    shows "V.inv μ = Chn = C.inv (Chn μ), Dom = Cod μ, Cod = Dom μ"
      using assms inverse_arrows iso_char by (simp add: V.inverse_unique)

  end

  subsection "Putting Spans in Homs"

  context span_vertical_category
  begin

    interpretation V: category vcomp
      using is_category by simp

    definition src
    where "src μ  if V.arr μ then mkObj (C.cod (Leg0 (Dom μ))) else V.null"

    lemma ide_src [simp]:
    assumes "V.arr μ"
    shows "V.ide (src μ)"
      using assms src_def arr_char ide_mkObj C.ide_cod
      by (simp add: arrow_of_spans_def span_in_category.leg_simps(1))

    interpretation src: endofunctor vcomp src
    proof
      show "μ. ¬ V.arr μ  src μ = V.null"
        using arr_char by (simp add: src_def null_char)
      show 1: "μ. V.arr μ  V.arr (src μ)"
        using ide_src by simp
      show 2: "μ. V.arr μ  V.dom (src μ) = src (V.dom μ)"
        using 1 arr_char src_def dom_char ide_src V.arr_dom V.ideD(2) by force      
      show 3: "μ. V.arr μ  V.cod (src μ) = src (V.cod μ)"
        using 1 arr_char src_def cod_char ide_src V.arr_cod V.ideD(3)
              arrow_of_spans.cod_src_eq_dom_src
        by force
      show "μ ν. V.seq ν μ  src (ν  μ) = src ν  src μ"
        by (metis (no_types, lifting) "1" "2" "3" V.comp_ide_self V.dom_comp V.ideD(2)
            V.seqE span_vertical_category.ide_src span_vertical_category_axioms)
    qed

    lemma src_is_endofunctor:
    shows "endofunctor vcomp src"
      ..

    lemma src_vcomp:
    assumes "V.seq ν μ"
    shows "src (ν  μ) = src ν  src μ"
      using assms src.preserves_comp by simp

    definition trg
    where "trg μ  if V.arr μ then mkObj (C.cod (Leg1 (Dom μ))) else V.null"

    lemma ide_trg [simp]:
    assumes "V.arr μ"
    shows "V.ide (trg μ)"
      using assms trg_def arr_char ide_mkObj C.ide_cod
      by (simp add: arrow_of_spans_def span_in_category.leg_simps(3))

    interpretation trg: endofunctor vcomp trg
    proof
      show "μ. ¬ V.arr μ  trg μ = V.null"
        using arr_char by (simp add: trg_def null_char)
      show 1: "μ. V.arr μ  V.arr (trg μ)"
        using ide_trg by simp
      show 2: "μ. V.arr μ  V.dom (trg μ) = trg (V.dom μ)"
        using 1 arr_char trg_def dom_char ide_trg V.arr_dom V.ideD(2) by force      
      show 3: "μ. V.arr μ  V.cod (trg μ) = trg (V.cod μ)"
        using 1 arr_char trg_def cod_char ide_trg V.arr_cod V.ideD(3)
              arrow_of_spans.cod_trg_eq_dom_trg
        by force
      show "μ ν. V.seq ν μ  trg (ν  μ) = trg ν  trg μ"
        by (metis "2" "3" V.comp_ide_self V.dom_comp V.ide_char V.seqE ide_trg)
    qed

    lemma trg_is_endofunctor:
    shows "endofunctor vcomp trg"
      ..

    lemma trg_vcomp:
    assumes "V.seq ν μ"
    shows "trg (ν  μ) = trg ν  trg μ"
      using assms trg.preserves_comp by simp

    lemma src_trg_simps [simp]:
    assumes "V.arr μ"
    shows "src (src μ) = src μ"
    and "src (trg μ) = trg μ"
    and "trg (src μ) = src μ"
    and "trg (trg μ) = trg μ"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      have 1: "V.arr Chn = μ.dsrc, Dom = Leg0 = μ.dsrc, Leg1 = μ.dsrc,
                      Cod = Leg0 = μ.dsrc, Leg1 = μ.dsrc"
        using ide_mkObj by auto
      have 2: "V.arr Chn = μ.dtrg, Dom = Leg0 = μ.dtrg, Leg1 = μ.dtrg,
                      Cod = Leg0 = μ.dtrg, Leg1 = μ.dtrg"
        using ide_mkObj by auto
      show "src (src μ) = src μ"
        using assms 1 src_def by simp
      show "trg (src μ) = src μ"
        using assms 1 src_def trg_def by simp
      show "src (trg μ) = trg μ"
        using assms 2 src_def trg_def by simp
      show "trg (trg μ) = trg μ"
        using assms 2 trg_def by simp
    qed

    sublocale horizontal_homs vcomp src trg
      by (unfold_locales, simp_all)

    lemma has_horizontal_homs:
    shows "horizontal_homs vcomp src trg"
      ..

    lemma obj_char:
    shows "obj a  V.ide a  a = mkObj (Chn a)"
      by (metis C.dom_cod V.comp_ide_self V.ide_char arrow_of_spans.chine_simps(3)
          arrow_of_spans_data.select_convs(1,3) objE objI_trg span_data.select_convs(2)
          cod_char seq_char trg_def)

  end

  subsection "Horizontal Composite of Spans"

  text ‹
    We now define the horizontal composite S ⋆ T› of spans S› and T›,
    assuming that C› is a category with chosen pullbacks.
    We think of Leg0 as an input and Leg1 as an output.
    The following then defines the composite span S ⋆ T›, with T› on the ``input side'' of S›.
    The notation is such that the 𝗉0 projections of C› are used for legs on the input
    (\emph{i.e.} the ``0'') side and the 𝗉1 projections are used for legs on the output
    (\emph{i.e.} the ``1'') side.
  ›

  locale composite_span =
    C: elementary_category_with_pullbacks +
    S: span_in_category C S +
    T: span_in_category C T
  for S (structure)
  and T (structure) +
  assumes composable: "C.cod (Leg0 S) = C.cod (Leg1 T)"
  begin

    abbreviation this
    where "this  Leg0 = T.leg0  𝗉0[S.leg0, T.leg1], Leg1 = S.leg1  𝗉1[S.leg0, T.leg1]"

    lemma leg0_prj_in_hom:
    shows "«T.leg0  𝗉0[S.leg0, T.leg1] : S.leg0 ↓↓ T.leg1  C.cod (Leg0 T)»"
      using S.is_span T.is_span C.prj0_in_hom [of "Leg0 S" "Leg1 T"] composable by auto

    lemma leg1_prj_in_hom:
    shows "«S.leg1  𝗉1[S.leg0, T.leg1] : S.leg0 ↓↓ T.leg1  C.cod (Leg1 S)»"
      using S.is_span T.is_span C.prj1_in_hom [of "Leg0 S" "Leg1 T"] composable by auto

    lemma is_span [simp]:
    shows "span_in_category C this"
      using leg0_prj_in_hom leg1_prj_in_hom
      by (unfold_locales, fastforce)

    sublocale span_in_category C this
      using is_span by auto

  end

  locale span_bicategory =
  C: elementary_category_with_pullbacks +
     span_vertical_category
  begin

    definition chine_hcomp
    where "chine_hcomp ν μ 
           Chn ν  𝗉1[Leg0 (Dom ν), Leg1 (Dom μ)]
             Leg0 (Cod ν), Leg1 (Cod μ)
            Chn μ  𝗉0[Leg0 (Dom ν), Leg1 (Dom μ)]"

    text ‹
$$\xymatrix{
  & & \scriptstyle{{\rm src}({\rm Dom}~\nu)} \;=\; {{\rm trg}({\rm Dom}~\mu)} & &\\
  &
    \ar[ddl] _{{\rm Leg1}({\rm Dom}~\nu)}
    \ar [ur] ^<>(0.4){{\rm Leg0}({\rm Dom}~\nu)\hspace{20pt}}
    \ar[dddd] ^{{\rm Chn}~\nu}
  &
  &
    \ar[ul] _<>(0.4){\hspace{20pt}{\rm Leg1}({\rm Dom}~\mu)}
    \ar[ddr] ^{{\rm Leg0}({\rm Dom}~\mu)}
    \ar[dddd] _{{\rm Chn}~\mu}
  \\
  & &
    \ar[ul] ^{p_1}
    \ar[ur] _{p_0}
    \ar@ {.>}[dd]^<>(0.3){{\rm chn\_hcomp~\mu~\nu}}
  \\
  \scriptstyle{{\rm trg}~\nu} & & & & \scriptstyle{{\rm src}~\mu} \\
  & &
    \ar[dl] _{p_1}
    \ar[dr] ^{p_0}
  & &
  \\
  &
    \ar[uul] ^{{\rm Leg1}({\rm Cod}~\nu)}
    \ar[dr] _<>(0.4){{\rm Leg1}({\rm Cod}~\nu)\hspace{20pt}}
  & &
    \ar[dl] ^<>(0.4){\hspace{20pt}{\rm Leg1}({\rm Cod}~\mu)}
    \ar[uur] _{{\rm Leg0}({\rm Cod}~\mu)}
  \\
  & & \scriptstyle{{\rm src}({\rm Cod}~\nu)} \;=\; {{\rm trg}({\rm Cod}~\mu)} & &
}$$
    ›

    definition hcomp
    where "hcomp ν μ  if arr μ  arr ν  src ν = trg μ then
                          Chn = chine_hcomp ν μ,
                           Dom = composite_span.this C prj0 prj1 (Dom ν) (Dom μ),
                           Cod = composite_span.this C prj0 prj1 (Cod ν) (Cod μ)
                       else
                          null"

    notation hcomp        (infixr "" 53)

    lemma chine_hcomp_props:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "«chine_hcomp ν μ : Leg0 (Dom ν) ↓↓ Leg1 (Dom μ) C Leg0 (Cod ν) ↓↓ Leg1 (Cod μ)»"
    and "C.commutative_square (Leg0 (Cod ν)) (Leg1 (Cod μ))
            (Chn ν  𝗉1[Leg0 (Dom ν), Leg1 (Dom μ)])
            (Chn μ  𝗉0[Leg0 (Dom ν), Leg1 (Dom μ)])"
    and "C.commutative_square 𝗉1[Leg0 (Cod ν), Leg1 (Cod μ)] (Chn ν)
            (chine_hcomp ν μ) 𝗉1[Leg0 (Dom ν), Leg1 (Dom μ)]"
    and "C.commutative_square 𝗉0[Leg0 (Cod ν), Leg1 (Cod μ)] (Chn μ)
            (chine_hcomp ν μ) 𝗉0[Leg0 (Dom ν), Leg1 (Dom μ)]"
    and "𝗉0[Leg0 (Cod ν), Leg1 (Cod μ)]  chine_hcomp ν μ =
         Chn μ  𝗉0[Leg0 (Dom ν), Leg1 (Dom μ)]"
    and "𝗉1[Leg0 (Cod ν), Leg1 (Cod μ)]  chine_hcomp ν μ =
         Chn ν  𝗉1[Leg0 (Dom ν), Leg1 (Dom μ)]"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      show 0: "C.commutative_square ν.cod.leg0 μ.cod.leg1
                 (ν.chine  𝗉1[ν.dom.leg0, μ.dom.leg1]) (μ.chine  𝗉0[ν.dom.leg0, μ.dom.leg1])"
        using assms src_def trg_def C.pullback_commutes C.comp_reduce C.commutative_square_def
        by auto
      show 1: "𝗉1[ν.cod.leg0, μ.cod.leg1]  chine_hcomp ν μ = ν.chine  𝗉1[ν.dom.leg0, μ.dom.leg1]"
        unfolding chine_hcomp_def
        using 0 by simp
      show 2: "𝗉0[ν.cod.leg0, μ.cod.leg1]  chine_hcomp ν μ = μ.chine  𝗉0[ν.dom.leg0, μ.dom.leg1]"
        unfolding chine_hcomp_def
        using 0 by simp
      show 3: "«chine_hcomp ν μ : ν.dom.leg0 ↓↓ μ.dom.leg1 C ν.cod.leg0 ↓↓ μ.cod.leg1»"
        unfolding chine_hcomp_def
        using assms 0 src_def trg_def C.tuple_in_hom by auto
      show "C.commutative_square 𝗉1[ν.cod.leg0, μ.cod.leg1] ν.chine
               (chine_hcomp ν μ) 𝗉1[ν.dom.leg0, μ.dom.leg1]"
        using assms src_def trg_def 1 3 by auto
      show "C.commutative_square 𝗉0[ν.cod.leg0, μ.cod.leg1] μ.chine
               (chine_hcomp ν μ) 𝗉0[ν.dom.leg0, μ.dom.leg1]"
        using assms src_def trg_def 2 3 by auto
    qed

    lemma chine_hcomp_in_hom [intro]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "«chine_hcomp ν μ : Leg0 (Dom ν) ↓↓ Leg1 (Dom μ) C Leg0 (Cod ν) ↓↓ Leg1 (Cod μ)»"
      using assms chine_hcomp_props(1) by simp

    lemma arrow_of_spans_hcomp:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "arrow_of_spans C (ν  μ)"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      show ?thesis
      proof
        show span_Dom: "C.span (Leg0 (Dom (ν  μ))) (Leg1 (Dom (ν  μ)))"
          using assms src_def trg_def hcomp_def C.seqI' by auto
        interpret Dom: span_in_category C Dom (ν  μ)
          using span_Dom by (unfold_locales, auto)
        show span_Cod: "C.span (Leg0 (Cod (ν  μ))) (Leg1 (Cod (ν  μ)))"
          using assms hcomp_def src_def trg_def by auto
        interpret Cod: span_in_category C Cod (ν  μ)
          using span_Cod by (unfold_locales, auto)
        show map: "«Chn (ν  μ) : Dom.apex C Cod.apex»"
          using assms src_def trg_def chine_hcomp_props hcomp_def Cod.apex_def Dom.apex_def
          by auto
        show "Cod.leg0  Chn (ν  μ) = Dom.leg0"
          by (metis C.comp_assoc μ.leg0_commutes arrow_of_spans_data.select_convs(1-3)
              assms(1-3) chine_hcomp_props(5) hcomp_def span_data.select_convs(1))
        show "Cod.leg1  Chn (ν  μ) = Dom.leg1"
        proof -
          have "(ν.cod.leg1  𝗉1[ν.cod.leg0, μ.cod.leg1])  chine_hcomp ν μ =
                 ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1]"
            by (metis C.comp_assoc ν.leg1_commutes assms(1-3) chine_hcomp_props(6))
          thus ?thesis
            using assms src_def trg_def hcomp_def chine_hcomp_props ν.chine_in_hom C.comp_reduce
            by auto
        qed
      qed
    qed

    lemma chine_hcomp_ide_arr:
    assumes "ide f" and "arr μ" and "src f = trg μ"
    shows "chine_hcomp f μ =
           𝗉1[Leg0 (Dom f), Leg1 (Dom μ)]
              Leg0 (Cod f), Leg1 (Cod μ)
            Chn μ  𝗉0[Leg0 (Dom f), Leg1 (Dom μ)]"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret f: arrow_of_spans C f
        using assms ide_char by auto
      have 1: "C.cospan f.dom.leg0 μ.dom.leg1"
        using assms src_def trg_def by auto
      have "chine_hcomp f μ = f.chine  𝗉1[f.dom.leg0, μ.dom.leg1]
                                 f.cod.leg0, μ.cod.leg1
                               μ.chine  𝗉0[f.dom.leg0, μ.dom.leg1]"
        unfolding chine_hcomp_def
        using assms ide_char by simp
      moreover have "f.chine  𝗉1[f.dom.leg0, μ.dom.leg1] = 𝗉1[f.dom.leg0, μ.dom.leg1]"
        using assms 1 C.comp_ide_arr ide_char by auto
      ultimately show ?thesis by argo
    qed

    lemma chine_hcomp_arr_ide:
    assumes "arr μ" and "ide f" and "src μ = trg f"
    shows "chine_hcomp μ f =
           Chn μ  𝗉1[Leg0 (Dom μ), Leg1 (Dom f)]
              Leg0 (Cod μ), Leg1 (Cod f)
            𝗉0[Leg0 (Dom μ), Leg1 (Dom f)]"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret f: arrow_of_spans C f
        using assms ide_char by auto
      have 1: "C.cospan μ.dom.leg0 f.dom.leg1"
        using assms src_def trg_def by auto
      have "chine_hcomp μ f = μ.chine  𝗉1[μ.dom.leg0, f.dom.leg1]
                                 μ.cod.leg0, f.cod.leg1
                               f.chine  𝗉0[μ.dom.leg0, f.dom.leg1]"
        unfolding chine_hcomp_def
        using assms ide_char by simp
      moreover have "f.chine  𝗉0[μ.dom.leg0, f.dom.leg1] = 𝗉0[μ.dom.leg0, f.dom.leg1]"
        using assms 1 C.comp_ide_arr ide_char by auto
      ultimately show ?thesis by argo
    qed

    lemma chine_hcomp_ide_ide:
    assumes "ide g" and "ide f" and "src g = trg f"
    shows "chine_hcomp g f = Leg0 (Dom g) ↓↓ Leg1 (Dom f)"
    proof -
      interpret g: identity_arrow_of_spans C g
        using assms ide_char' by auto
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      have 1: "C.cospan g.dom.leg0 f.dom.leg1"
        using assms src_def trg_def by auto
       have "chine_hcomp g f = g.chine  𝗉1[g.dom.leg0, f.dom.leg1]
                               g.cod.leg0, f.cod.leg1
                              𝗉0[g.dom.leg0, f.dom.leg1]"
        using assms chine_hcomp_arr_ide by simp
      moreover have "g.chine  𝗉1[g.dom.leg0, f.dom.leg1] = 𝗉1[g.dom.leg0, f.dom.leg1]"
        using assms 1 C.comp_ide_arr ide_char by auto
      ultimately have "chine_hcomp g f = 𝗉1[g.dom.leg0, f.dom.leg1]
                                          g.cod.leg0, f.cod.leg1
                                        𝗉0[g.dom.leg0, f.dom.leg1]"
        by simp
      also have "... =
                 𝗉1[g.dom.leg0, f.dom.leg1]  (g.dom.leg0 ↓↓ f.dom.leg1)
                    g.cod.leg0, f.cod.leg1
                  𝗉0[g.dom.leg0, f.dom.leg1]  (g.dom.leg0 ↓↓ f.dom.leg1)"
        using assms 1 C.comp_arr_dom by simp
      also have "... = g.dom.leg0 ↓↓ f.dom.leg1"
        using 1 C.pullback_commutes C.tuple_prj by simp
      finally show ?thesis by simp
    qed

    lemma chine_hcomp_trg_arr:
    assumes "arr μ"
    shows "chine_hcomp (trg μ) μ =
           𝗉1[C.cod (Leg1 (Dom μ)), Leg1 (Dom μ)]
              C.cod (Leg1 (Dom μ)), Leg1 (Cod μ)
            Chn μ  𝗉0[C.cod (Leg1 (Dom μ)), Leg1 (Dom μ)]"
      using assms chine_hcomp_ide_arr ide_trg src_trg trg_def by force

    lemma chine_hcomp_trg_ide:
    assumes "ide f"
    shows "chine_hcomp (trg f) f = C.cod (Leg1 (Dom f)) ↓↓ Leg1 (Dom f)"
      using assms chine_hcomp_ide_ide ide_trg src_trg trg_def by force

    lemma chine_hcomp_arr_src:
    assumes "arr μ"
    shows "chine_hcomp μ (src μ) =
           Chn μ  𝗉1[Leg0 (Dom μ), C.cod (Leg0 (Dom μ))]
              Leg0 (Cod μ), C.cod (Leg0 (Dom μ))
            𝗉0[Leg0 (Dom μ), C.cod (Leg0 (Dom μ))]"
      using assms chine_hcomp_arr_ide ide_src src_def trg_src by force

    lemma chine_hcomp_ide_src:
    assumes "ide f"
    shows "chine_hcomp f (src f) = Leg0 (Dom f) ↓↓ C.cod (Leg0 (Dom f))"
      using assms chine_hcomp_ide_ide src.preserves_ide src_def trg_src by force

    lemma src_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "src (ν  μ) = src μ"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      have "C.cod (μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1]) = C.cod μ.dom.leg0"
        using assms C.commutative_squareE chine_hcomp_props(2)
        by (metis (mono_tags, lifting) C.cod_comp C.match_3 μ.leg0_commutes μ.dom.is_span)
      thus ?thesis
        using assms arr_char hcomp_def src_def C.comp_cod_arr C.comp_arr_dom arrow_of_spans_hcomp
        by simp
    qed

    lemma trg_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "trg (ν  μ) = trg ν"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      have "C.cod (ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1]) = ν.dtrg"
        using assms C.commutative_squareE chine_hcomp_props(2)
        by (metis (mono_tags, lifting) C.cod_comp C.match_3 ν.leg1_commutes ν.dom.is_span)
      thus ?thesis
        using assms arr_char hcomp_def trg_def C.comp_cod_arr C.comp_arr_dom arrow_of_spans_hcomp
        by simp
    qed

    lemma dom_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "dom (ν  μ) = dom ν  dom μ"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      interpret νμ: arrow_of_spans C hcomp ν μ
        using assms arr_char arrow_of_spans_hcomp by simp
      have 1: "C.cospan μ.dom.leg1 ν.dom.leg0"
        using assms μ.dom.is_span ν.dom.is_span src_def trg_def by auto
      have "dom (ν  μ) = 
            Chn = ν.dom.leg0 ↓↓ μ.dom.leg1,
             Dom = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                    Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1],
             Cod = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                    Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1]"
        using assms νμ.arrow_of_spans_axioms νμ.dom.leg_simps(2) νμ.dom.is_span
              arr_char dom_char hcomp_def
        by auto
      also have "... =
                 Chn = chine_hcomp (dom ν) (dom μ),
                  Dom = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                         Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1],
                  Cod = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                         Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1]"
        using assms src_dom trg_dom ide_dom dom_char chine_hcomp_ide_ide
        apply auto
        by (metis (no_types, lifting) arrow_of_spans_data.select_convs(2))
      also have "... = dom ν  dom μ"
        using assms src_dom trg_dom arr_dom dom_char hcomp_def
        apply auto
        by (metis (no_types, lifting))
      finally show ?thesis by blast
    qed

    lemma cod_hcomp [simp]:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    shows "cod (ν  μ) = cod ν  cod μ"
    proof -
      interpret μ: arrow_of_spans C μ
        using assms arr_char by auto
      interpret ν: arrow_of_spans C ν
        using assms arr_char by auto
      interpret νμ: arrow_of_spans C hcomp ν μ
        using assms arr_char arrow_of_spans_hcomp by simp
      have 1: "C.cospan μ.cod.leg1 ν.cod.leg0"
        using assms μ.cod.is_span ν.cod.is_span src_def trg_def by simp
      have 2: "cod (ν  μ) =
               Chn = ν.cod.leg0 ↓↓ μ.cod.leg1,
                Dom = Leg0 = μ.cod.leg0  𝗉0[ν.cod.leg0, μ.cod.leg1],
                       Leg1 = ν.cod.leg1  𝗉1[ν.cod.leg0, μ.cod.leg1],
                Cod = Leg0 = μ.cod.leg0  𝗉0[ν.cod.leg0, μ.cod.leg1],
                       Leg1 = ν.cod.leg1  𝗉1[ν.cod.leg0, μ.cod.leg1]"
        using assms νμ.arrow_of_spans_axioms νμ.cod.leg_simps(2) νμ.cod.is_span
              arr_char cod_char hcomp_def
        by auto
      also have "... =
               Chn = chine_hcomp (cod ν) (cod μ),
                Dom = Leg0 = μ.cod.leg0  𝗉0[ν.cod.leg0, μ.cod.leg1],
                       Leg1 = ν.cod.leg1  𝗉1[ν.cod.leg0, μ.cod.leg1],
                Cod = Leg0 = μ.cod.leg0  𝗉0[ν.cod.leg0, μ.cod.leg1],
                       Leg1 = ν.cod.leg1  𝗉1[ν.cod.leg0, μ.cod.leg1]"
        using assms src_cod trg_cod ide_cod cod_char chine_hcomp_ide_ide
        apply auto
        by (metis (no_types, lifting) arrow_of_spans_data.select_convs(2))
      also have "... = cod ν  cod μ"
        using assms src_cod trg_cod arr_cod cod_char hcomp_def
        apply auto
        by (metis (no_types, lifting))
      finally show ?thesis by simp
    qed

    lemma hcomp_vcomp:
    assumes "arr μ" and "arr ν" and "src ν = trg μ"
    and "arr μ'" and "arr ν'" and "src ν' = trg μ'"
    and "seq μ' μ" and "seq ν' ν"
    shows "(ν'  ν)  (μ'  μ) = (ν'  μ')  (ν  μ)"
    proof -
      interpret μ: arrow_of_spans C μ using assms arr_char by auto
      interpret ν: arrow_of_spans C ν using assms arr_char by auto
      interpret μ': arrow_of_spans C μ' using assms arr_char by auto
      interpret ν': arrow_of_spans C ν' using assms arr_char by auto
      interpret νμ: arrow_of_spans C hcomp ν μ
        using assms arr_char arrow_of_spans_hcomp by auto
      interpret ν'μ': arrow_of_spans C hcomp ν' μ'
        using assms arr_char arrow_of_spans_hcomp by auto

      have 1: "Dom ν' = Cod ν  Dom μ' = Cod μ"
          using assms src_def trg_def seq_char by blast
      have 2: "Dom (μ'  μ) = Dom μ  Dom (ν'  ν) = Dom ν 
               Cod (μ'  μ) = Cod μ'  Cod (ν'  ν) = Cod ν'"
        using assms seq_char arr_char vcomp_def
        by (metis arrow_of_spans_data.select_convs(2) arrow_of_spans_data.select_convs(3))
      have 3: "chine_hcomp (ν'  ν) (μ'  μ) =
               Chn (ν'  ν)  𝗉1[ν.dom.leg0, μ.dom.leg1]
                  ν'.cod.leg0, μ'.cod.leg1
                Chn (μ'  μ)  𝗉0[ν.dom.leg0, μ.dom.leg1]"
        unfolding chine_hcomp_def using 2 by simp

      have C1: "C.commutative_square ν'.cod.leg0 μ'.cod.leg1
                 (Chn ν'  𝗉1[ν'.dom.leg0, μ'.dom.leg1])
                 (Chn μ'  𝗉0[ν'.dom.leg0, μ'.dom.leg1])"
         using assms 1 vcomp_def seq_char arr_char chine_hcomp_props(2) by blast
      have C2: "C.commutative_square ν'.cod.leg0 μ'.cod.leg1
                 (Chn (ν'  ν)  𝗉1[ν.dom.leg0, μ.dom.leg1])
                 (Chn (μ'  μ)  𝗉0[ν.dom.leg0, μ.dom.leg1])"
        by (metis "2" assms(3,6-8) chine_hcomp_props(2) src.as_nat_trans.preserves_comp_2
                  trg.as_nat_trans.preserves_comp_2 vseq_implies_hpar(2))
      have "(ν'  ν)  (μ'  μ) =
            Chn = chine_hcomp (ν'  ν) (μ'  μ),
             Dom = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                    Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1],
             Cod = Leg0 = μ'.cod.leg0  𝗉0[ν'.cod.leg0, μ'.cod.leg1],
                    Leg1 = ν'.cod.leg1  𝗉1[ν'.cod.leg0, μ'.cod.leg1]"
        using "2" assms(3,6-8) hcomp_def src_vcomp trg_vcomp by presburger
      moreover have "(ν'  μ')  (ν  μ) =
                     Chn = chine_hcomp ν' μ'  chine_hcomp ν μ,
                      Dom = Leg0 = μ.dom.leg0  𝗉0[ν.dom.leg0, μ.dom.leg1],
                             Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, μ.dom.leg1],
                      Cod = Leg0 = μ'.cod.leg0  𝗉0[ν'.cod.leg0, μ'.cod.leg1],
                             Leg1 = ν'.cod.leg1  𝗉1[ν'.cod.leg0, μ'.cod.leg1]"
        using "1" ν'μ'.arrow_of_spans_axioms νμ.arrow_of_spans_axioms assms(1-6)
              hcomp_def span_vertical_category.seq_char span_vertical_category_axioms vcomp_eq
        by fastforce
      moreover have "chine_hcomp (ν'  ν) (μ'  μ) = chine_hcomp ν' μ'  chine_hcomp ν μ"
      proof -
        have "C.cospan ν'.cod.leg0 μ'.cod.leg1"
          using assms src_def trg_def by simp
        moreover have "C.seq 𝗉1[ν'.cod.leg0, μ'.cod.leg1] (chine_hcomp (ν'  ν) (μ'  μ))"
          using assms 2 C2 chine_hcomp_props [of "μ'  μ" "ν'  ν"] by auto
        moreover have "C.seq 𝗉1[ν'.cod.leg0, μ'.cod.leg1] (chine_hcomp ν' μ'  chine_hcomp ν μ)"
          using assms 1 chine_hcomp_props [of μ ν] chine_hcomp_props [of μ' ν'] by auto
        moreover have "𝗉0[ν'.cod.leg0, μ'.cod.leg1]  chine_hcomp (ν'  ν) (μ'  μ) =
                       𝗉0[ν'.cod.leg0, μ'.cod.leg1]  chine_hcomp ν' μ'  chine_hcomp ν μ"
          by (metis (no_types, lifting) "1" "2" C.comp_assoc Chn_vcomp assms(1-8)
              chine_hcomp_props(5) src_vcomp trg_vcomp)
        moreover have "𝗉1[ν'.cod.leg0, μ'.cod.leg1]  chine_hcomp (ν'  ν) (μ'  μ) =
                       𝗉1[ν'.cod.leg0, μ'.cod.leg1]  chine_hcomp ν' μ'  chine_hcomp ν μ"
          by (metis (no_types, lifting) "1" "3" C.comp_assoc C.prj_tuple(2) C1 C2 Chn_vcomp
              assms(1-3,8) chine_hcomp_def chine_hcomp_props(6))
        ultimately show ?thesis
          using C.prj_joint_monic
                  [of "ν'.cod.leg0" "μ'.cod.leg1"
                      "chine_hcomp (ν'  ν) (μ'  μ)" "chine_hcomp ν' μ'  chine_hcomp ν μ"]
          by simp
      qed
      ultimately show ?thesis by auto
    qed

    interpretation H: "functor" VV.comp vcomp λνμ. fst νμ  snd νμ
    proof
      show "νμ. ¬ VV.arr νμ  fst νμ  snd νμ = null"
        using hcomp_def VV.arr_charSbC null_char by auto
      show "νμ. VV.arr νμ  arr (fst νμ  snd νμ)"
        using arr_char arrow_of_spans_hcomp VV.arr_charSbC by simp
      show "νμ. VV.arr νμ 
                    dom (fst νμ  snd νμ) = fst (VV.dom νμ)  snd (VV.dom νμ)"
        using VV.arr_charSbC VV.dom_charSbC dom_hcomp by auto
      show "νμ. VV.arr νμ  cod (fst νμ  snd νμ) = fst (VV.cod νμ)  snd (VV.cod νμ)"
        using VV.arr_charSbC VV.cod_charSbC cod_hcomp by auto
      show "νμ' νμ. VV.seq νμ' νμ  fst (VV.comp νμ' νμ)  snd (VV.comp νμ' νμ) =
                                        (fst νμ'  snd νμ')  (fst νμ  snd νμ)"
      proof -
        fix νμ' νμ
        assume 1: "VV.seq νμ' νμ"
        have "VV.comp νμ' νμ = (fst νμ'  fst νμ, snd νμ'  snd νμ)"
          by (metis (no_types, lifting) "1" VV.comp_simp VV.seq_charSbC VxV.comp_char VxV.seqEPC)
        thus "fst (VV.comp νμ' νμ)  snd (VV.comp νμ' νμ) =
              (fst νμ'  snd νμ')  (fst νμ  snd νμ)"
          using 1 hcomp_vcomp VV.seq_charSbC VV.arr_charSbC VV.comp_char
          by (metis (no_types, lifting) fst_conv snd_conv)
      qed
    qed

    lemma hcomp_is_functor:
    shows "functor VV.comp vcomp (λνμ. fst νμ  snd νμ)"
      ..

    lemma ide_hcomp:
    assumes "ide f" and "ide g" and "src f = trg g"
    shows "ide (f  g)"
      using assms VV.ide_charSbC VV.arr_charSbC H.preserves_ide [of "(f, g)"] by auto

    sublocale horizontal_composition vcomp hcomp src trg
      using src_hcomp trg_hcomp VV.arr_charSbC not_arr_null hcomp_def null_char
      by (unfold_locales, auto)

    lemma has_horizontal_composition:
    shows "horizontal_composition vcomp hcomp src trg"
      ..

  end

  subsection "The Bicategory Span(C)"

  context span_bicategory
  begin

    lemma arr_eqI:
    assumes "par μ μ'" and "Chn μ = Chn μ'"
    shows "μ = μ'"
      using assms dom_char cod_char by auto

    abbreviation 𝗅
    where "𝗅 f  Chn = 𝗉0[C.cod (Leg1 (Dom f)), Leg1 (Dom f)],
                  Dom = Dom (L f), Cod = Cod f"

    interpretation 𝔩: transformation_by_components vcomp vcomp L map 𝗅
    proof
      have *: "f. ide f  arrow_of_spans C (𝗅 f)"
      proof -
        fix f
        assume f: "ide f"
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        interpret 𝗅f: arrow_of_spans C 𝗅 f
        proof
          show Dom: "C.span (Leg0 (Dom (𝗅 f))) (Leg1 (Dom (𝗅 f)))"
            using f
            by (simp add: arrow_of_spans_hcomp arrow_of_spans.axioms(2)
                span_in_category.is_span)
          interpret Dom: span_in_category C Dom (𝗅 f)
            using Dom by (unfold_locales, auto)
          show Cod: "C.span (Leg0 (Cod (𝗅 f))) (Leg1 (Cod (𝗅 f)))"
            using f hcomp_def trg_def src_def ide_mkObj C.pullback_commutes by force
          interpret Cod: span_in_category C Cod (𝗅 f)
            using Cod by (unfold_locales, auto)
          show "«Chn (𝗅 f) : Dom.apex C Cod.apex»"
          proof -
            have "C.dom Dom.leg0 = C.cod f.dom.leg1 ↓↓ f.dom.leg1"
            proof -
              have "arr (trg f)"
                using f by simp
              hence "Dom (𝗅 f) = Leg0 = f.dom.leg0  𝗉0[C.cod f.dom.leg1, f.dom.leg1],
                                 Leg1 = C.cod f.dom.leg1  𝗉1[C.cod f.dom.leg1, f.dom.leg1]"
                using f src_def trg_def hcomp_def by simp
              thus ?thesis
                using f Dom hcomp_def by auto
            qed
            thus ?thesis
              using f ide_char Dom.apex_def Cod.apex_def by simp
          qed
          show "Cod.leg0  Chn (𝗅 f) = Dom.leg0"
            using f ide_char hcomp_def src_def trg_def C.comp_arr_ide ide_mkObj by simp
          show "Cod.leg1  Chn (𝗅 f) = Dom.leg1"
            using f ide_char hcomp_def src_def trg_def C.pullback_commutes ide_mkObj
                  C.comp_arr_ide
            by (simp add: C.commutative_square_def)
        qed
        show "arrow_of_spans C (𝗅 f)" ..
      qed
      show 0: "f. ide f  «𝗅 f : L f  map f»"
      proof -
        fix f
        assume f: "ide f"
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        interpret 𝗅f: arrow_of_spans C 𝗅 f
          using f * by blast
        show "«𝗅 f : L f  map f»"
        proof
          show 1: "arr (𝗅 f)"
            using f * arr_char by blast
          show "dom (𝗅 f) = L f"
            using f 1 dom_char ideD(2) by auto
          show "cod (𝗅 f) = map f"
            using f 1 cod_char ideD(3) by auto
         qed
      qed
      show "μ. arr μ  𝗅 (cod μ)  L μ = map μ  𝗅 (dom μ)"
      proof -
        fix μ
        assume μ: "arr μ"
        interpret μ: arrow_of_spans C μ
          using μ arr_char by auto
        interpret 𝗅_dom_μ: arrow_of_spans C 𝗅 (dom μ)
          using μ * [of "dom μ"] by fastforce
        interpret 𝗅_cod_μ: arrow_of_spans C 𝗅 (cod μ)
          using μ * [of "cod μ"] by fastforce
        interpret: arrow_of_spans C L μ
          using μ arr_char by blast
        show "𝗅 (cod μ)  L μ = map μ  𝗅 (dom μ)"
        proof (intro arr_eqI)
          show par: "par (𝗅 (cod μ)  L μ) (map μ  𝗅 (dom μ))"
            using μ 0 [of "dom μ"] 0 [of "cod μ"] by fastforce
          show "Chn (𝗅 (cod μ)  L μ) = Chn (map μ  𝗅 (dom μ))"
          proof -
            have "Chn (𝗅 (cod μ)  L μ) =
                   𝗉0[μ.dtrg, μ.cod.leg1] 
                     𝗉1[μ.dtrg, μ.dom.leg1] μ.dtrg, μ.cod.leg1 μ.chine  𝗉0[μ.dtrg, μ.dom.leg1]"
            proof -
              have "Chn (𝗅 (cod μ)  L μ) = 𝗉0[μ.dtrg, μ.cod.leg1]  Chn (trg μ  μ)"
                using Chn_vcomp μ cod_char par by force
              moreover
              have "Chn (trg μ  μ) = 𝗉1[μ.dtrg, μ.dom.leg1]
                                        μ.dtrg, μ.cod.leg1
                                       μ.chine  𝗉0[μ.dtrg, μ.dom.leg1]"
                using μ hcomp_def chine_hcomp_trg_arr by simp
              ultimately show ?thesis
                using μ by (auto simp add: cod_char)
            qed
            also have "... = μ.chine  𝗉0[C.cod μ.dom.leg1, μ.dom.leg1]"
              using μ C.in_homE C.pullback_commutes [of "C.cod μ.dom.leg1" "μ.dom.leg1"]
                    C.comp_reduce ide_char C.prj_tuple(1)
              by auto
            also have "... = Chn (map μ  𝗅 (dom μ))"
              using μ par seq_char dom_char vcomp_eq map_simp by simp
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    interpretation 𝔩: natural_isomorphism vcomp vcomp L map 𝔩.map
    proof
      fix f
      assume f: "ide f"
      show "iso (𝔩.map f)"
      proof -
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        have 1: "𝔩.map f = Chn = 𝗉0[f.dtrg, f.leg1], Dom = Dom (trg f  f), Cod = Dom f"
          using f ide_char cod_char by simp
        interpret 𝗅f: arrow_of_spans C 𝔩.map f
          using f arr_char 𝔩.preserves_reflects_arr by fastforce
        let ?𝗅f' = "Chn = f.leg1 f.dtrg, f.leg1 C.dom f.leg1,
                    Dom = Dom f, Cod = Dom (trg f  f)"
        have 2: "C.inverse_arrows 𝗅f.chine (Chn ?𝗅f')"
          using 1 C.pullback_arr_cod(2) [of "f.leg1"] by simp
        interpret 𝗅f': arrow_of_spans C ?𝗅f'
        proof
          show Dom: "C.span (Leg0 (Dom ?𝗅f')) (Leg1 (Dom ?𝗅f'))"
            using f 1 by auto
          interpret Dom: span_in_category C Dom ?𝗅f'
            using Dom by (unfold_locales, auto)
          show Cod: "C.span (Leg0 (Cod ?𝗅f')) (Leg1 (Cod ?𝗅f'))"
            using f 1 𝗅f.dom.is_span by auto
          interpret Cod: span_in_category C Cod ?𝗅f'
            using Cod by (unfold_locales, auto)
          show "«Chn ?𝗅f' : Dom.apex C Cod.apex»"
            using f src_def trg_def hcomp_def ide_mkObj Cod.apex_def Dom.apex_def
                  C.comp_arr_dom C.comp_cod_arr
            by auto
          show "Cod.leg0  Chn ?𝗅f' = Dom.leg0"
            using 2 𝗅f.leg0_commutes C.invert_side_of_triangle
            by (metis (no_types, lifting) "1" C.inverse_unique C.isoI 𝗅f.dom.is_span
                arrow_of_spans_data.select_convs(2) arrow_of_spans_data.select_convs(3))
          show "Cod.leg1  Chn ?𝗅f' = Dom.leg1"
            using 2 𝗅f.leg1_commutes C.invert_side_of_triangle
            by (metis (no_types, lifting) "1" C.inverse_unique C.isoI 𝗅f.dom.is_span
                arrow_of_spans_data.select_convs(2) arrow_of_spans_data.select_convs(3))
        qed
        have "inverse_arrows (𝔩.map f) ?𝗅f'"
        proof
          show "ide (?𝗅f'  𝔩.map f)"
          proof -
            have "?𝗅f'  𝔩.map f = dom (𝔩.map f)"
            proof -
              have "?𝗅f'  𝔩.map f =
                    Chn = f.dtrg ↓↓ f.leg1, Dom = Dom (𝔩.map f), Cod = Dom (𝔩.map f)"
                using f 1 2 f.arrow_of_spans_axioms 𝗅f.arrow_of_spans_axioms
                      𝗅f'.arrow_of_spans_axioms vcomp_def ide_char arr_char
                by (simp add: vcomp_def C.comp_inv_arr)
              also have "... = dom (𝔩.map f)"
                by (metis (no_types, lifting) "1" C.pbdom_def 𝗅f.chine_simps(2)
                    𝔩.preserves_reflects_arr arrow_of_spans_data.select_convs(1)
                    dom_char f ideD(1))
              finally show ?thesis by blast
            qed
            thus ?thesis
              using 𝗅f.arrow_of_spans_axioms arr_char by simp
          qed
          show "ide (𝔩.map f  ?𝗅f')"
          proof -
            have "𝔩.map f  ?𝗅f' = dom ?𝗅f'"
            proof -
              have "𝔩.map f  ?𝗅f' = Chn = Chn f, Dom = Dom ?𝗅f', Cod = Dom ?𝗅f'"
                using f 1 2 f.arrow_of_spans_axioms 𝗅f.arrow_of_spans_axioms
                      𝗅f'.arrow_of_spans_axioms vcomp_def ide_char arr_char
                by fastforce
              also have "... = dom ?𝗅f'"
                using 1 𝗅f'.arrow_of_spans_axioms arr_char dom_char by simp
              finally show ?thesis by blast
            qed
            thus ?thesis
              using 𝗅f'.arrow_of_spans_axioms arr_char by simp
          qed
        qed
        thus ?thesis by auto
      qed
    qed

    lemma 𝔩_is_natural_isomorphism:
    shows "natural_isomorphism vcomp vcomp L map 𝔩.map"
      ..

    sublocale L: equivalence_functor vcomp vcomp L
      using L.isomorphic_to_identity_is_equivalence 𝔩.natural_isomorphism_axioms by simp

    lemma equivalence_functor_L:
    shows "equivalence_functor vcomp vcomp L"
      ..

    abbreviation 𝗋
    where "𝗋 f  Chn = 𝗉1[Leg0 (Dom f), C.cod (Leg0 (Dom f))],
                  Dom = Dom (R f), Cod = Cod f"

    interpretation ρ: transformation_by_components vcomp vcomp R map 𝗋
    proof
      have *: "f. ide f  arrow_of_spans C (𝗋 f)"
      proof -
        fix f
        assume f: "ide f"
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        interpret 𝗋f: arrow_of_spans C 𝗋 f
        proof
          show Dom: "C.span (Leg0 (Dom (𝗋 f))) (Leg1 (Dom (𝗋 f)))"
            using f
            by (simp add: arrow_of_spans_hcomp arrow_of_spans.axioms(2)
                span_in_category.is_span)
          interpret Dom: span_in_category C Dom (𝗋 f)
            using Dom by (unfold_locales, auto)
          show Cod: "C.span (Leg0 (Cod (𝗋 f))) (Leg1 (Cod (𝗋 f)))"
            using f hcomp_def trg_def src_def ide_mkObj C.pullback_commutes by force
          interpret Cod: span_in_category C Cod (𝗋 f)
            using Cod by (unfold_locales, auto)
          show "«Chn (𝗋 f) : Dom.apex C Cod.apex»"
          proof -
            have "C.dom Dom.leg0 = f.dom.leg0 ↓↓ C.cod f.dom.leg0"
            proof -
              have "arr (src f)"
                using f by simp
              hence "Dom (𝗋 f) = Leg0 = C.cod f.dom.leg0  𝗉0[f.dom.leg0, C.cod f.dom.leg0],
                                  Leg1 = f.dom.leg1  𝗉1[f.dom.leg0, C.cod f.dom.leg0]"
                using f src_def trg_def by (simp add: hcomp_def)
              thus ?thesis
                using f ide_char Dom.apex_def Cod.apex_def by simp
            qed
            thus ?thesis
              using f ide_char Dom.apex_def Cod.apex_def by simp
          qed
          show "Cod.leg0  Chn (𝗋 f) = Dom.leg0"
            using f ide_char hcomp_def src_def trg_def C.pullback_commutes
                  ide_mkObj C.comp_arr_ide
            by (simp add: C.commutative_square_def)
          show "Cod.leg1  Chn (𝗋 f) = Dom.leg1"
            using f ide_char hcomp_def src_def trg_def ide_mkObj C.comp_arr_ide
            by (simp add: C.commutative_square_def)
        qed
        show "arrow_of_spans C (𝗋 f)" ..
      qed
      show 0: "f. ide f  «𝗋 f : R f  map f»"
      proof -
        fix f
        assume f: "ide f"
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        interpret 𝗋f: arrow_of_spans C 𝗋 f
          using f * by blast
        show "«𝗋 f : R f  map f»"
        proof
          show 1: "arr (𝗋 f)"
            using f * arr_char by blast
          show "dom (𝗋 f) = R f"
            using f 1 dom_char ideD(2) by auto
          show "cod (𝗋 f) = map f"
            using f 1 cod_char ideD(3) by auto
         qed
      qed
      show "μ. arr μ  𝗋 (cod μ)  R μ = map μ  𝗋 (dom μ)"
      proof -
        fix μ
        assume μ: "arr μ"
        interpret μ: arrow_of_spans C μ
          using μ arr_char by auto
        interpret 𝗋_dom_μ: arrow_of_spans C 𝗋 (dom μ)
          using μ * [of "dom μ"] by fastforce
        interpret 𝗋_cod_μ: arrow_of_spans C 𝗋 (cod μ)
          using μ * [of "cod μ"] by fastforce
        interpret: arrow_of_spans C R μ
          using μ arr_char by blast
        show "𝗋 (cod μ)  R μ = map μ  𝗋 (dom μ)"
        proof (intro arr_eqI)
          show par: "par (𝗋 (cod μ)  R μ) (map μ  𝗋 (dom μ))"
            using μ 0 [of "dom μ"] 0 [of "cod μ"] by force
          show "Chn (𝗋 (cod μ)  R μ) = Chn (map μ  𝗋 (dom μ))"
          proof -
            have "Chn (𝗋 (cod μ)  R μ) =
                  𝗉1[μ.cod.leg0, μ.cod.src] 
                    μ.chine  𝗉1[μ.dom.leg0, μ.dsrc] μ.cod.leg0, μ.cod.src 𝗉0[μ.dom.leg0, μ.dsrc]"
            proof -
              have "Chn (𝗋 (cod μ)  R μ) = 𝗉1[μ.cod.leg0, μ.cod.src]  Chn (μ  src μ)"
                using Chn_vcomp μ cod_char par by force
              moreover
              have "Chn (μ  src μ) = μ.chine  𝗉1[μ.dom.leg0, μ.dsrc]
                                        μ.cod.leg0, μ.dsrc
                                       𝗉0[μ.dom.leg0, μ.dsrc]"
                using μ hcomp_def chine_hcomp_arr_src by simp
              ultimately show ?thesis
                using μ by (auto simp add: cod_char)
            qed
            also have "... = μ.chine  𝗉1[μ.dom.leg0, C.cod μ.dom.leg0]"
              using μ ide_char C.prj_tuple(2)
                    C.in_homE C.pullback_commutes [of "μ.dom.leg0" "C.cod μ.dom.leg0"]
                    C.comp_reduce
              by auto
            also have "... = Chn (map μ  𝗋 (dom μ))"
              using μ par seq_char dom_char vcomp_eq map_simp by simp
            finally show ?thesis by blast
          qed
        qed
      qed
    qed

    interpretation ρ: natural_isomorphism vcomp vcomp R map ρ.map
    proof
      fix f
      assume f: "ide f"
      show "iso (ρ.map f)"
      proof -
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        have 1: "ρ.map f = Chn = 𝗉1[f.leg0, f.dsrc], Dom = Dom (f  src f), Cod = Dom f"
          using f ide_char by auto
        interpret ρf: arrow_of_spans C ρ.map f
          using f arr_char ρ.preserves_reflects_arr by fastforce
        let ?ρf' = "Chn = C.dom f.leg0 f.leg0, f.dsrc f.leg0,
                     Dom = Dom f, Cod = Dom (f  src f)"
        have 2: "C.inverse_arrows (Chn (ρ.map f)) (Chn ?ρf')"
          using 1 C.pullback_arr_cod(1) [of "f.dom.leg0"] by simp
        interpret ρf': arrow_of_spans C ?ρf'
        proof
          show Dom: "C.span (Leg0 (Dom ?ρf')) (Leg1 (Dom ?ρf'))"
            using f 1 by auto
          interpret Dom: span_in_category C Dom ?ρf'
            using Dom by (unfold_locales, auto)
          show Cod: "C.span (Leg0 (Cod ?ρf')) (Leg1 (Cod ?ρf'))"
            using f 1 ρf.dom.is_span by auto
          interpret Cod: span_in_category C Cod ?ρf'
            using Cod by (unfold_locales, auto)
          show "«Chn ?ρf' : Dom.apex C Cod.apex»"
            using f src_def trg_def hcomp_def ide_mkObj Cod.apex_def Dom.apex_def
                  C.comp_arr_dom C.comp_cod_arr
            by auto
          show "Cod.leg0  Chn ?ρf' = Dom.leg0"
            using 2 ρf.leg0_commutes C.invert_side_of_triangle
            by (metis (no_types, lifting) "1" C.inverse_unique C.isoI ρf.dom.is_span
                arrow_of_spans_data.select_convs(2) arrow_of_spans_data.select_convs(3))
          show "Cod.leg1  Chn ?ρf' = Dom.leg1"
            using 2 ρf.leg1_commutes C.invert_side_of_triangle
            by (metis (no_types, lifting) "1" C.inverse_unique C.isoI ρf.dom.is_span
                arrow_of_spans_data.select_convs(2) arrow_of_spans_data.select_convs(3))
        qed
        have "inverse_arrows (ρ.map f) ?ρf'"
        proof
          show "ide (?ρf'  ρ.map f)"
            using "2" C.comp_inv_arr ρf'.arrow_of_spans_axioms ρf.arrow_of_spans_axioms
                  ρf.chine_simps(2) dom_char f ideD(2) vcomp_def
            by force
          show "ide (ρ.map f  ?ρf')"
          proof -
            have "ρ.map f  ?ρf' = dom ?ρf'"
            proof -
              have "ρ.map f  ?ρf' = Chn = Chn f, Dom = Dom ?ρf', Cod = Dom ?ρf'"
                using f 1 2 f.arrow_of_spans_axioms
                      ρf.arrow_of_spans_axioms ρf'.arrow_of_spans_axioms
                      vcomp_def ide_char arr_char
                by fastforce
              also have "... = dom ?ρf'"
                using 1 ρf'.arrow_of_spans_axioms arr_char dom_char by simp
              finally show ?thesis by blast
            qed
            thus ?thesis
              using ρf'.arrow_of_spans_axioms arr_char by simp
          qed
        qed
        thus ?thesis by auto
      qed
    qed

    lemma ρ_is_natural_isomorphism:
    shows "natural_isomorphism vcomp vcomp R map ρ.map"
      ..

    sublocale R: equivalence_functor vcomp vcomp R
      using R.isomorphic_to_identity_is_equivalence ρ.natural_isomorphism_axioms by simp

    lemma equivalence_functor_R:
    shows "equivalence_functor vcomp vcomp R"
      ..

    definition unit  ("𝗂[_]")
    where "𝗂[a]  Chn = 𝗉0[Chn a, Chn a], Dom = Dom (a  a), Cod = Cod a"

    lemma unit_in_hom [intro]:
    assumes "obj a"
    shows "in_hhom 𝗂[a] a a"
    and "«𝗂[a] : a  a  a»"
    proof -
      show "«𝗂[a] : a  a  a»"
      proof (intro in_homI)
        interpret a: identity_arrow_of_spans C a
          using assms obj_char ide_char' by auto
        have 0: "src a = trg a"
          using assms arr_char obj_char src_def trg_def by (elim objE, auto)
        interpret aa: arrow_of_spans C a  a
          using assms 0 a.arrow_of_spans_axioms arrow_of_spans_hcomp by auto
        interpret aa: identity_arrow_of_spans C a  a
        proof
          have "ide (a  a)"
            using assms 0 obj_char H.preserves_ide by simp
          thus "C.ide aa.chine" using ide_char by auto
        qed
        have 1: "«𝗉0[a.chine, a.chine] : a.chine ↓↓ a.chine C a.chine» 
                 «𝗉1[a.chine, a.chine] : a.chine ↓↓ a.chine C a.chine»"
          by auto
        have 2: "a.dom.leg0 = a.chine  a.dom.leg1 = a.chine 
                 a.cod.leg0 = a.chine  a.cod.leg1 = a.chine"
          using assms obj_char by (cases a, simp_all)
        have 3: "a  a = Chn = a.chine ↓↓ a.chine,
                          Dom = Leg0 = 𝗉0[a.chine, a.chine], Leg1 = 𝗉1[a.chine, a.chine],
                          Cod = Leg0 = 𝗉0[a.chine, a.chine], Leg1 = 𝗉1[a.chine, a.chine]"
          using assms 0 1 2 chine_hcomp_ide_ide hcomp_def C.comp_cod_arr
                a.identity_arrow_of_spans_axioms ide_char'
          by auto
        have "aa.apex = a.chine ↓↓ a.chine"
          using 3 aa.chine_eq_apex by auto
        interpret 𝗂a: arrow_of_spans C 𝗂[a]
        proof
          have 4: "Dom 𝗂[a] = Dom (a  a)"
            using assms hcomp_def unit_def by simp
          have 5: "Cod 𝗂[a] = Cod a"
            using assms unit_def by simp
          show Dom: "C.span (Leg0 (Dom 𝗂[a])) (Leg1 (Dom 𝗂[a]))"
            using 4 by simp
          interpret Dom: span_in_category C Dom 𝗂[a]
            using Dom by (unfold_locales, auto)
          show Cod: "C.span (Leg0 (Cod 𝗂[a])) (Leg1 (Cod 𝗂[a]))"
            using 5 by simp
          interpret Cod: span_in_category C Cod 𝗂[a]
            using Cod by (unfold_locales, auto)
          show "«Chn 𝗂[a] : Dom.apex C Cod.apex»"
            by (simp add: aa.apex = a.chine ↓↓ a.chine unit_def)
          show "Cod.leg0  Chn 𝗂[a] = Dom.leg0"
            unfolding unit_def using 1 2 3 C.comp_cod_arr by auto
          show "Cod.leg1  Chn 𝗂[a] = Dom.leg1"
            unfolding unit_def using 1 2 3 C.comp_cod_arr C.pullback_ide_self by auto
        qed
        show "arr 𝗂[a]"
          using 𝗂a.arrow_of_spans_axioms arr_char by simp
        show "dom 𝗂[a] = hcomp a a"
          using 3 unit_def 𝗂a.arrow_of_spans_axioms arr_char dom_char 𝗂a.dom.apex_def
          by auto
        show "cod 𝗂[a] = a"
          using assms 3 obj_char arr_char dom_char cod_char unit_def
                𝗂a.arrow_of_spans_axioms
          by auto
      qed
      thus "in_hhom 𝗂[a] a a"
        using assms
        by (metis arrI in_hhom_def objE vconn_implies_hpar(1) vconn_implies_hpar(2-4))
    qed

    lemma unit_simps [simp]:
    assumes "obj a"
    shows "src 𝗂[a] = a" and "trg 𝗂[a] = a"
    and "dom 𝗂[a] = hcomp a a" and "cod 𝗂[a] = a"
      using assms unit_in_hom by auto

    lemma iso_unit:
    assumes "obj a"
    shows "iso 𝗂[a]"
    proof -
      have "Chn 𝗂[a] = 𝗉0[Chn a, Chn a]"
        unfolding unit_def by simp
      moreover have "C.iso 𝗉0[Chn a, Chn a]"
        using assms C.ide_is_iso C.iso_is_arr C.iso_pullback_ide ide_char by blast
      ultimately show ?thesis
        using assms unit_in_hom iso_char by auto
    qed

  end

  locale two_composable_arrows_of_spans =
    span_bicategory +
  μ: arrow_of_spans C μ +
  ν: arrow_of_spans C ν
  for μ (structure)
  and ν (structure) +
  assumes composable: "src μ = trg ν"
  begin

    lemma are_arrows [simp]:
    shows "arr μ" and "arr ν"
      using arr_char μ.arrow_of_spans_axioms ν.arrow_of_spans_axioms by auto

    lemma legs_form_cospan:
    shows "C.cospan μ.dom.leg0 ν.dom.leg1" and "C.cospan μ.cod.leg0 ν.cod.leg1"
      using composable src_def trg_def by auto

    interpretation μν: arrow_of_spans C μ  ν
      using arrow_of_spans_hcomp composable by auto

    lemma composite_is_arrow [simp]:
    shows "arr (μ  ν)"
      using μν.arrow_of_spans_axioms arr_char by auto

    lemma composite_in_hom [intro]:
    shows "«μ  ν : dom μ  dom ν  cod μ  cod ν»"
      using composable by auto

    lemma composite_simps [simp]:
    shows "src (μ  ν) = src ν" and "trg (μ  ν) = trg μ"
    and "dom (μ  ν) = dom μ  dom ν" and "cod (μ  ν) = cod μ  cod ν"
      by (simp_all add: composable)

    lemma chine_composite:
    shows "Chn (μ  ν) = μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1]
                           μ.cod.leg0, ν.cod.leg1
                          ν.chine  𝗉0[μ.dom.leg0, ν.dom.leg1]"
       unfolding hcomp_def chine_hcomp_def using composable by simp

    lemma chine_composite_in_hom [intro]:
    shows "«Chn (μ  ν) : μ.dom.leg0 ↓↓ ν.dom.leg1 C μ.cod.leg0 ↓↓ ν.cod.leg1»"
      using hcomp_def chine_hcomp_props(1) composable by auto

  end

  sublocale two_composable_arrows_of_spans  arrow_of_spans C μ  ν
  proof -
    interpret Domμ_Domν: composite_span C prj0 prj1 Dom μ Dom ν
      using legs_form_cospan(1) by (unfold_locales, auto)
    interpret Codμ_Codν: composite_span C prj0 prj1 Cod μ Cod ν
      using legs_form_cospan(1) by (unfold_locales, auto)
    interpret Dom_μν: span_in_category C Dom (μ  ν)
      apply unfold_locales apply (unfold hcomp_def)
      using Domμ_Domν.apex_def Domμ_Domν.leg_simps(1) are_arrows(1) composable by auto
    interpret Cod_μν: span_in_category C Cod (μ  ν)
      apply unfold_locales apply (unfold hcomp_def)
      using Codμ_Codν.apex_def Codμ_Codν.leg_simps(1) are_arrows(1) composable by auto
    show "arrow_of_spans C (μ  ν)"
    proof
      show "«Chn (hcomp μ ν) : Dom_μν.apex C Cod_μν.apex»"
        unfolding hcomp_def
        using are_arrows(1) are_arrows(2) arrow_of_spans_hcomp composable hcomp_def
              arrow_of_spans.chine_in_hom Codμ_Codν.leg_simps(4) Domμ_Domν.leg_simps(3)
              Domμ_Domν.leg_simps(4) chine_composite_in_hom
        by auto
      show "Cod_μν.leg0  Chn (hcomp μ ν) = Dom_μν.leg0"
      proof (unfold hcomp_def)
        have "arrow_of_spans C
                Chn = chine_hcomp μ ν, Dom = Domμ_Domν.this, Cod = Codμ_Codν.this"
          using arrow_of_spans_hcomp composable hcomp_def by auto
        thus "Leg0 (Cod (if arr ν  arr μ  src μ = trg ν then
                            Chn = chine_hcomp μ ν,
                             Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                         else null)) 
                      Chn (if arr ν  arr μ  src μ = trg ν then
                             Chn = chine_hcomp μ ν,
                              Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                           else null) =
              Leg0 (Dom (if arr ν  arr μ  src μ = trg ν then
                            Chn = chine_hcomp μ ν,
                             Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                         else null))"
          using arrow_of_spans.leg0_commutes composable by fastforce
      qed
      show "Cod_μν.leg1  Chn (hcomp μ ν) = Dom_μν.leg1"
      proof (unfold hcomp_def)
        have "arrow_of_spans C
                Chn = chine_hcomp μ ν, Dom = Domμ_Domν.this, Cod = Codμ_Codν.this"
          using arrow_of_spans_hcomp composable hcomp_def by force
        thus "Leg1 (Cod (if arr ν  arr μ  src μ = trg ν then
                           Chn = chine_hcomp μ ν,
                            Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                         else null)) 
                    Chn (if arr ν  arr μ  src μ = trg ν then
                           Chn = chine_hcomp μ ν,
                            Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                         else null) =
              Leg1 (Dom (if arr ν  arr μ  src μ = trg ν then
                           Chn = chine_hcomp μ ν,
                            Dom = Domμ_Domν.this, Cod = Codμ_Codν.this
                         else null))"
          using arrow_of_spans.leg1_commutes composable by force
        qed
    qed
  qed

  locale two_composable_identity_arrows_of_spans =
     two_composable_arrows_of_spans +
  μ: identity_arrow_of_spans C μ +
  ν: identity_arrow_of_spans C ν
  begin

    lemma are_identities [simp]:
    shows "ide μ" and "ide ν"
      using ide_char μ.arrow_of_spans_axioms ν.arrow_of_spans_axioms by auto

    interpretation H: "functor" VV.comp vcomp λνμ. fst νμ  snd νμ
      using hcomp_is_functor by auto

    interpretation μν: identity_arrow_of_spans C μ  ν
      using are_identities(1-2) composable ide_char' by blast

    lemma ide_composite [simp]:
    shows "ide (μ  ν)"
      using μν.identity_arrow_of_spans_axioms arrow_of_spans_axioms ide_char by auto

    lemma apex_composite:
    shows "μν.apex = μ.leg0 ↓↓ ν.leg1"
      using dom.apex_def hcomp_def chine_hcomp_ide_ide composable legs_form_cospan
      by simp

    lemma leg0_composite:
    shows "μν.leg0 = ν.leg0  𝗉0[μ.leg0, ν.leg1]"
      using dom.apex_def hcomp_def composable legs_form_cospan by simp

    lemma leg1_composite:
    shows "μν.leg1 = μ.leg1  𝗉1[μ.leg0, ν.leg1]"
      using dom.apex_def hcomp_def composable legs_form_cospan by simp

    lemma chine_composite:
    shows "Chn (μ  ν) = μ.leg0 ↓↓ ν.leg1"
       unfolding hcomp_def using chine_hcomp_ide_ide composable by simp

    abbreviation prj0
    where "prj0  𝗉0[μ.leg0, ν.leg1]"

    abbreviation prj1
    where "prj1  𝗉1[μ.leg0, ν.leg1]"

    lemma prj_in_hom [intro]:
    shows "«prj1 : μ.leg0 ↓↓ ν.leg1 C μ.apex»"
    and "«prj0 : μ.leg0 ↓↓ ν.leg1 C ν.apex»"
      using legs_form_cospan by auto

    lemma prj_simps [simp]:
    shows "C.arr prj1" and "C.dom prj1 = μ.leg0 ↓↓ ν.leg1" and "C.cod prj1 = μ.apex"
    and "C.arr prj0" and "C.dom prj0 = μ.leg0 ↓↓ ν.leg1" and "C.cod prj0 = ν.apex"
      using prj_in_hom by auto

    sublocale identity_arrow_of_spans C μ  ν
      using apex_composite dom.ide_apex chine_composite by (unfold_locales, auto)

  end

  locale three_composable_arrows_of_spans =
     span_bicategory +
  μ: arrow_of_spans C μ +
  ν: arrow_of_spans C ν +
  π: arrow_of_spans C π +
  μν: two_composable_arrows_of_spans C prj0 prj1 μ ν +
  νπ: two_composable_arrows_of_spans C prj0 prj1 ν π
  for μ (structure)
  and ν (structure)
  and π (structure)
  begin

    interpretation μνπ: arrow_of_spans C μ  ν  π
      using μ.arrow_of_spans_axioms νπ.arrow_of_spans_axioms
            arrow_of_spans_hcomp arr_char μν.composable νπ.composable
      by force

    interpretation μν_π: arrow_of_spans C (μ  ν)  π
      using μν.arrow_of_spans_axioms π.arrow_of_spans_axioms
            arrow_of_spans_hcomp arr_char μν.composable νπ.composable
      by force

    lemma composites_are_arrows [simp]:
    shows "arr (μ  ν  π)" and "arr ((μ  ν)  π)"
      using μνπ.arrow_of_spans_axioms μν_π.arrow_of_spans_axioms arr_char by auto

    lemma composite_in_hom [intro]:
    shows "«μ  ν  π : dom μ  dom ν  dom π  cod μ  cod ν  cod π»"
    and "«(μ  ν)  π : (dom μ  dom ν)  dom π  (cod μ  cod ν)  cod π»"
      using μν.composable νπ.composable by auto

    lemma composite_simps [simp]:
    shows "src (μ  ν  π) = src π"
    and "src ((μ  ν)  π) = src π"
    and "trg (μ  ν  π) = trg μ"
    and "trg ((μ  ν)  π) = trg μ"
    and "dom (μ  ν  π) = dom μ  dom ν  dom π"
    and "dom ((μ  ν)  π) = (dom μ  dom ν)  dom π"
    and "cod (μ  ν  π) = cod μ  cod ν  cod π"
    and "cod ((μ  ν)  π) = (cod μ  cod ν)  cod π"
      by (auto simp add: μν.composable νπ.composable)

    lemma chine_composite:
    shows "μνπ.chine =
             μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1]]
               μ.cod.leg0, ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]
              ν.chine  𝗉1[ν.dom.leg0, π.dom.leg1]
                ν.cod.leg0, π.cod.leg1
               π.chine  𝗉0[ν.dom.leg0, π.dom.leg1] 
                 𝗉0[μ.dom.leg0, ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1]]"
    and "μν_π.chine =
           μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1]
              μ.cod.leg0, ν.cod.leg1
            ν.chine  𝗉0[μ.dom.leg0, ν.dom.leg1] 
              𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]
              ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1
            π.chine  𝗉0[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
    proof -
      show "μνπ.chine =
             μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1]]
               μ.cod.leg0, ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]
              ν.chine  𝗉1[ν.dom.leg0, π.dom.leg1]
                ν.cod.leg0, π.cod.leg1
               π.chine  𝗉0[ν.dom.leg0, π.dom.leg1] 
                 𝗉0[μ.dom.leg0, ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1]]"
       unfolding hcomp_def chine_hcomp_def μν.composable νπ.composable
       using trg_def νπ.are_arrows(1-2) νπ.composable νπ.composite_is_arrow
             νπ.composite_simps(2) hcomp_def
       by (simp add: chine_hcomp_def)
     show "μν_π.chine =
             μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1]
                μ.cod.leg0, ν.cod.leg1
              ν.chine  𝗉0[μ.dom.leg0, ν.dom.leg1] 
                𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]
                ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1
              π.chine  𝗉0[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
        unfolding hcomp_def chine_hcomp_def μν.composable νπ.composable
        using src_def μν.are_arrows(1-2) μν.composable μν.composite_is_arrow
              μν.composite_simps(1) hcomp_def νπ.composable
        by (simp add: chine_hcomp_def)
    qed

  end

  locale three_composable_identity_arrows_of_spans =
    three_composable_arrows_of_spans +
  μ: identity_arrow_of_spans C μ +
  ν: identity_arrow_of_spans C ν +
  π: identity_arrow_of_spans C π +
  μν: two_composable_identity_arrows_of_spans C prj0 prj1 μ ν +
  νπ: two_composable_identity_arrows_of_spans C prj0 prj1 ν π
  begin

    lemma composites_are_identities [simp]:
    shows "ide (μ  ν  π)" and "ide ((μ  ν)  π)"
      by (auto simp add: μν.composable νπ.composable)

    interpretation μνπ: identity_arrow_of_spans C μ  ν  π
      using composites_are_identities ide_char' by auto
    interpretation μν_π: identity_arrow_of_spans C (μ  ν)  π
      using composites_are_identities ide_char' by auto

    abbreviation Prj11
    where "Prj11  𝗉1[μ.leg0, ν.leg1]  𝗉1[ν.leg0  𝗉0[μ.leg0, ν.leg1], π.leg1]"
    abbreviation Prj01
    where "Prj01  𝗉0[μ.leg0, ν.leg1]  𝗉1[ν.leg0  𝗉0[μ.leg0, ν.leg1], π.leg1]"
    abbreviation Prj0
    where "Prj0  𝗉0[ν.leg0  𝗉0[μ.leg0, ν.leg1], π.leg1]"

    abbreviation Prj1
    where "Prj1  𝗉1[μ.leg0, ν.leg1  𝗉1[ν.leg0, π.leg1]]"
    abbreviation Prj10
    where "Prj10  𝗉1[ν.leg0, π.leg1]  𝗉0[μ.leg0, ν.leg1  𝗉1[ν.leg0, π.leg1]]"
    abbreviation Prj00
    where "Prj00  𝗉0[ν.leg0, π.leg1]  𝗉0[μ.leg0, ν.leg1  𝗉1[ν.leg0, π.leg1]]"

    lemma leg0_composite:
    shows "μνπ.leg0 = π.leg0  Prj00"
    and "μν_π.leg0 = π.leg0  Prj0"
    proof -
      show "μνπ.leg0 = π.leg0  Prj00"
        using hcomp_def μν.composable νπ.composite_is_arrow νπ.composite_simps(2)
              C.comp_assoc
        by auto
      show "μν_π.leg0 = π.leg0  Prj0"
        using hcomp_def μν.composite_is_arrow μν.composite_simps(1) νπ.composable by auto
    qed

    lemma leg1_composite:
    shows "μνπ.leg1 = μ.leg1  Prj1"
    and "μν_π.leg1 = μ.leg1  Prj11"
    proof -
      show "μνπ.leg1 = μ.leg1  Prj1"
        using hcomp_def μν.composable νπ.composite_is_arrow νπ.composite_simps(2) by auto
      show "μν_π.leg1 = μ.leg1  Prj11"
        using hcomp_def μν.composite_is_arrow μν.composite_simps(1) νπ.composable
              C.comp_assoc
        by auto
    qed

    definition chine_assoc
    where "chine_assoc 
           Prj11 μ.leg0, ν.leg1  𝗉1[ν.leg0, π.leg1] Prj01 ν.leg0, π.leg1 Prj0"

    definition chine_assoc'
    where "chine_assoc' 
           Prj1 μ.leg0, ν.leg1 Prj10 ν.leg0  𝗉0[μ.leg0, ν.leg1], π.leg1 Prj00"

    (*
     * Don't be fooled by how short the following proofs look -- there's a heck of a lot
     * going on behind the scenes here!
     *)
    lemma chine_composite:
    shows "μν_π.chine = ν.leg0  μν.prj0 ↓↓ π.leg1"
    and "μνπ.chine = μ.leg0 ↓↓ ν.leg1  νπ.prj1"
    proof -
      show "μν_π.chine = ν.leg0  μν.prj0 ↓↓ π.leg1"
        using hcomp_def chine_hcomp_arr_ide [of "hcomp μ ν" π] chine_hcomp_ide_ide
              src_def trg_def μν.composable νπ.composable μν.ide_composite
              μν.are_identities νπ.are_identities(2)
        by simp
      show "μνπ.chine = μ.leg0 ↓↓ ν.leg1  νπ.prj1"
        using hcomp_def chine_hcomp_ide_arr [of μ "hcomp ν π"] chine_hcomp_ide_ide
              src_def trg_def μν.composable νπ.composable νπ.ide_composite
              μν.are_identities νπ.are_identities(2)
        by simp
    qed

    lemma prj_in_hom [intro]:
    shows "«Prj11 : μν_π.chine C μ.apex»"
    and "«Prj01 : μν_π.chine C ν.apex»"
    and "«Prj0 : μν_π.chine C π.apex»"
    and "«Prj1 : μνπ.chine C μ.apex»"
    and "«Prj10 : μνπ.chine C ν.apex»"
    and "«Prj00 : μνπ.chine C π.apex»"
      using μν.composable νπ.composable src_def trg_def chine_composite by auto

    lemma prj_simps [simp]:
    shows "C.arr Prj11"
    and "C.arr Prj01"
    and "C.arr Prj0"
    and "C.dom Prj11 = μν_π.chine"
    and "C.dom Prj01 = μν_π.chine"
    and "C.dom Prj0 = μν_π.chine"
    and "C.cod Prj11 = μ.apex"
    and "C.cod Prj01 = ν.apex"
    and "C.cod Prj0 = π.apex"
    and "C.arr Prj1"
    and "C.arr Prj10"
    and "C.arr Prj00"
    and "C.dom Prj1 = μνπ.chine"
    and "C.dom Prj10 = μνπ.chine"
    and "C.dom Prj00 = μνπ.chine"
    and "C.cod Prj1 = μ.apex"
    and "C.cod Prj10 = ν.apex"
    and "C.cod Prj00 = π.apex"
      using prj_in_hom by auto

    lemma chine_assoc_props:
    shows "«chine_assoc : μν_π.chine C μνπ.chine»"
    and "Prj1  chine_assoc = Prj11"
    and "Prj10  chine_assoc = Prj01"
    and "Prj00  chine_assoc = Prj0"
    proof -
      have 1: "ν.leg0  Prj01 = π.leg1  Prj0"
        using μν.are_identities νπ.are_identities μν.composable νπ.composable src_def trg_def
              C.pullback_commutes [of "ν.leg0  𝗉0[μ.leg0, ν.leg1]" π.leg1] C.comp_assoc
        by auto
      have 2: "μ.leg0  Prj11 = ν.leg1  Prj01"
        by (metis C.comp_assoc C.pullback_commutes' μν.legs_form_cospan(1))
      show "«chine_assoc : μν_π.chine C μνπ.chine»"
        unfolding chine_assoc_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def chine_composite C.comp_assoc by auto
      show "Prj1  chine_assoc = Prj11"
        unfolding chine_assoc_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def C.comp_assoc
        by auto
      show "Prj10  chine_assoc = Prj01"
        unfolding chine_assoc_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def C.comp_assoc
        by auto
      show "Prj00  chine_assoc = Prj0"
        unfolding chine_assoc_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def C.comp_assoc
        by auto
    qed

    lemma chine_assoc_in_hom [intro]:
    shows "«chine_assoc : μν_π.chine C μνπ.chine»"
      using chine_assoc_props(1) by simp

    lemma prj_chine_assoc [simp]:
    shows "Prj1  chine_assoc = Prj11"
    and "Prj10  chine_assoc = Prj01"
    and "Prj00  chine_assoc = Prj0"
      using chine_assoc_props(2-4) by auto

    lemma chine_assoc'_props:
    shows "«chine_assoc' : μνπ.chine C μν_π.chine»"
    and "Prj11  chine_assoc' = Prj1"
    and "Prj01  chine_assoc' = Prj10"
    and "Prj0  chine_assoc' = Prj00"
    proof -
      have 1: "μ.leg0  Prj1 = ν.leg1  Prj10"
        using μν.are_identities νπ.are_identities μν.composable νπ.composable
              src_def trg_def C.pullback_commutes [of μ.leg0 "ν.leg1  𝗉1[ν.leg0, π.leg1]"]
              C.comp_assoc
        by auto
      have 2: "ν.leg0  Prj10 = π.leg1  Prj00"
        by (metis C.comp_assoc C.pullback_commutes' νπ.legs_form_cospan(1))
      show "«chine_assoc' : μνπ.chine C μν_π.chine»"
        unfolding chine_assoc'_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def chine_composite C.comp_assoc
        by auto
      show "Prj11  chine_assoc' = Prj1"
          unfolding chine_assoc'_def
          using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
                src_def trg_def C.comp_assoc
          by auto
      show "Prj01  chine_assoc' = Prj10"
        unfolding chine_assoc'_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def C.comp_assoc
        by auto
      show "Prj0  chine_assoc' = Prj00"
        unfolding chine_assoc'_def
        using μν.are_identities νπ.are_identities μν.composable νπ.composable 1 2
              src_def trg_def C.comp_assoc
        by auto
    qed

    lemma chine_assoc'_in_hom [intro]:
    shows "«chine_assoc' : μνπ.chine C μν_π.chine»"
      using chine_assoc'_props(1) by simp

    lemma prj_chine_assoc' [simp]:
    shows "Prj11  chine_assoc' = Prj1"
    and "Prj01  chine_assoc' = Prj10"
    and "Prj0  chine_assoc' = Prj00"
      using chine_assoc'_props(2-4) by auto

    lemma prj_joint_monic:
    assumes "«h: a C μν_π.chine»" and "«h': a C μν_π.chine»"
    and "Prj11  h = Prj11  h'" and "Prj01  h = Prj01  h'" and "Prj0  h = Prj0  h'"
    shows "h = h'"
    proof -
      have "𝗉1[ν.leg0  μν.prj0, π.leg1]  h = 𝗉1[ν.leg0  μν.prj0, π.leg1]  h'"
      proof -
        have "μν.prj0  𝗉1[ν.leg0  μν.prj0, π.leg1]  h = μν.prj0  𝗉1[ν.leg0  μν.prj0, π.leg1]  h'"
          using assms μν.composable νπ.composable src_def trg_def chine_composite(1)
                C.comp_assoc
          by force
        moreover
        have "μν.prj1  𝗉1[ν.leg0  μν.prj0, π.leg1]  h = μν.prj1  𝗉1[ν.leg0  μν.prj0, π.leg1]  h'"
          using assms μν.composable νπ.composable src_def trg_def chine_composite(1)
                C.comp_assoc
          by force
        ultimately show ?thesis
          using assms μν.composable νπ.composable src_def trg_def
                chine_composite(1) cod_char
                C.prj_joint_monic
                  [of μ.leg0 ν.leg1 "𝗉1[ν.leg0  μν.prj0, π.leg1]  h"
                      "𝗉1[ν.leg0  μν.prj0, π.leg1]  h'"]
          by auto
      qed
      moreover have "Prj0  h = Prj0  h'"
        using assms cod_char by simp
      ultimately show ?thesis
        using assms μν.composable νπ.composable src_def trg_def
              chine_composite(1) cod_char
              C.prj_joint_monic [of "ν.leg0  μν.prj0" π.leg1 h h']
        by auto
    qed

    lemma prj'_joint_monic:
    assumes "«h: a C μνπ.chine»" and "«h': a C μνπ.chine»"
    and "Prj1  h = Prj1  h'" and "Prj10  h = Prj10  h'" and "Prj00  h = Prj00  h'"
    shows "h = h'"
    proof -
      have "𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h = 𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h'"
      proof -
        have "νπ.prj0  𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h = νπ.prj0  𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h'"
          using assms μν.composable νπ.composable src_def trg_def chine_composite(2)
                C.comp_assoc
          by force
        moreover
        have "νπ.prj1  𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h = νπ.prj1  𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h'"
          using assms μν.composable νπ.composable src_def trg_def chine_composite(2)
                C.comp_assoc
          by force
        ultimately show ?thesis
          using assms μν.composable νπ.composable src_def trg_def
                chine_composite(2) cod_char
                C.prj_joint_monic
                  [of ν.leg0 π.leg1 "𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h"
                      "𝗉0[μ.leg0, ν.leg1  νπ.prj1]  h'"]
          by auto
      qed
      moreover have "Prj1  h = Prj1  h'"
        using assms cod_char by simp
      ultimately show ?thesis
        using assms μν.composable νπ.composable src_def trg_def chine_composite(2)
              C.prj_joint_monic [of μ.leg0 "ν.leg1  νπ.prj1" h h']
        by auto
    qed

    lemma chine_assoc_inverse:
    shows "C.inverse_arrows chine_assoc chine_assoc'"
    proof
      show "C.ide (chine_assoc'  chine_assoc)"
      proof -
        have 1: "C.ide μν_π.chine"
          using chine_assoc_props(1) C.ide_dom by fastforce
        have "chine_assoc'  chine_assoc = μν_π.chine"
        proof -
          have 2: "C.seq chine_assoc' chine_assoc"
            using chine_assoc_props(1) chine_assoc'_props(1) by auto
          have 3: "C.seq Prj11 chine_assoc'  C.seq Prj01 chine_assoc'  C.seq Prj0 chine_assoc'"
            using prj_in_hom chine_assoc'_props(1) by auto
          have "Prj11  chine_assoc'  chine_assoc = Prj11  μν_π.chine"
          proof -
            have "Prj11  chine_assoc'  chine_assoc = (Prj11  chine_assoc')  chine_assoc"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom by simp
          qed
          moreover have "Prj01  chine_assoc'  chine_assoc = Prj01  μν_π.chine"
          proof -
            have "Prj01  chine_assoc'  chine_assoc = (Prj01  chine_assoc')  chine_assoc"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom by simp
          qed
          moreover have "Prj0  chine_assoc'  chine_assoc = Prj0  μν_π.chine"
          proof -
            have "Prj0  chine_assoc'  chine_assoc = (Prj0  chine_assoc')  chine_assoc"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom C.comp_arr_ide prj_in_hom(3) by auto
          qed
          moreover have "«μν_π.chine : μν_π.chine C μν_π.chine»"
            using chine_assoc_props(1) C.ide_dom [of chine_assoc]
            by (elim C.in_homE, auto)
          ultimately show ?thesis
            using chine_assoc_props(1) chine_assoc'_props(1)
                  prj_joint_monic [of "chine_assoc'  chine_assoc" "μν_π.chine" "μν_π.chine"]
            by auto
        qed
        thus ?thesis
          using 1 by simp
      qed
      show "C.ide (chine_assoc  chine_assoc')"
       proof -
        have 1: "C.ide μνπ.chine"
          using chine_assoc_props(1) C.ide_cod by fastforce
        have "chine_assoc  chine_assoc' = μνπ.chine"
        proof -
          have 2: "C.seq chine_assoc chine_assoc'"
            using chine_assoc_props(1) chine_assoc'_props(1) by auto
          have 3: "C.seq Prj1 chine_assoc  C.seq Prj10 chine_assoc  C.seq Prj00 chine_assoc"
            using prj_in_hom chine_assoc_props(1) by auto
          have "Prj1  chine_assoc  chine_assoc' = Prj1  μνπ.chine"
          proof -
            have "Prj1  chine_assoc  chine_assoc' = (Prj1  chine_assoc)  chine_assoc'"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom prj_in_hom(4) by auto
          qed
          moreover have "Prj10  chine_assoc  chine_assoc' = Prj10  μνπ.chine"
          proof -
            have "Prj10  chine_assoc  chine_assoc' = (Prj10  chine_assoc)  chine_assoc'"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom by simp
          qed
          moreover have "Prj00  chine_assoc  chine_assoc' = Prj00  μνπ.chine"
          proof -
            have "Prj00  chine_assoc  chine_assoc' = (Prj00  chine_assoc)  chine_assoc'"
              using C.comp_assoc by metis
            thus ?thesis using 1 C.comp_arr_dom by simp
          qed
          moreover have "«μνπ.chine : μνπ.chine C μνπ.chine»"
            using chine_assoc'_props(1) C.ide_dom [of chine_assoc']
            by (elim C.in_homE, auto)
          ultimately show ?thesis
            using chine_assoc_props(1) chine_assoc'_props(1)
                  prj'_joint_monic [of "chine_assoc  chine_assoc'" "μνπ.chine" "μνπ.chine"]
            by auto
        qed
        thus ?thesis
          using 1 by simp
      qed
    qed

  end

  context three_composable_arrows_of_spans
  begin

    interpretation V: category vcomp
      using is_category by auto
    interpretation H: horizontal_homs vcomp src trg
      using has_horizontal_homs by auto

    interpretation dom_μ: arrow_of_spans C dom μ
      using μ.arrow_of_spans_axioms arr_char [of "dom μ"] by auto
    interpretation dom_ν: arrow_of_spans C dom ν
      using ν.arrow_of_spans_axioms arr_char [of "dom ν"] by auto
    interpretation dom_π: arrow_of_spans C dom π
      using π.arrow_of_spans_axioms arr_char [of "dom π"] by auto
    interpretation doms: three_composable_identity_arrows_of_spans C prj0 prj1
                           dom μ dom ν dom π
      using μν.composable νπ.composable ide_char [of "dom μ"] ide_char [of "dom ν"]
            ide_char [of "dom π"]
      by (unfold_locales, auto)

    interpretation cod_μ: arrow_of_spans C cod μ
      using μ.arrow_of_spans_axioms arr_char [of "cod μ"] by auto
    interpretation cod_ν: arrow_of_spans C cod ν
      using ν.arrow_of_spans_axioms arr_char [of "cod ν"] by auto
    interpretation cod_π: arrow_of_spans C cod π
      using π.arrow_of_spans_axioms arr_char [of "cod π"] by auto
    interpretation cods: three_composable_identity_arrows_of_spans C prj0 prj1
                           cod μ cod ν cod π
      using μν.composable νπ.composable ide_char [of "cod μ"] ide_char [of "cod ν"]
            ide_char [of "cod π"]
      by (unfold_locales, auto)

    interpretation μνπ: arrow_of_spans C μ  ν  π
      using μ.arrow_of_spans_axioms νπ.arrow_of_spans_axioms
            arrow_of_spans_hcomp arr_char μν.composable νπ.composable
      by force

    interpretation μν_π: arrow_of_spans C (μ  ν)  π
      using μν.arrow_of_spans_axioms π.arrow_of_spans_axioms
            arrow_of_spans_hcomp arr_char μν.composable νπ.composable
      by force

    lemma chine_composite':
    shows "μνπ.chine = μ.chine  doms.Prj1
                         μ.cod.leg0, ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]
                       ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00"
    and "μν_π.chine = μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01
                         ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1
                       π.chine  doms.Prj0"
    proof -
      show "μν_π.chine = μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01
                           ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1
                         π.chine  doms.Prj0"
      proof -
        have "arr (μ  ν)" by simp
        thus ?thesis
           unfolding hcomp_def chine_hcomp_def dom_char
           using μν.composable νπ.composable src_def trg_def dom_char chine_hcomp_props
                 C.comp_tuple_arr C.pullback_commutes C.comp_assoc
           by auto
      qed
      show "μνπ.chine = μ.chine  doms.Prj1
                          μ.cod.leg0, ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]
                        ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00"
      proof -
        have "arr (ν  π)" by simp
        thus ?thesis
           unfolding hcomp_def chine_hcomp_def dom_char
           using μν.composable νπ.composable src_def trg_def dom_char chine_hcomp_props
                 C.comp_tuple_arr C.pullback_commutes C.comp_assoc
           by auto
      qed
    qed

    lemma chine_composite_in_hom [intro]:
    shows "«μν_π.chine : Chn ((dom μ  dom ν)  dom π) C Chn ((cod μ  cod ν)  cod π)»"
    and "«μνπ.chine : Chn (dom μ  dom ν  dom π) C Chn (cod μ  cod ν  cod π)»"
      using Chn_in_hom by auto

    lemma cospan_μν:
    shows "C.cospan μ.dom.leg0 ν.dom.leg1"
      using μν.legs_form_cospan by simp

    lemma cospan_νπ:
    shows "C.cospan ν.dom.leg0 π.dom.leg1"
      using νπ.legs_form_cospan by simp

    lemma commutativities:
    shows "μ.cod.leg0  μ.chine  doms.Prj11 = ν.cod.leg1  ν.chine  doms.Prj01"
    and "π.cod.leg1  π.chine  doms.Prj0 =
         (ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1]) 
           μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01"
    proof -
      have AB: "μ.dom.leg0  doms.Prj11 = ν.dom.leg1  doms.Prj01"
      proof -
        have "μ.dom.leg0  doms.Prj11 =
              (μ.dom.leg0  𝗉1[μ.dom.leg0, ν.dom.leg1]) 
                𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
          using μν.composable νπ.composable src_def trg_def dom_char C.comp_assoc
          by simp
        also have "... = (ν.dom.leg1  𝗉0[μ.dom.leg0, ν.dom.leg1]) 
                           𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
          using C.pullback_commutes' μν.legs_form_cospan by auto
        also have "... = ν.dom.leg1  doms.Prj01"
          using μν.composable νπ.composable src_def trg_def dom_char C.comp_assoc
          by simp
        finally show ?thesis by auto
      qed
      have BC: "ν.dom.leg0  doms.Prj01 = π.dom.leg1  doms.Prj0"
      proof -
        have "ν.dom.leg0  doms.Prj01 =
              (ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1]) 
                𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
          using μν.composable νπ.composable src_def trg_def dom_char C.comp_assoc
          by simp
        also have "... = π.dom.leg1  doms.Prj0"
          using C.pullback_commutes' dom_char cod_char μν.legs_form_cospan νπ.legs_form_cospan
          by auto
        finally show ?thesis by simp
      qed                    
      show 1: "μ.cod.leg0  μ.chine  doms.Prj11 = ν.cod.leg1  ν.chine  doms.Prj01"
        using AB C.comp_assoc [of μ.cod.leg0 μ.chine]
              C.comp_assoc [of ν.cod.leg1 ν.chine doms.Prj01]
        by simp
      show "π.cod.leg1  π.chine  doms.Prj0 =
            (ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1]) 
              μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01"
      proof -
        have "(ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1]) 
                μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01 =
              ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1] 
                μ.chine  doms.Prj11 μ.cod.leg0, ν.cod.leg1 ν.chine  doms.Prj01"
          using 1 μν.composable νπ.composable src_def trg_def dom_char C.comp_assoc by simp
        also have "... = ν.cod.leg0  ν.chine  doms.Prj01"
          using 1 dom_char μν.composable νπ.composable src_def trg_def by simp
        also have "... = (ν.cod.leg0  ν.chine)  doms.Prj01"
          using C.comp_assoc [of ν.cod.leg0 ν.chine doms.Prj01] by simp
        also have "... = (π.cod.leg1  π.chine)  doms.Prj0"
          using BC by simp
        also have "... = π.cod.leg1  π.chine  doms.Prj0"
          using C.comp_assoc by blast
        finally show ?thesis by simp
      qed
    qed

    lemma prj_chine_composite:
    shows "cods.Prj11  μν_π.chine = μ.chine  doms.Prj11"
    and "cods.Prj01  μν_π.chine = ν.chine  doms.Prj01"
    and "cods.Prj0  μν_π.chine = π.chine  doms.Prj0"
      using μν.composable νπ.composable src_def trg_def dom_char cod_char commutativities
            chine_composite' C.comp_assoc
      by auto

    lemma commutativities':
    shows "ν.cod.leg0  ν.chine  doms.Prj10 = π.cod.leg1  π.chine  doms.Prj00"
    and "μ.cod.leg0  μ.chine  doms.Prj1 =
         (ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]) 
           ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00"
    proof -
      have AB: "μ.dom.leg0  doms.Prj1 = ν.dom.leg1  doms.Prj10"
        using C.pullback_commutes' dom_char cod_char μν.legs_form_cospan νπ.legs_form_cospan
              C.comp_assoc
        by auto
      have BC: "ν.dom.leg0  doms.Prj10 = π.dom.leg1  doms.Prj00"
      proof -
        have "ν.dom.leg0  doms.Prj10 =
              (ν.dom.leg0  𝗉1[ν.dom.leg0, π.dom.leg1]) 
                 𝗉0[μ.dom.leg0, ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1]]"
          using dom_char μν.legs_form_cospan νπ.legs_form_cospan C.comp_assoc by simp
        also have "... = π.dom.leg1  doms.Prj00"
          using C.pullback_commutes' dom_char μν.legs_form_cospan νπ.legs_form_cospan C.comp_assoc
          by simp
        finally show ?thesis by auto
      qed
      show 1: "ν.cod.leg0  ν.chine  doms.Prj10 = π.cod.leg1  π.chine  doms.Prj00"
        using BC C.comp_assoc [of ν.cod.leg0 ν.chine doms.Prj10]
              C.comp_assoc [of π.cod.leg1 π.chine doms.Prj00]
              doms.prj_in_hom(5-6) dom_char
         by force
      show "μ.cod.leg0  μ.chine  doms.Prj1 =
            (ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]) 
              ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00"
      proof -
        have "(ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]) 
                ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00 =
              ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1] 
                ν.chine  doms.Prj10 ν.cod.leg0, π.cod.leg1 π.chine  doms.Prj00"
          using 1 μν.composable νπ.composable src_def trg_def dom_char C.comp_assoc by simp
        also have "... = ν.cod.leg1  ν.chine  doms.Prj10"
          using 1 dom_char μν.composable νπ.composable src_def trg_def
          by simp
        also have "... = (ν.cod.leg1  ν.chine)  doms.Prj10"
          using C.comp_assoc [of ν.cod.leg1 ν.chine doms.Prj10] by auto
        also have "... = (μ.cod.leg0  μ.chine)  doms.Prj1"
          using AB by simp
        also have "... = μ.cod.leg0  μ.chine  doms.Prj1"
          using C.comp_assoc [of μ.cod.leg0 μ.chine doms.Prj1] doms.prj_in_hom(4) dom_char
          by auto
        finally show ?thesis by simp
      qed
    qed

    lemma prj'_chine_composite:
    shows "cods.Prj1  μνπ.chine = μ.chine  doms.Prj1"
    and "cods.Prj10  μνπ.chine = ν.chine  doms.Prj10"
    and "cods.Prj00  μνπ.chine = π.chine  doms.Prj00"
      using μν.composable νπ.composable src_def trg_def dom_char cod_char commutativities'
            chine_composite' C.comp_assoc
      by auto

    lemma chine_assoc_naturality:
    shows "cods.chine_assoc  μν_π.chine = μνπ.chine  doms.chine_assoc"
    proof -
      have "«cods.chine_assoc  μν_π.chine :
               Chn ((dom μ  dom ν)  dom π) C Chn (cod μ  cod ν  cod π)»"
        using cods.chine_assoc_props(1) chine_composite_in_hom(1) by blast
      moreover have "«μνπ.chine  doms.chine_assoc :
                        Chn ((dom μ  dom ν)  dom π) C Chn (cod μ  cod ν  cod π)»"
        using doms.chine_assoc_props(1) chine_composite_in_hom(2) by blast
      moreover
      have "cods.Prj1  cods.chine_assoc  μν_π.chine =
            cods.Prj1  μνπ.chine  doms.chine_assoc"
        using C.comp_assoc doms.chine_assoc_props(2) cods.chine_assoc_props(2)
              prj_chine_composite prj'_chine_composite
        by metis
      moreover have "cods.Prj10  cods.chine_assoc  μν_π.chine =
                     cods.Prj10  μνπ.chine  doms.chine_assoc"
        using C.comp_assoc doms.chine_assoc_props(3) cods.chine_assoc_props(3)
              prj_chine_composite prj'_chine_composite
        by metis
      moreover have "cods.Prj00  cods.chine_assoc  μν_π.chine =
                     cods.Prj00  μνπ.chine  doms.chine_assoc"
        using C.comp_assoc doms.chine_assoc_props(4) cods.chine_assoc_props(4)
              prj_chine_composite prj'_chine_composite
        by metis
      ultimately show ?thesis
        using cods.prj'_joint_monic by auto
    qed

  end

  context span_bicategory
  begin

    abbreviation (input) assocSB
    where "assocSB f g h  Chn = three_composable_identity_arrows_of_spans.chine_assoc
                                   C prj0 prj1 f g h,
                            Dom = Dom ((f  g)  h), Cod = Cod (f  g  h)"

    abbreviation (input) assoc'SB
    where "assoc'SB f g h  Chn = three_composable_identity_arrows_of_spans.chine_assoc'
                                    C prj0 prj1 f g h,
                             Dom = Cod (f  g  h), Cod = Dom ((f  g)  h)"

    lemma assoc_props:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "src (assocSB f g h) = src h" and "trg (assocSB f g h) = trg f"
    and "«assocSB f g h : (f  g)  h  f  g  h»"
    and "src (assoc'SB f g h) = src h" and "trg (assoc'SB f g h) = trg f"
    and "«assoc'SB f g h : f  g  h  (f  g)  h»"
    proof -
      have fgh: "VVV.ide (f, g, h)"
        using assms VVV.ide_charSbC VV.ide_charSbC VVV.arr_charSbC VV.arr_charSbC by simp
      interpret f: arrow_of_spans C f
        using assms arr_char by fastforce
      interpret g: arrow_of_spans C g
        using assms arr_char by fastforce
      interpret h: arrow_of_spans C h
        using assms arr_char by fastforce
      interpret fgh: three_composable_arrows_of_spans C prj0 prj1 f g h
        using assms arr_char by (unfold_locales, auto)
      interpret fgh: three_composable_identity_arrows_of_spans C prj0 prj1 f g h
        using assms ide_char by (unfold_locales, auto)
      interpret HHfgh: arrow_of_spans C (f  g)  h
        using assms fgh.composites_are_arrows arrow_of_spans_hcomp by simp
      interpret HfHgh: arrow_of_spans C f  g  h
        using assms fgh.composites_are_arrows arrow_of_spans_hcomp by simp
      interpret assoc_fgh: arrow_of_spans C assocSB f g h
        apply unfold_locales
            apply simp_all
          apply (metis C.ideD(2) C.ideD(3) HHfgh.chine_simps(2) HfHgh.chine_simps(3)
            fgh.composites_are_identities(1) fgh.composites_are_identities(2)
            fgh.chine_assoc_in_hom ide_char)
        apply (metis C.comp_assoc fgh.composites_are_identities(1) fgh.leg0_composite(1-2)
                     fgh.prj_chine_assoc(3) ide_char' identity_arrow_of_spans.cod_simps(2))
        by (metis C.comp_assoc fgh.composites_are_identities(1) fgh.leg1_composite(1-2)
            fgh.prj_chine_assoc(1) ide_char' identity_arrow_of_spans.cod_simps(3))
      interpret assoc'_fgh: arrow_of_spans C assoc'SB f g h
        apply unfold_locales
            apply simp_all
          apply (metis C.ideD(2) C.ideD(3) HHfgh.chine_simps(2) HfHgh.chine_simps(3)
            fgh.composites_are_identities(1) fgh.composites_are_identities(2)
            fgh.chine_assoc'_in_hom ide_char)
        using C.comp_assoc fgh.composites_are_identities(1) fgh.leg0_composite(1-2)
              ide_char' identity_arrow_of_spans.cod_simps(2)
         apply force
        using C.comp_assoc fgh.composites_are_identities(1) fgh.leg1_composite(1-2)
              fgh.prj_chine_assoc'(1) ide_char' identity_arrow_of_spans.cod_simps(3)
        by force
      show 1: "«assocSB f g h : (f  g)  h  f  g  h»"
      proof
        show 1: "arr (assocSB f g h)"
          using assoc_fgh.arrow_of_spans_axioms arr_char by blast
        show "dom (assocSB f g h) = (f  g)  h"
          using fgh 1 dom_char fgh.μν.composable fgh.νπ.composable ideD(2)
          by auto
        show "cod (assocSB f g h) = f  g  h"
          using fgh 1 HoVH_def cod_char fgh.μν.composable fgh.νπ.composable ideD(3)
          by auto
      qed
      show 2: "«assoc'SB f g h : f  g  h  (f  g)  h»"
      proof
        show 1: "arr (assoc'SB f g h)"
          using assoc'_fgh.arrow_of_spans_axioms arr_char by blast
        show "dom (assoc'SB f g h) = f  g  h"
          using fgh 1 dom_char cod_char ideD(3) by auto
        show "cod (assoc'SB f g h) = (f  g)  h"
          using fgh 1 cod_char dom_char ideD(2) by auto            
      qed
      show 3: "src (assocSB f g h) = src h"
      proof -
        have 4: "src (assocSB f g h) =
                 Chn = assoc_fgh.dsrc, Dom = Leg0 = assoc_fgh.dsrc, Leg1 = assoc_fgh.dsrc,
                  Cod = Leg0 = assoc_fgh.dsrc, Leg1 = assoc_fgh.dsrc"
          unfolding src_def using 1 by auto
        also have "... = src h"
          using fgh.composite_simps(2) src_def by auto
        finally show ?thesis by blast
      qed
      show "src (assoc'SB f g h) = src h"
      proof -
        have "src (assoc'SB f g h) =
              Chn = assoc'_fgh.dsrc, Dom = Leg0 = assoc'_fgh.dsrc, Leg1 = assoc'_fgh.dsrc,
               Cod = Leg0 = assoc'_fgh.dsrc, Leg1 = assoc'_fgh.dsrc"
          unfolding src_def using 2 by auto
        also have "... = src h"
          using 1 3 assoc_fgh.cod_src_eq_dom_src arrI src_def by auto
        finally show ?thesis by blast
      qed
      show 4: "trg (assocSB f g h) = trg f"
      proof -
        have 5: "trg (assocSB f g h) =
              Chn = assoc_fgh.dtrg, Dom = Leg0 = assoc_fgh.dtrg, Leg1 = assoc_fgh.dtrg,
               Cod = Leg0 = assoc_fgh.dtrg, Leg1 = assoc_fgh.dtrg"
          unfolding trg_def using 1 by auto
        also have "... = trg f"
          using fgh.composite_simps(4) trg_def by auto
        finally show ?thesis by blast
      qed
      show "trg (assoc'SB f g h) = trg f"
      proof -
        have 5: "trg (assoc'SB f g h) =
              Chn = assoc'_fgh.dtrg, Dom = Leg0 = assoc'_fgh.dtrg, Leg1 = assoc'_fgh.dtrg,
               Cod = Leg0 = assoc'_fgh.dtrg, Leg1 = assoc'_fgh.dtrg"
          unfolding trg_def using 2 by auto
        also have "... = trg f"
          using 1 4 assoc_fgh.cod_trg_eq_dom_trg arrI trg_def by auto
        finally show ?thesis by blast
      qed
    qed

    lemma assoc_in_hom [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "«assocSB f g h : (f  g)  h  f  g  h» "
      using assms assoc_props by auto

    lemma assoc'_in_hom [intro]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "«assoc'SB f g h : f  g  h  (f  g)  h» "
      using assms assoc_props by auto

    lemma assoc_simps [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "arr (assocSB f g h)" and "dom (assocSB f g h) = (f  g)  h"
    and "cod (assocSB f g h) = f  g  h"
    and "src (assocSB f g h) = src h" and "trg (assocSB f g h) = trg f"
      using assms assoc_props(1-3) by (fast, fast, fast, auto)

    lemma assoc'_simps [simp]:
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "arr (assoc'SB f g h)" and "dom (assoc'SB f g h) = f  g  h"
    and "cod (assoc'SB f g h) = (f  g)  h"
    and "src (assoc'SB f g h) = src h" and "trg (assoc'SB f g h) = trg f"
      using assms assoc_props(4-6) by (fast, fast, fast, auto)

    lemma inverse_assoc_assoc':
    assumes "ide f" and "ide g" and "ide h" and "src f = trg g" and "src g = trg h"
    shows "inverse_arrows (assocSB f g h) (assoc'SB f g h)"
    proof -
      interpret f: arrow_of_spans C f using assms arr_char ideD(1) by simp
      interpret g: arrow_of_spans C g using assms arr_char ideD(1) by simp
      interpret h: arrow_of_spans C h using assms arr_char ideD(1) by simp
      interpret fgh: three_composable_arrows_of_spans C prj0 prj1 f g h
        using assms arr_char by (unfold_locales, auto)
      interpret fgh: three_composable_identity_arrows_of_spans C prj0 prj1 f g h
        using assms ide_char
        by unfold_locales blast+
      interpret afgh: arrow_of_spans C assocSB f g h
        using assms assoc_props(3) arr_char by blast
      interpret a'fgh: arrow_of_spans C assoc'SB f g h
        using assms assoc_props(6) arr_char by blast
      show ?thesis
      proof -
        have "inverse_arrows (assocSB f g h)
                             Chn = C.inv (Chn (assocSB f g h)),
                              Dom = Cod (assocSB f g h), Cod = Dom (assocSB f g h)"
          using inverse_arrows [of "assocSB f g h"] afgh.arrow_of_spans_axioms
                arr_char fgh.chine_assoc_inverse
          by auto
        moreover have "C.inv (Chn (assocSB f g h)) = fgh.chine_assoc'"
          using fgh.chine_assoc_inverse C.inv_is_inverse C.inverse_arrow_unique by auto
        ultimately show ?thesis by simp
      qed
    qed

    interpretation α: transformation_by_components VVV.comp vcomp HoHV HoVH
                        λfgh. assocSB (fst fgh) (fst (snd fgh)) (snd (snd fgh))
    proof
      show *: "fgh. VVV.ide fgh  «assocSB (fst fgh) (fst (snd fgh)) (snd (snd fgh)) :
                                         HoHV fgh  HoVH fgh»"
      proof -
        fix fgh
        assume fgh: "VVV.ide fgh"
        show "«assocSB (fst fgh) (fst (snd fgh)) (snd (snd fgh)) : HoHV fgh  HoVH fgh»"
          unfolding HoHV_def HoVH_def
          using fgh assoc_in_hom [of "fst fgh" "fst (snd fgh)" "snd (snd fgh)"]
                VVV.arr_charSbC VVV.ide_charSbC VV.arr_charSbC
          by simp
      qed
      show "μνπ. VVV.arr μνπ 
                     assocSB (fst (VVV.cod μνπ)) (fst (snd (VVV.cod μνπ)))
                             (snd (snd (VVV.cod μνπ))) 
                       HoHV μνπ =
                     HoVH μνπ  assocSB (fst (VVV.dom μνπ)) (fst (snd (VVV.dom μνπ)))
                                        (snd (snd (VVV.dom μνπ)))"
      proof -
        fix μνπ
        assume μνπ: "VVV.arr μνπ"
        interpret μ: arrow_of_spans C fst μνπ
          using μνπ VVV.ide_char VVV.arr_charSbC arr_char by auto
        interpret ν: arrow_of_spans C fst (snd μνπ)
          using μνπ VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char by auto
        interpret π: arrow_of_spans C snd (snd μνπ)
          using μνπ VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char by auto
        interpret μνπ: three_composable_arrows_of_spans C prj0 prj1
                         fst μνπ fst (snd μνπ) snd (snd μνπ)
          using μνπ VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char
          by (unfold_locales, auto)

        interpret HoHV_μνπ: arrow_of_spans C (fst μνπ  fst (snd μνπ))  snd (snd μνπ)
        proof -
          have "arr (HoHV μνπ)"
            using μνπ by simp
          thus "arrow_of_spans C ((fst μνπ  fst (snd μνπ))  snd (snd μνπ))"
            using μνπ HoHV_def arr_char by auto
        qed
        interpret HoVH_μνπ: arrow_of_spans C fst μνπ  fst (snd μνπ)  snd (snd μνπ)
        proof -
          have "arr (HoVH μνπ)"
            using μνπ by simp
          thus "arrow_of_spans C (fst μνπ  fst (snd μνπ)  snd (snd μνπ))"
            using μνπ HoVH_def arr_char by auto
        qed

        have dom_μνπ: "VVV.ide (VVV.dom μνπ)"
          using μνπ VVV.ide_dom by blast
        interpret dom_μ: identity_arrow_of_spans C fst (VVV.dom μνπ)
          using dom_μνπ VVV.ide_charSbC ide_char' by blast
        interpret dom_ν: identity_arrow_of_spans C fst (snd (VVV.dom μνπ))
          using dom_μνπ VVV.ide_charSbC ide_char' by blast
        interpret dom_π: identity_arrow_of_spans C snd (snd (VVV.dom μνπ))
          using dom_μνπ VVV.ide_charSbC ide_char' by blast
        interpret dom_μνπ: three_composable_identity_arrows_of_spans C prj0 prj1
                             fst (VVV.dom μνπ) fst (snd (VVV.dom μνπ))
                             snd (snd (VVV.dom μνπ))
          using dom_μνπ VVV.ide_char VVV.arr_charSbC VV.arr_charSbC
          by (unfold_locales, auto)
        interpret assoc_dom_μνπ: arrow_of_spans C
                                  assocSB (fst (VVV.dom μνπ)) (fst (snd (VVV.dom μνπ)))
                                    (snd (snd (VVV.dom μνπ)))
          using μνπ VVV.ide_dom * arr_char by fast

        have cod_μνπ: "VVV.ide (VVV.cod μνπ)"
          using μνπ VVV.ide_cod by blast
        interpret cod_μ: identity_arrow_of_spans C fst (VVV.cod μνπ)
          using cod_μνπ VVV.ide_charSbC ide_char' by blast
        interpret cod_ν: identity_arrow_of_spans C fst (snd (VVV.cod μνπ))
          using cod_μνπ VVV.ide_charSbC ide_char' by blast
        interpret cod_π: identity_arrow_of_spans C snd (snd (VVV.cod μνπ))
          using cod_μνπ VVV.ide_charSbC ide_char' by blast
        interpret cod_μνπ: three_composable_identity_arrows_of_spans C prj0 prj1
                             fst (VVV.cod μνπ) fst (snd (VVV.cod μνπ))
                             snd (snd (VVV.cod μνπ))
          using cod_μνπ VVV.ide_char VVV.arr_charSbC VV.arr_charSbC
          by (unfold_locales, auto)
        interpret assoc_cod_μνπ: arrow_of_spans C
                               assocSB (fst (VVV.cod μνπ)) (fst (snd (VVV.cod μνπ)))
                                  (snd (snd (VVV.cod μνπ)))
          using μνπ VVV.ide_cod * arr_char by fast

        have dom_legs:
               "dom_μ.leg0 = μ.dom.leg0  dom_ν.leg0 = ν.dom.leg0  dom_π.leg0 = π.dom.leg0 
                dom_μ.leg1 = μ.dom.leg1  dom_ν.leg1 = ν.dom.leg1  dom_π.leg1 = π.dom.leg1"
          using VVV.arr_charSbC VVV.dom_charSbC dom_char μνπ.μν.composable μνπ.νπ.composable
          by auto
        have cod_legs:
                "cod_μ.leg0 = μ.cod.leg0  cod_ν.leg0 = ν.cod.leg0  cod_π.leg0 = π.cod.leg0 
                 cod_μ.leg1 = μ.cod.leg1  cod_ν.leg1 = ν.cod.leg1  cod_π.leg1 = π.cod.leg1"
          using μνπ VVV.cod_charSbC cod_char by auto

        have Prj11_dom: "dom_μνπ.Prj11 =
                          𝗉1[μ.dom.leg0, ν.dom.leg1] 
                            𝗉1[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
          using dom_legs by argo
        have Prj11_cod: "cod_μνπ.Prj11 =
                          𝗉1[μ.cod.leg0, ν.cod.leg1] 
                            𝗉1[ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1]"
          using cod_legs by argo
        have Prj0_dom: "dom_μνπ.Prj0 = 𝗉0[ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1], π.dom.leg1]"
          using dom_legs by argo
        have Prj0_cod: "cod_μνπ.Prj0 = 𝗉0[ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1]"
          using cod_legs by argo

        have Dom: "Dom ((fst (VVV.dom μνπ)  fst (snd (VVV.dom μνπ))) 
                         snd (snd (VVV.dom μνπ))) =
                   Leg0 = π.dom.leg0  dom_μνπ.Prj0, Leg1 = μ.dom.leg1  dom_μνπ.Prj11"
          using dom_μνπ.leg0_composite(2) dom_μνπ.leg1_composite(2) dom_legs by auto
        have Cod: "Cod (fst (VVV.dom μνπ)  fst (snd (VVV.dom μνπ)) 
                         snd (snd (VVV.dom μνπ))) =
                   Leg0 = π.dom.leg0  dom_μνπ.Prj00, Leg1 = μ.dom.leg1  dom_μνπ.Prj1"
        proof -
            have "arr (dom (fst (snd μνπ))  dom (snd (snd μνπ)))"
              using μνπ.μν.composable μνπ.νπ.composable by simp
            thus ?thesis
              using μνπ hcomp_def dom_legs ide_dom dom_char
                apply simp
              using μνπ.μν.composable μνπ.νπ.composable src_def trg_def dom_char C.comp_assoc
                    VVV.dom_simp VV.dom_simp
              by auto
        qed
        have Dom': "Dom ((fst (VVV.cod μνπ)  fst (snd (VVV.cod μνπ))) 
                          snd (snd (VVV.cod μνπ))) =
                    Leg0 = π.cod.leg0  cod_μνπ.Prj0, Leg1 = μ.cod.leg1  cod_μνπ.Prj11"
          by (simp add: cod_μνπ.leg0_composite(2) cod_μνπ.leg1_composite(2) cod_legs)
        have Cod': "Cod (fst (VVV.cod μνπ)  fst (snd (VVV.cod μνπ)) 
                          snd (snd (VVV.cod μνπ))) =
                    Leg0 = π.cod.leg0  cod_μνπ.Prj00, Leg1 = μ.cod.leg1  cod_μνπ.Prj1"
        proof -
            have "arr (cod (fst (snd μνπ))  cod (snd (snd μνπ)))"
              using μνπ.μν.composable μνπ.νπ.composable by simp
            moreover have "μ.dsrc = ν.dtrg"
              using μνπ.μν.composable src_def trg_def cod_char by simp
            ultimately show ?thesis
              using μνπ hcomp_def cod_legs ide_cod cod_char VVV.cod_simp VV.cod_simp
                apply simp
              using μνπ.μν.composable μνπ.νπ.composable src_def trg_def cod_char C.comp_assoc
              by auto
        qed

        have assoc_dom:
             "assocSB (fst (VVV.dom μνπ)) (fst (snd (VVV.dom μνπ)))
                      (snd (snd (VVV.dom μνπ))) =
              Chn = dom_μνπ.chine_assoc,
               Dom = Leg0 = π.dom.leg0  dom_μνπ.Prj0, Leg1 = μ.dom.leg1  dom_μνπ.Prj11,
               Cod = Leg0 = π.dom.leg0  dom_μνπ.Prj00, Leg1 = μ.dom.leg1  dom_μνπ.Prj1"
          using Dom Cod by simp
        have assoc_cod:
             "assocSB (fst (VVV.cod μνπ)) (fst (snd (VVV.cod μνπ)))
                     (snd (snd (VVV.cod μνπ))) =
              Chn = cod_μνπ.chine_assoc,
               Dom = Leg0 = π.cod.leg0  cod_μνπ.Prj0, Leg1 = μ.cod.leg1  cod_μνπ.Prj11,
               Cod = Leg0 = π.cod.leg0  cod_μνπ.Prj00, Leg1 = μ.cod.leg1  cod_μνπ.Prj1"
          using Dom' Cod' by simp
        have HoHV_μνπ:
          "HoHV μνπ =
           Chn = HoHV_μνπ.chine,
            Dom = Leg0 = π.dom.leg0  dom_μνπ.Prj0, Leg1 = μ.dom.leg1  dom_μνπ.Prj11,
            Cod = Leg0 = π.cod.leg0  cod_μνπ.Prj0, Leg1 = μ.cod.leg1  cod_μνπ.Prj11"
        proof -
          have "arr Chn = μ.chine  𝗉1[μ.dom.leg0, ν.dom.leg1]
                              μ.cod.leg0, ν.cod.leg1
                            ν.chine  𝗉0[μ.dom.leg0, ν.dom.leg1],
                     Dom = Leg0 = ν.dom.leg0  𝗉0[μ.dom.leg0, ν.dom.leg1],
                            Leg1 = μ.dom.leg1  𝗉1[μ.dom.leg0, ν.dom.leg1],
                     Cod = Leg0 = ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1],
                            Leg1 = μ.cod.leg1  𝗉1[μ.cod.leg0, ν.cod.leg1]"
            unfolding hcomp_def chine_hcomp_def
            using μνπ hcomp_def dom_legs cod_legs ide_dom ide_cod dom_char cod_char
                  μνπ.μν.composable
            by (metis (no_types, lifting) hseq_char(1) μνπ.μν.composite_is_arrow chine_hcomp_def)
          moreover have "(μ.cod.leg1  𝗉1[μ.cod.leg0, ν.cod.leg1]) 
                           𝗉1[ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1] =
                          μ.cod.leg1  𝗉1[μ.cod.leg0, ν.cod.leg1] 
                           𝗉1[ν.cod.leg0  𝗉0[μ.cod.leg0, ν.cod.leg1], π.cod.leg1]"
           using C.comp_assoc by simp
          ultimately show ?thesis
            unfolding HoHV_def hcomp_def chine_hcomp_def
            using μνπ μνπ.μν.composable μνπ.νπ.composable src_def trg_def dom_legs cod_legs
                  C.comp_assoc
            by simp
        qed
        have HoVH_μνπ:
          "HoVH μνπ =
           Chn = HoVH_μνπ.chine,
            Dom = Leg0 = π.dom.leg0  dom_μνπ.Prj00, Leg1 = μ.dom.leg1  dom_μνπ.Prj1,
            Cod = Leg0 = π.cod.leg0  cod_μνπ.Prj00, Leg1 = μ.cod.leg1  cod_μνπ.Prj1"
        proof -
          have "arr Chn = ν.chine  𝗉1[ν.dom.leg0, π.dom.leg1]
                             ν.cod.leg0, π.cod.leg1
                            π.chine  𝗉0[ν.dom.leg0, π.dom.leg1],
                     Dom = Leg0 = π.dom.leg0  𝗉0[ν.dom.leg0, π.dom.leg1],
                            Leg1 = ν.dom.leg1  𝗉1[ν.dom.leg0, π.dom.leg1],
                     Cod = Leg0 = π.cod.leg0  𝗉0[ν.cod.leg0, π.cod.leg1],
                            Leg1 = ν.cod.leg1  𝗉1[ν.cod.leg0, π.cod.leg1]"
            unfolding hcomp_def chine_hcomp_def
            using μνπ hcomp_def dom_legs cod_legs ide_dom ide_cod dom_char cod_char
                  μνπ.νπ.composable
            by (metis (no_types, lifting) hseq_char μνπ.νπ.composite_is_arrow chine_hcomp_def)
         moreover have "(π.cod.leg0  𝗉0[ν.cod.leg0, π.cod.leg1])  𝗉0[μ.cod.leg0, ν.cod.leg1 
                          𝗉1[ν.cod.leg0, π.cod.leg1]] =
                         π.cod.leg0  𝗉0[ν.cod.leg0, π.cod.leg1]  𝗉0[μ.cod.leg0, ν.cod.leg1 
                           𝗉1[ν.cod.leg0, π.cod.leg1]]"
           using C.comp_assoc by simp
         ultimately show ?thesis
            unfolding HoVH_def hcomp_def chine_hcomp_def
            using μνπ μνπ.μν.composable μνπ.νπ.composable src_def trg_def dom_legs cod_legs
                  C.comp_assoc
            by simp
       qed
       have "assocSB (fst (VVV.cod μνπ)) (fst (snd (VVV.cod μνπ)))
                     (snd (snd (VVV.cod μνπ))) 
               HoHV μνπ =
             Chn = cod_μνπ.chine_assoc  HoHV_μνπ.chine,
              Dom = Leg0 = π.dom.leg0  dom_μνπ.Prj0, Leg1 = μ.dom.leg1  dom_μνπ.Prj11,
              Cod = Leg0 = π.cod.leg0  cod_μνπ.Prj00, Leg1 = μ.cod.leg1  cod_μνπ.Prj1"
        proof -
          have "arr (HoHV μνπ)"
            using μνπ by simp
          thus ?thesis
            using vcomp_def HoHV_μνπ HoHV_μνπ.arrow_of_spans_axioms
                  assoc_cod_μνπ.arrow_of_spans_axioms assoc_cod dom_legs cod_legs
                  arr_char
            by simp
        qed
        moreover
        have "HoVH μνπ 
                assocSB (fst (VVV.dom μνπ)) (fst (snd (VVV.dom μνπ)))
                        (snd (snd (VVV.dom μνπ))) =
              Chn = HoVH_μνπ.chine  dom_μνπ.chine_assoc,
               Dom = Leg0 = π.dom.leg0  dom_μνπ.Prj0, Leg1 = μ.dom.leg1  dom_μνπ.Prj11,
               Cod = Leg0 = π.cod.leg0  cod_μνπ.Prj00, Leg1 = μ.cod.leg1  cod_μνπ.Prj1"
        proof -
          have "arr (HoVH μνπ)"
            using μνπ by simp
          thus ?thesis
            using vcomp_def HoVH_μνπ HoVH_μνπ.arrow_of_spans_axioms
                  assoc_dom_μνπ.arrow_of_spans_axioms assoc_dom dom_legs cod_legs
                  arr_char
            by simp
        qed
        moreover
        have "cod_μνπ.chine_assoc  HoHV_μνπ.chine = HoVH_μνπ.chine  dom_μνπ.chine_assoc"
          using μνπ HoHV_def HoVH_def μνπ.chine_assoc_naturality
                VVV.dom_simp VV.dom_simp VVV.cod_simp VV.cod_simp by simp
        ultimately show "assocSB (fst (VVV.cod μνπ)) (fst (snd (VVV.cod μνπ)))
                                 (snd (snd (VVV.cod μνπ))) 
                           HoHV μνπ =
                         HoVH μνπ 
                           assocSB (fst (VVV.dom μνπ)) (fst (snd (VVV.dom μνπ)))
                                   (snd (snd (VVV.dom μνπ)))"
          by argo
      qed
    qed

    definition assoc  ("𝖺[_, _, _]")
    where "assoc  λμ ν π. α.map (μ, ν, π)"

    abbreviation (input) αSB
    where "αSB  λμνπ. assoc (fst μνπ) (fst (snd μνπ)) (snd (snd μνπ))"

    lemma α_ide:
    assumes "ide f" and "ide g" and "ide h"
    and "src f = trg g" and "src g = trg h"
    shows "αSB (f, g, h) = assocSB f g h"
      using assms assoc_def α.map_simp_ide VVV.ide_charSbC VVV.arr_charSbC VV.ide_charSbC VV.arr_charSbC
      by simp

    lemma natural_transformation_α:
    shows "natural_transformation VVV.comp vcomp HoHV HoVH αSB"
      using assoc_def α.natural_transformation_axioms by auto

    interpretation α: natural_transformation VVV.comp vcomp HoHV HoVH αSB
      using natural_transformation_α by simp

    sublocale α: natural_isomorphism VVV.comp vcomp HoHV HoVH αSB
    proof
      show "fgh. VVV.ide fgh  iso (αSB fgh)"
      proof -
        fix fgh
        assume fgh: "VVV.ide fgh"
        interpret f: arrow_of_spans C fst fgh
          using fgh VVV.ide_char VVV.arr_charSbC arr_char by auto
        interpret g: arrow_of_spans C fst (snd fgh)
          using fgh VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char by auto
        interpret h: arrow_of_spans C snd (snd fgh)
          using fgh VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char by auto
        interpret fgh: three_composable_arrows_of_spans C prj0 prj1
                         fst fgh fst (snd fgh) snd (snd fgh)
          using fgh VVV.ide_char VVV.arr_charSbC VV.arr_charSbC arr_char
          by (unfold_locales, auto)
        interpret fgh: three_composable_identity_arrows_of_spans C prj0 prj1
                         fst fgh fst (snd fgh) snd (snd fgh)
          using fgh VVV.ide_charSbC ide_char
          by unfold_locales blast+
        have 1: "arr (αSB fgh)"
          using fgh α.preserves_reflects_arr VVV.ideD(1) by blast
        have 2: "αSB fgh = assocSB (fst fgh) (fst (snd fgh)) (snd (snd fgh))"
          using fgh assoc_def α_ide [of "fst fgh" "fst (snd fgh)" "snd (snd fgh)"]
                VVV.ide_charSbC VV.ide_charSbC VVV.arr_charSbC VV.arr_charSbC
          by simp
        moreover have "iso ..."
          using 1 2 iso_char [of "assocSB (fst fgh) (fst (snd fgh)) (snd (snd fgh))"]
                fgh.chine_assoc_inverse by auto
        ultimately show "iso (αSB fgh)" by argo
      qed
    qed

    lemma natural_isomorphism_α:
    shows "natural_isomorphism VVV.comp vcomp HoHV HoVH αSB"
      ..

  end

  locale four_composable_arrows_of_spans =
     span_bicategory +
  μ: arrow_of_spans C μ +
  ν: arrow_of_spans C ν +
  π: arrow_of_spans C π +
  ρ: arrow_of_spans C ρ +
  μν: two_composable_arrows_of_spans C prj0 prj1 μ ν +
  νπ: two_composable_arrows_of_spans C prj0 prj1 ν π +
  πρ: two_composable_arrows_of_spans C prj0 prj1 π ρ +
  μνπ: three_composable_arrows_of_spans C prj0 prj1 μ ν π +
  νπρ: three_composable_arrows_of_spans C prj0 prj1 ν π ρ
  for μ (structure)
  and ν (structure)
  and π (structure)
  and ρ (structure)

  locale four_composable_identity_arrows_of_spans =
    four_composable_arrows_of_spans +
  μ: identity_arrow_of_spans C μ +
  ν: identity_arrow_of_spans C ν +
  π: identity_arrow_of_spans C π +
  ρ: identity_arrow_of_spans C ρ +
  μν: two_composable_identity_arrows_of_spans C prj0 prj1 μ ν +
  νπ: two_composable_identity_arrows_of_spans C prj0 prj1 ν π +
  πρ: two_composable_identity_arrows_of_spans C prj0 prj1 π ρ +
  μνπ: three_composable_identity_arrows_of_spans C prj0 prj1 μ ν π +
  νπρ: three_composable_identity_arrows_of_spans C prj0 prj1 ν π ρ
  begin

    interpretation H: horizontal_composition vcomp hcomp src trg
      using has_horizontal_composition by auto

    text ‹
      The following interpretations provide us with some systematic names
      for a lot of things.
    ›

    interpretation HμHνπ: identity_arrow_of_spans C μ  ν  π
      using μνπ.composites_are_identities ide_char' by auto
    interpretation HHμνπ: identity_arrow_of_spans C (μ  ν)  π
      using μνπ.composites_are_identities ide_char' by auto
    interpretation HνHπρ: identity_arrow_of_spans C ν  π  ρ
      using νπρ.composites_are_identities ide_char' by auto
    interpretation HHνπρ: identity_arrow_of_spans C (ν  π)  ρ
      using νπρ.composites_are_identities ide_char' by auto

    interpretation HμHνHπρ: arrow_of_spans C μ  ν  π  ρ
      using arrow_of_spans_hcomp μν.composable νπρ.composites_are_arrows(1) by auto
    interpretation HμHHνπρ: arrow_of_spans C μ  (ν  π)  ρ
      using arrow_of_spans_hcomp μν.composable νπρ.composites_are_arrows(1) by auto
    interpretation HHμνHπρ: arrow_of_spans C (μ  ν)  π  ρ
      using hseq_char' match_4 μνπ.composites_are_arrows(2) πρ.composite_is_arrow arr_char
      by auto
    interpretation HHμHνπρ: arrow_of_spans C (μ  ν  π)  ρ
      using arrow_of_spans_hcomp πρ.composable μνπ.composites_are_arrows(1) by auto
    interpretation HHHμνπρ: arrow_of_spans C ((μ  ν)  π)  ρ
      using arrow_of_spans_hcomp πρ.composable μνπ.composites_are_arrows(2) by auto

    interpretation assocμνπ: arrow_of_spans C assocSB μ ν π
      using arr_char μν.composable νπ.composable assoc_simps(1) by auto
    interpretation assocνπρ: arrow_of_spans C assocSB ν π ρ
      using arr_char νπ.composable πρ.composable assoc_simps(1) by auto

    interpretation μ_νπ: two_composable_identity_arrows_of_spans C prj0 prj1 μ ν  π
      using μν.composable νπ.composable by (unfold_locales, auto)
    interpretation μν_π: two_composable_identity_arrows_of_spans C prj0 prj1 μ  ν π
      using μν.composable νπ.composable by (unfold_locales, auto)
    interpretation ν_πρ: two_composable_identity_arrows_of_spans C prj0 prj1 ν π  ρ
      using νπ.composable πρ.composable by (unfold_locales, auto)
    interpretation νπ_ρ: two_composable_identity_arrows_of_spans C prj0 prj1 ν  π ρ
      using νπ.composable πρ.composable by (unfold_locales, auto)
    (* The two other cases, μνπ and νπρ, are part of the locale assumptions. *)

    interpretation μ_νπ_ρ: three_composable_identity_arrows_of_spans C prj0 prj1 μ ν  π ρ ..
    interpretation μ_ν_πρ: three_composable_identity_arrows_of_spans C prj0 prj1 μ ν π  ρ ..
    interpretation μν_π_ρ: three_composable_identity_arrows_of_spans C prj0 prj1 μ  ν π ρ ..

    lemma chines_eq:
    shows "HμHHνπρ.chine = μ.leg0 ↓↓ HHνπρ.leg1"
    and "HHμHνπρ.chine = assocμνπ.cod.leg0 ↓↓ ρ.leg1"
    and "HμHνHπρ.chine = μ.leg0 ↓↓ HνHπρ.leg1"
    proof -
      show "HμHHνπρ.chine = μ.leg0 ↓↓ HHνπρ.leg1"
        using hcomp_def [of μ "hcomp (hcomp ν π) ρ"] chine_hcomp_ide_ide μν.composable
        by simp
      show "HHμHνπρ.chine = assocμνπ.cod.leg0 ↓↓ ρ.leg1"
        by (simp add: μ_νπ.leg0_composite μ_νπ_ρ.chine_composite(1))
      show "HμHνHπρ.chine = μ.leg0 ↓↓ HνHπρ.leg1"
        using hcomp_def [of μ "hcomp ν (hcomp π ρ)"] chine_hcomp_ide_ide μν.composable
        by simp
    qed

    lemma cospan_μ0_HνHπρ1:
    shows "C.cospan μ.leg0 HνHπρ.leg1"
      by (metis C.cod_comp HνHπρ.dom.leg_simps(3) μ_ν_πρ.cospan_μν νπρ.leg1_composite(1))
 
    (* TODO: Better name for this. *)
    lemma assoc_in_homs:
    shows "«μ  (assocSB ν π ρ) : μ  (ν  π)  ρ  μ  ν  π  ρ»"
    and "«assocSB μ (ν  π) ρ : (μ  ν  π)  ρ  μ  (ν  π)  ρ»"
    and "«assocSB μ ν π  ρ : ((μ  ν)  π)  ρ  (μ  ν  π)  ρ»"
    and "«assocSB μ ν (π  ρ) : (μ  ν)  π  ρ  μ  ν  π  ρ»"
    and "«assocSB (μ  ν) π ρ : ((μ  ν)  π)  ρ  (μ  ν)  π  ρ»"
    proof -
      show "«μ  (assocSB ν π ρ) : μ  (ν  π)  ρ  μ  ν  π  ρ»"
        using μν.composable νπ.composable πρ.composable by auto
      show "«assocSB μ (ν  π) ρ : (μ  ν  π)  ρ  μ  (ν  π)  ρ»"
        using assoc_in_hom μν.composable νπ.composable πρ.composable by simp
      show "«assocSB μ ν π  ρ : ((μ  ν)  π)  ρ  (μ  ν  π)  ρ»"
        using μν.composable νπ.composable πρ.composable by auto
      show "«assocSB μ ν (π  ρ) : (μ  ν)  π  ρ  μ  ν  π  ρ»"
        using μν.composable νπ.composable πρ.composable
        by auto
      show "«assocSB (μ  ν) π ρ : ((μ  ν)  π)  ρ  (μ  ν)  π  ρ»"
        using μν.composable νπ.composable πρ.composable by auto
    qed

    lemma chine_composites:
    shows "Chn (μ  assocSB ν π ρ) = chine_hcomp μ (assocSB ν π ρ)"
    and "Chn (assocSB μ (ν  π) ρ) = μ_νπ_ρ.chine_assoc"
    and "Chn (assocSB μ ν π  ρ) = chine_hcomp (assocSB μ ν π) ρ"
    and "Chn (assocSB μ ν (π  ρ)) = μ_ν_πρ.chine_assoc"
    and "Chn (assocSB (μ  ν) π ρ) = μν_π_ρ.chine_assoc"
    proof -
      show "Chn (μ  assocSB ν π ρ) = chine_hcomp μ (assocSB ν π ρ)"
        using hcomp_def [of μ "assocSB ν π ρ"] chine_hcomp_def [of μ "assocSB ν π ρ"]
              μν.composable νπ.composable πρ.composable
        by auto
      show "Chn (assocSB μ ν π  ρ) = chine_hcomp (assocSB μ ν π) ρ"
        using assoc_in_homs(2-3) hcomp_def
        by (metis arrI arrow_of_spans_data.select_convs(1) hseqE)
      show "Chn (assocSB μ (ν  π) ρ) = μ_νπ_ρ.chine_assoc"
        using hcomp_def
        by (meson arrow_of_spans_data.select_convs(1))
      show "Chn (assocSB μ ν (π  ρ)) = μ_ν_πρ.chine_assoc"
        using hcomp_def
        by (meson arrow_of_spans_data.select_convs(1))
      show "Chn (assocSB (μ  ν) π ρ) = μν_π_ρ.chine_assoc"
        using hcomp_def
        by (meson arrow_of_spans_data.select_convs(1))
    qed

    lemma prj_in_homs [intro, simp]:
    shows "«𝗉0[μ.leg0, HHνπρ.leg1] : HμHHνπρ.chine C HHνπρ.chine»"
    and "«𝗉1[μ.leg0, HνHπρ.leg1] : HμHνHπρ.chine C μ.apex»"
    and "«𝗉1[assocμνπ.cod.leg0, ρ.cod.leg1] : HHμHνπρ.chine C HμHνπ.chine»"
    and "«𝗉0[HHμνπ.leg0, ρ.leg1] : HHHμνπρ.chine C ρ.chine»"
    and "«𝗉1[HHμνπ.leg0, ρ.leg1] : HHHμνπρ.chine C HHμνπ.chine»"
    and "«𝗉1[νπ.leg0  μ_νπ.prj0, ρ.leg1] : HHμHνπρ.chine C HμHνπ.chine»"
    and "«𝗉1[assocμνπ.dom.leg0, ρ.leg1] : HHHμνπρ.chine C HHμνπ.chine»"
    and "«μ_νπ.prj0 : HμHνπ.chine C νπ.apex»"
    proof -
      show "«𝗉0[μ.leg0, HHνπρ.leg1] : HμHHνπρ.chine C HHνπρ.chine»"
        by (metis C.dom_comp C.prj0_in_hom' C.prj1_simps_arr HHνπρ.chine_eq_apex
            HHνπρ.cod.apex_def HHνπρ.cod.is_span HHνπρ.cod_simps(1) HHνπρ.cod_simps(3)
            μ_νπ_ρ.prj_simps(10) μ_νπ_ρ.prj_simps(11) μ_νπ_ρ.prj_simps(14) νπ_ρ.leg1_composite)
      show "«𝗉1[assocμνπ.cod.leg0, ρ.cod.leg1] : HHμHνπρ.chine C HμHνπ.chine»"
        using μνπ.leg0_composite(1) μν_π_ρ.prj_simps(3) μ_νπ.leg0_composite 
              μ_νπ_ρ.prj_simps(6)
        by auto
      show "«𝗉0[HHμνπ.leg0, ρ.leg1] : HHHμνπρ.chine C ρ.chine»"
        by (simp add: μν_π.leg0_composite μν_π_ρ.prj_in_hom(3))
      show "«𝗉1[HHμνπ.leg0, ρ.leg1] : HHHμνπρ.chine C HHμνπ.chine»"
        using μν.leg0_composite μν_π.leg0_composite μν_π_ρ.prj_in_hom(2) by fastforce
      show "«𝗉1[νπ.leg0  μ_νπ.prj0, ρ.leg1] : HHμHνπρ.chine C HμHνπ.chine»"
        using μνπ.leg0_composite(1) μ_νπ.leg0_composite μ_νπ_ρ.prj_simps(3)
              μ_νπ_ρ.prj_simps(6)
        by force
      show "«𝗉1[assocμνπ.dom.leg0, ρ.leg1] : HHHμνπρ.chine C HHμνπ.chine»"
        using «𝗉1[HHμνπ.leg0, ρ.leg1] : HHHμνπρ.chine C HHμνπ.chine» by fastforce
      show "«𝗉1[μ.leg0, HνHπρ.leg1] : HμHνHπρ.chine C μ.apex»"
        by (simp add: μ_ν_πρ.prj_in_hom(4) ν_πρ.leg1_composite)
      show "«μ_νπ.prj0 : HμHνπ.chine C νπ.apex»"
        using μ_νπ.chine_composite μ_νπ.prj_in_hom(2) by presburger
    qed

    lemma chine_in_homs [intro, simp]:
    shows "«assocμνπ.chine : HHμνπ.chine C HμHνπ.chine»"
    and "«assocνπρ.chine : HHνπρ.chine C HνHπρ.chine»"
    and "«chine_hcomp μ (assocSB ν π ρ) : HμHHνπρ.chine C HμHνHπρ.chine»"
    and "«chine_hcomp (assocSB μ ν π) ρ : HHHμνπρ.chine C HHμHνπρ.chine»"
    proof -
      show 1: "«assocμνπ.chine : HHμνπ.chine C HμHνπ.chine»"
        using μνπ.chine_assoc_in_hom by simp
      show "«assocνπρ.chine : HHνπρ.chine C HνHπρ.chine»"
        using νπρ.chine_assoc_in_hom by simp
      show "«chine_hcomp μ (assocSB ν π ρ) : HμHHνπρ.chine C HμHνHπρ.chine»"
        using Chn_in_hom by (metis assoc_in_homs(1) chine_composites(1))
      show "«chine_hcomp (assocSB μ ν π) ρ : HHHμνπρ.chine C HHμHνπρ.chine»"
        using Chn_in_hom by (metis assoc_in_homs(3) chine_composites(3))
    qed

    lemma commutative_squares [intro, simp]:
    shows "C.commutative_square νπ.leg0 ρ.leg1 μ_νπ_ρ.Prj01 μ_νπ_ρ.Prj0"
    and "C.commutative_square ν.leg0 πρ.leg1 μ_ν_πρ.Prj01 μ_ν_πρ.Prj0"
    and "C.commutative_square 𝗉0[μ.cod.leg0, assocνπρ.cod.leg1] assocνπρ.chine
            (chine_hcomp μ (assocSB ν π ρ)) 𝗉0[μ.leg0, assocνπρ.dom.leg1]"
    and "C.commutative_square 𝗉1[μ.cod.leg0, assocνπρ.cod.leg1] μ.chine
            (chine_hcomp μ (assocSB ν π ρ)) 𝗉1[μ.leg0, assocνπρ.dom.leg1]"
    and "C.commutative_square assocμνπ.cod.leg0 ρ.cod.leg1
            (assocμνπ.chine  𝗉1[assocμνπ.dom.leg0, ρ.leg1])
            (ρ.chine  𝗉0[assocμνπ.dom.leg0, ρ.leg1])"
    and "C.commutative_square μ.leg0 (νπ.leg1  νπ_ρ.prj1) μ_νπ_ρ.Prj11
             μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0"
    and "C.commutative_square μ.leg0 (ν.leg1  ν_πρ.prj1) μ_ν_πρ.Prj11
             μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0"
    proof -
      show 1: "C.commutative_square νπ.leg0 ρ.leg1 μ_νπ_ρ.Prj01 μ_νπ_ρ.Prj0"
      proof -
        have 1: "C.arr μ_νπ_ρ.Prj0  C.dom μ_νπ_ρ.Prj0 = HHμHνπρ.chine 
                 C.cod μ_νπ_ρ.Prj0 = ρ.apex"
          by (meson C.in_homE μ_νπ_ρ.prj_in_hom(3))
        hence "(νπ.leg0  μ_νπ.prj0)  𝗉1[νπ.leg0  μ_νπ.prj0, ρ.leg1] = ρ.leg1  μ_νπ_ρ.Prj0"
          by (meson C.prj0_simps_arr C.pullback_commutes')
        thus ?thesis
          using 1 C.comp_assoc νπ_ρ.legs_form_cospan(1) by simp
      qed
      show 2: "C.commutative_square ν.leg0 πρ.leg1 μ_ν_πρ.Prj01 μ_ν_πρ.Prj0"
      proof -
        have "ν.leg0  μν.prj0  𝗉1[ν.leg0  μν.prj0, πρ.leg1] =
              πρ.leg1  𝗉0[ν.leg0  μν.prj0, πρ.leg1]"
          by (metis (no_types) C.category_axioms C.prj0_simps_arr C.pullback_commutes'
              category.comp_reduce μ_ν_πρ.prj_simps(2) μ_ν_πρ.prj_simps(3))
        thus ?thesis
          using C.commutative_square_def μ_ν_πρ.cospan_νπ
            μ_ν_πρ.prj_simps(2) μ_ν_πρ.prj_simps(3) μ_ν_πρ.prj_simps(5) μ_ν_πρ.prj_simps(6)
            μ_ν_πρ.prj_simps(8) ν.dom.apex_def
          by presburger
      qed
      show "C.commutative_square 𝗉0[μ.cod.leg0, assocνπρ.cod.leg1] assocνπρ.chine
                  (chine_hcomp μ (assocSB ν π ρ)) 𝗉0[μ.leg0, assocνπρ.dom.leg1]"
        using assoc_in_homs(1) chine_hcomp_props(4) [of "assocSB ν π ρ" μ] hseq_char by blast
      show "C.commutative_square 𝗉1[μ.cod.leg0, assocνπρ.cod.leg1] μ.chine
                  (chine_hcomp μ (assocSB ν π ρ)) 𝗉1[μ.leg0, assocνπρ.dom.leg1]"
        using chine_hcomp_props(3) [of "assocSB ν π ρ" μ] hseq_char
              μν.composable νπ.composable πρ.composable
        by auto
      show "C.commutative_square assocμνπ.cod.leg0 ρ.cod.leg1
                  (assocμνπ.chine  𝗉1[assocμνπ.dom.leg0, ρ.leg1])
                  (ρ.chine  𝗉0[assocμνπ.dom.leg0, ρ.leg1])"
        using assoc_in_homs(3) hseq_char chine_hcomp_props(2) by blast
      show "C.commutative_square μ.leg0 (νπ.leg1  νπ_ρ.prj1) μ_νπ_ρ.Prj11
              μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0"
      proof
        show "C.cospan μ.leg0 (νπ.leg1  νπ_ρ.prj1)"
          using HHνπρ.dom.leg_simps(1) μ_νπ_ρ.cospan_μν C.arrI by fastforce
        show "C.span μ_νπ_ρ.Prj11 μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0"
          using 1 μ_νπ_ρ.prj_in_hom(1) by auto
        show "C.dom μ.leg0 = C.cod μ_νπ_ρ.Prj11"
          by simp
        show "μ.leg0  μ_νπ_ρ.Prj11 =
              (νπ.leg1  νπ_ρ.prj1)  μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0"
          by (metis (no_types, lifting) "1" C.comp_assoc C.prj_tuple(2) C.pullback_commutes'
              μ_νπ_ρ.cospan_μν)
      qed
      show "C.commutative_square μ.leg0 (ν.leg1  ν_πρ.prj1) μ_ν_πρ.Prj11
               μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0"
      proof
        show "C.cospan μ.leg0 (ν.leg1  ν_πρ.prj1)"
          using C.arrI μ_ν_πρ.prj_in_hom(4) by auto
        show "C.span μ_ν_πρ.Prj11 μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0"
          using 2 by fastforce
        thus "C.dom μ.leg0 = C.cod μ_ν_πρ.Prj11"
          using μ_ν_πρ.cospan_μν by simp
        show "μ.leg0  μ_ν_πρ.Prj11 =
              (ν.leg1  ν_πρ.prj1)  μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0"
          by (metis (no_types, lifting) "2" C.comp_assoc C.prj_tuple(2) C.pullback_commutes'
              μ_ν_πρ.cospan_μν)
      qed
    qed

    lemma chine_pentagon:
    shows "Chn ((μ  assocSB ν π ρ)  assocSB μ (ν  π) ρ  (assocSB μ ν π  ρ)) =
           Chn (assocSB μ ν (π  ρ)  assocSB (μ  ν) π ρ)"
    proof -
      let ?LHS = "(μ  assocSB ν π ρ)  assocSB μ (ν  π) ρ  (assocSB μ ν π  ρ)"
      let ?RHS = "assocSB μ ν (π  ρ)  assocSB (μ  ν) π ρ"

      have LHS_in_hom: "«?LHS : ((μ  ν)  π)  ρ  μ  ν  π  ρ»"
        using μν.composable νπ.composable πρ.composable by auto
      have RHS_in_hom: "«?RHS : ((μ  ν)  π)  ρ  μ  ν  π  ρ»"
        using μν.composable νπ.composable πρ.composable by auto

      have 1: "arrow_of_spans (⋅) ?LHS"
        using arr_char assoc_in_homs(1-3) by blast

      have L: "Chn ?LHS = chine_hcomp μ (assocSB ν π ρ)  μ_νπ_ρ.chine_assoc 
                            chine_hcomp (assocSB μ ν π) ρ"
        using Chn_vcomp 1 arr_char chine_composites(1) chine_composites(3) seq_char
        by fastforce
      have R: "Chn ?RHS = μ_ν_πρ.chine_assoc  μν_π_ρ.chine_assoc"
        using Chn_vcomp assoc_in_homs(4) assoc_in_homs(5) seqI' by auto

      text ‹
        The outline of the proof is to show that the compositions of ?LHS›
        and ?RHS› with the two projections 𝗉0[μ.leg0, HνHπρ.leg1]› and
        𝗉1[μ.leg0, HνHπρ.leg1]› are equal, and then apply νπρ.prj'_joint_monic›.
      ›

      text ‹
        The case for projection 𝗉1[μ.leg0, HνHπρ.leg1]› does not have subcases,
        so we'll dispatch that one first.
      ›

      have "𝗉1[μ.leg0, HνHπρ.leg1]  Chn ?LHS = 𝗉1[μ.leg0, HνHπρ.leg1]  Chn ?RHS"
      proof -
        have "𝗉1[μ.leg0, HνHπρ.leg1]  Chn ?LHS = μν.prj1  μν_π_ρ.Prj11"
        proof -
          have "𝗉1[μ.leg0, HνHπρ.leg1]  Chn ?LHS =
                𝗉1[μ.leg0, HνHπρ.leg1]  chine_hcomp μ (assocSB ν π ρ)  μ_νπ_ρ.chine_assoc 
                  chine_hcomp (assocSB μ ν π) ρ"
            using L by simp
          also have "... = μ.chine  𝗉1[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                             chine_hcomp (assocSB μ ν π) ρ"
          proof -
            have "𝗉1[μ.leg0, HνHπρ.leg1]  chine_hcomp μ (assocSB ν π ρ) =
                  μ.chine  𝗉1[μ.leg0, HHνπρ.leg1]"
            proof -
              have "C.commutative_square 𝗉1[μ.cod.leg0, assocνπρ.cod.leg1] μ.chine
                     (chine_hcomp μ (assocSB ν π ρ)) 𝗉1[μ.leg0, assocνπρ.dom.leg1]"
                by blast
              thus ?thesis by auto
            qed
            thus ?thesis
            using C.comp_permute [of "𝗉1[μ.leg0, HνHπρ.leg1]" "chine_hcomp μ (assocSB ν π ρ)"
                                      μ.chine "𝗉1[μ.leg0, HHνπρ.leg1]"
                                     "μ_νπ_ρ.chine_assoc  chine_hcomp (assocSB μ ν π) ρ"]
              by blast
          qed
          also have "... = μ.chine  μ_νπ_ρ.Prj11  chine_hcomp (assocSB μ ν π) ρ"
            using C.comp_reduce [of "𝗉1[μ.leg0, HHνπρ.leg1]" μ_νπ_ρ.chine_assoc]
                  νπ_ρ.leg1_composite
            by fastforce
          also have "... = μ.chine  μν.prj1  μν_π_ρ.Prj11"
          proof -
            have "μ.chine  μ_νπ_ρ.Prj11  chine_hcomp (assocSB μ ν π) ρ =
                  μ.chine  μ_νπ.prj1  𝗉1[νπ.leg0  μ_νπ.prj0, ρ.leg1] 
                    chine_hcomp (assocSB μ ν π) ρ"
              using C.comp_assoc by simp
            also have "... = μ.chine  (μ_νπ.prj1  assocμνπ.chine)  𝗉1[assocμνπ.dom.leg0, ρ.leg1]"
            proof -
              have "𝗉1[νπ.leg0  μ_νπ.prj0, ρ.leg1]  chine_hcomp (assocSB μ ν π) ρ =
                    assocμνπ.chine  𝗉1[assocμνπ.dom.leg0, ρ.leg1]"
                using chine_hcomp_props(6) [of ρ "assocSB μ ν π"] hcomp_def [of μ "hcomp ν π"]
                      μν.composable νπ.composable πρ.composable
                      hseq_char assoc_in_homs(3)
                by auto
              thus ?thesis
                using C.comp_assoc by auto
            qed
            also have "... = μ.chine  μνπ.Prj11  𝗉1[assocμνπ.dom.leg0, ρ.leg1]"
              using μνπ.prj_chine_assoc(1) hcomp_def νπ.composable by auto
            also have "... = μ.chine  μν.prj1  μν_π_ρ.Prj11"
            proof -
              have "μνπ.Prj11  𝗉1[assocμνπ.dom.leg0, ρ.leg1] = μν.prj1  μν_π_ρ.Prj11"
                by (simp add: C.comp_assoc μν.leg0_composite μν_π.leg0_composite)
              thus ?thesis by simp
            qed
            finally show ?thesis by blast
          qed
          also have "... = μν.prj1  μν_π_ρ.Prj11"
            using μν_π_ρ.prj_in_hom(1) hcomp_def [of μ ν] chine_hcomp_ide_ide μν.cod.apex_def
                  μν.composable μ_ν_πρ.cospan_μν C.comp_ide_arr
            by auto
          finally show ?thesis by blast
        qed
        also have "... = 𝗉1[μ.leg0, HνHπρ.leg1]  Chn ?RHS"
          by (metis C.comp_assoc R μν.leg0_composite μν_π_ρ.prj_chine_assoc(1)
                    μ_ν_πρ.prj_chine_assoc(1) ν_πρ.leg1_composite πρ.leg1_composite)
        finally show ?thesis by blast
      qed

      text ‹
        Now for the case of 𝗉0[μ.leg0, HνHπρ.leg1]›.
        We have to consider three sub-cases, involving the compositions with the projections
        νπρ.Prj1, νπρ.Prj10, and νπρ.Prj00.
      ›

      moreover have "𝗉0[μ.leg0, HνHπρ.leg1]  Chn ?LHS =
                     𝗉0[μ.leg0, HνHπρ.leg1]  Chn ?RHS"
      proof -
        (* Facts common to the three sub-cases. *)
        have A: "𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc =
                μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0"
          using μ_νπ_ρ.chine_assoc_def νπ_ρ.leg1_composite by auto
        have B: "μ_νπ_ρ.Prj01  chine_hcomp (assocSB μ ν π) ρ =
                 μ_νπ.prj0  μνπ.chine_assoc  𝗉1[HHμνπ.leg0, ρ.leg1]"
        proof -
          have "μ_νπ_ρ.Prj01  chine_hcomp (assocSB μ ν π) ρ =
                (μ_νπ.prj0  𝗉1[assocμνπ.cod.leg0, ρ.cod.leg1])  chine_hcomp (assocSB μ ν π) ρ"
            using μ_νπ.composable νπ.composite_is_arrow hcomp_def by auto
          also have "... = μ_νπ.prj0  𝗉1[assocμνπ.cod.leg0, ρ.cod.leg1] 
                             chine_hcomp (assocSB μ ν π) ρ"
            using C.comp_assoc by simp
          also have "... = μ_νπ.prj0  μνπ.chine_assoc  𝗉1[HHμνπ.leg0, ρ.leg1]"
          proof -
            have "HHμνπ.leg0 = assocμνπ.dom.leg0"
              using hcomp_def [of "hcomp μ ν" π] by simp
            moreover have "C.commutative_square assocμνπ.cod.leg0 ρ.cod.leg1
                               (assocμνπ.chine  𝗉1[assocμνπ.dom.leg0, ρ.leg1])
                               (ρ.chine  𝗉0[assocμνπ.dom.leg0, ρ.leg1])"
              by blast
            ultimately show ?thesis
              using chine_hcomp_def [of "assocSB μ ν π" ρ] by simp
          qed
          finally show ?thesis by blast
        qed
        have *: "assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                   chine_hcomp (assocSB μ ν π) ρ =
                 μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
        proof -
          text ‹Subcase νπρ.Prj1:›
          have "νπρ.Prj1  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                  chine_hcomp (assocSB μ ν π) ρ =
                νπρ.Prj1  μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
          proof -
            have "νπρ.Prj1  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ =
                  νπρ.Prj11  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ"
              using νπρ.chine_assoc_props(1) C.prj0_in_hom [of μ.leg0 HHνπρ.leg1] cospan_μ0_HνHπρ1
                    C.comp_reduce [of νπρ.Prj1 assocνπρ.chine νπρ.Prj11
                                      "𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                                         chine_hcomp (assocSB μ ν π) ρ"]
              by auto
            also have "... = νπρ.Prj11  μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0 
                              chine_hcomp (assocSB μ ν π) ρ"
              using A C.comp_reduce [of "𝗉0[μ.leg0, HHνπρ.leg1]" μ_νπ_ρ.chine_assoc]
              by fastforce
            also have "... = νπ.prj1  μ_νπ_ρ.Prj01  chine_hcomp (assocSB μ ν π) ρ"
              by (metis A C.comp_assoc μ_νπ_ρ.prj_chine_assoc(2) νπ.leg0_composite
                        νπ_ρ.leg1_composite)
            also have "... = νπ.prj1  μ_νπ.prj0  μνπ.chine_assoc  𝗉1[HHμνπ.leg0, ρ.leg1]"
              using B by simp
            also have "... = μνπ.Prj01  𝗉1[HHμνπ.leg0, ρ.leg1]"
              using hcomp_def [of ν π] νπ.composable C.comp_assoc
                    C.comp_reduce [of μνπ.Prj10 μνπ.chine_assoc μνπ.Prj01 "𝗉1[HHμνπ.leg0, ρ.leg1]"]
                    μνπ.prj_in_hom(5) μνπ.prj_chine_assoc(2)
              by auto
            also have "... = νπρ.Prj1 
                             μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
              by (metis (no_types, lifting) C.comp_assoc C.prj_tuple(2) μν.leg0_composite
                  μνπ.leg0_composite(2) μν_π_ρ.prj_chine_assoc(1) πρ.leg1_composite
                  commutative_squares(2))
            finally show ?thesis by simp
          qed
          moreover
          text ‹Subcase νπρ.Prj10:›
          have "νπρ.Prj10  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                  chine_hcomp (assocSB μ ν π) ρ =
                νπρ.Prj10  μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
          proof -
            have "νπρ.Prj10  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ =
                  νπρ.Prj01  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ"
              using C.comp_reduce [of νπρ.Prj10 "assocνπρ.chine" νπρ.Prj01
                                      "𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                                         chine_hcomp (assocSB μ ν π) ρ"]
              by auto
            also have "... = νπρ.Prj01  μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0 
                              chine_hcomp (assocSB μ ν π) ρ"
              using A C.comp_reduce [of "𝗉0[μ.leg0, HHνπρ.leg1]" μ_νπ_ρ.chine_assoc]
              by fastforce
            also have "... = νπ.prj0  μ_νπ_ρ.Prj01  chine_hcomp (assocSB μ ν π) ρ"
              by (metis A C.comp_assoc μ_νπ_ρ.prj_chine_assoc(2) νπ.leg0_composite
                        νπ_ρ.leg1_composite)
            also have "... = νπ.prj0  μ_νπ.prj0  μνπ.chine_assoc  𝗉1[HHμνπ.leg0, ρ.leg1]"
              using B by simp
            also have "... = μνπ.Prj0  𝗉1[HHμνπ.leg0, ρ.leg1]"
              using hcomp_def [of ν π] νπ.composable μνπ.prj_in_hom(6)
                    C.comp_reduce [of νπ.prj0 μ_νπ.prj0 μνπ.Prj00
                                      "μνπ.chine_assoc  𝗉1[HHμνπ.leg0, ρ.leg1]"]
                    C.comp_reduce [of μνπ.Prj00 μνπ.chine_assoc μνπ.Prj0
                                      "𝗉1[HHμνπ.leg0, ρ.leg1]"]
              by fastforce
            also have "... = νπρ.Prj10 
                             μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
              by (metis C.comp_assoc C.tuple_prj μν.leg0_composite μν_π.leg0_composite
                        μν_π_ρ.prj_chine_assoc(2) μ_ν_πρ.cospan_νπ μ_ν_πρ.prj_chine_assoc(2)
                        μ_ν_πρ.prj_chine_assoc(3) μ_ν_πρ.prj_simps(2) πρ.leg1_composite)
            finally show ?thesis by blast
          qed
          moreover
          text ‹Subcase νπρ.Prj00:›
          have "νπρ.Prj00  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                  chine_hcomp (assocSB μ ν π) ρ =
                νπρ.Prj00  μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
          proof -
            have "νπρ.Prj00  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ =
                  νπρ.Prj0  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                    chine_hcomp (assocSB μ ν π) ρ"
              using C.comp_reduce [of νπρ.Prj00 assocνπρ.chine νπρ.Prj0
                                      "𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                                         chine_hcomp (assocSB μ ν π) ρ"]
              by fastforce
            also have "... = νπρ.Prj0  μ_νπ_ρ.Prj01 νπ.leg0, ρ.leg1 μ_νπ_ρ.Prj0 
                              chine_hcomp (assocSB μ ν π) ρ"
              using A C.comp_reduce [of "𝗉0[μ.leg0, HHνπρ.leg1]" μ_νπ_ρ.chine_assoc]
              by fastforce
            also have "... = μ_νπ_ρ.Prj0  chine_hcomp (assocSB μ ν π) ρ"
              by (metis A C.comp_assoc μ_νπ_ρ.prj_chine_assoc(3) νπ.leg0_composite
                        νπ_ρ.leg1_composite)
            also have "... = ρ.chine  𝗉0[assocμνπ.dom.leg0, ρ.leg1]"
            proof -
              have "μ_νπ_ρ.Prj0 = 𝗉0[assocμνπ.cod.leg0, ρ.cod.leg1]"
                using μ_νπ.composable νπ.composite_is_arrow hcomp_def by auto
              thus ?thesis
                using chine_hcomp_props(5) [of ρ "assocSB μ ν π"]
                      μν.composable νπ.composable πρ.composable
                by simp
            qed
            also have "... = 𝗉0[HHμνπ.leg0, ρ.leg1]"
              by (metis C.comp_cod_arr C.in_homE arrow_of_spans_data.select_convs(2)
                        prj_in_homs(4))
            also have "... = νπρ.Prj00 
                             μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
              by (metis C.comp_assoc C.tuple_prj μν.leg0_composite μν_π.leg0_composite
                        μν_π_ρ.prj_chine_assoc(3) μ_ν_πρ.cospan_νπ μ_ν_πρ.prj_chine_assoc(2)
                        μ_ν_πρ.prj_chine_assoc(3) μ_ν_πρ.prj_simps(2) πρ.leg1_composite)
            finally show ?thesis by blast
          qed
          moreover have "«assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                            chine_hcomp (assocSB μ ν π) ρ : HHHμνπρ.chine C HνHπρ.chine»"
            using νπρ.chine_assoc_props(1) by fast
          moreover have "«μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc :
                            HHHμνπρ.chine C HνHπρ.chine»"
          proof -
            have "«μν_π_ρ.chine_assoc : HHHμνπρ.chine C HHμνHπρ.chine»"
              using μν_π_ρ.chine_assoc_props(1) by blast
            moreover have "«μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0 :
                              HHμνHπρ.chine C HνHπρ.chine»"
              using chine_hcomp_ide_ide hcomp_def [of ν "hcomp π ρ"] νπ.composable by auto
            ultimately show ?thesis by blast
          qed
          ultimately show ?thesis
            using νπρ.prj'_joint_monic
                    [of "assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                           chine_hcomp (assocSB μ ν π) ρ"
                        HHHμνπρ.chine
                        "μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"]
            by simp
        qed

        text ‹
          Now use fact *› to finish off the 𝗉0[μ.leg0, HνHπρ.leg1]› case.
        ›
        have "𝗉0[μ.leg0, HνHπρ.leg1]  Chn ?LHS =
              assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                chine_hcomp (assocSB μ ν π) ρ"
        proof -
          have "𝗉0[μ.leg0, HνHπρ.leg1]  Chn ?LHS =
                𝗉0[μ.leg0, HνHπρ.leg1]  chine_hcomp μ (assocSB ν π ρ)  μ_νπ_ρ.chine_assoc 
                  chine_hcomp (assocSB μ ν π) ρ"
            using L by simp
          also have "... = assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]  μ_νπ_ρ.chine_assoc 
                             chine_hcomp (assocSB μ ν π) ρ"
          proof -
            have "𝗉0[μ.leg0, HνHπρ.leg1]  chine_hcomp μ (assocSB ν π ρ) =
                  assocνπρ.chine  𝗉0[μ.leg0, HHνπρ.leg1]"
            proof -
              have "C.commutative_square 𝗉0[μ.cod.leg0, assocνπρ.cod.leg1] assocνπρ.chine
                      (chine_hcomp μ (assocSB ν π ρ)) 𝗉0[μ.leg0, assocνπρ.dom.leg1]"
                by blast
              thus ?thesis
                using νπρ.chine_assoc_props(1) by auto
            qed
            moreover have "C.seq 𝗉0[μ.leg0, HνHπρ.leg1] (chine_hcomp μ (assocSB ν π ρ))"
              using cospan_μ0_HνHπρ1 prj_in_homs(2) by fastforce
            moreover have "C.seq (chine_hcomp μ (assocSB ν π ρ))
                                 (μ_νπ_ρ.chine_assoc  chine_hcomp (assocSB μ ν π) ρ)"
              by blast
            ultimately show ?thesis
              using chine_hcomp_props(4) C.comp_permute by auto
          qed
          finally show ?thesis by blast
        qed
        also have "... = μ_ν_πρ.Prj01 ν.leg0, πρ.leg1 μ_ν_πρ.Prj0  μν_π_ρ.chine_assoc"
          using * by simp
        also have "... = 𝗉0[μ.leg0, HνHπρ.leg1]  Chn ?RHS"
          by (metis C.comp_assoc C.tuple_prj R μ_ν_πρ.cospan_νπ μ_ν_πρ.prj_chine_assoc(2)
                    μ_ν_πρ.prj_chine_assoc(3) μ_ν_πρ.prj_simps(2) ν_πρ.leg1_composite)
        finally show ?thesis by blast
      qed
      moreover have "C.seq 𝗉1[μ.leg0, HνHπρ.leg1] (Chn ?LHS)"
        using LHS_in_hom Chn_in_hom by blast
      moreover have "C.seq 𝗉1[μ.leg0, HνHπρ.leg1] (Chn ?RHS)"
        using RHS_in_hom Chn_in_hom by blast
      ultimately show "Chn ?LHS = Chn ?RHS"
        using cospan_μ0_HνHπρ1 C.prj_joint_monic by blast
    qed

  end

  context span_bicategory
  begin

    lemma pentagon:
    assumes "ide f" and "ide g" and "ide h" and "ide k"
    and "src f = trg g" and "src g = trg h" and "src h = trg k"
    shows "(f  αSB (g, h, k))  αSB (f, g  h, k)  (αSB (f, g, h)  k) =
           αSB (f, g, h  k)  αSB (f  g, h, k)"
    proof -
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      interpret g: identity_arrow_of_spans C g
        using assms ide_char' by auto
      interpret h: identity_arrow_of_spans C h
        using assms ide_char' by auto
      interpret k: identity_arrow_of_spans C k
        using assms ide_char' by auto

      interpret fghk: four_composable_identity_arrows_of_spans C prj0 prj1 f g h k
        using assms by (unfold_locales, auto)

      let ?LHS = "(f  assocSB g h k)  (assocSB f (g  h) k)  (assocSB f g h  k)"
      let ?RHS = "assocSB f g (h  k)  assocSB (f  g) h k"

      have "(f  αSB (g, h, k))  αSB (f, g  h, k)  (αSB (f, g, h)  k) = ?LHS"
        using assms α_ide ide_hcomp src_hcomp trg_hcomp by simp
      also have "... = ?RHS"
        using fghk.μν.composable fghk.νπ.composable fghk.πρ.composable fghk.chine_pentagon
        by (intro arr_eqI, auto)
      also have "... = αSB (f, g, h  k)  αSB (f  g, h, k)"
        using assms α_ide ide_hcomp src_hcomp trg_hcomp by simp
      finally show ?thesis by blast
    qed

    lemma extends_to_bicategory:
    shows "bicategory vcomp hcomp assoc unit src trg"
      using unit_in_hom obj_char iso_unit assoc_def pentagon
      apply unfold_locales by auto

    sublocale bicategory vcomp hcomp assoc unit src trg
      using extends_to_bicategory by auto

  subsection "Miscellaneous Formulas"

    no_notation in_hom    ("«_ : _  _»")
    notation in_hom       ("«_ : _  _»")

    notation lunit        ("𝗅[_]")
    notation runit        ("𝗋[_]")
    notation lunit'       ("𝗅-1[_]")
    notation runit'       ("𝗋-1[_]")
    notation assoc        ("𝖺[_, _, _]")
    notation 𝖺'           ("𝖺-1[_, _, _]")

    lemma α'_ide:
    assumes "ide f" and "ide g" and "ide h"
    and "src f = trg g" and "src g = trg h"
    shows "α' (f, g, h) = assoc'SB f g h"
    proof -
      have fgh: "VVV.ide (f, g, h)"
        using assms VVV.ide_charSbC VVV.arr_charSbC VV.arr_charSbC by simp
      interpret f: arrow_of_spans C f
        using assms arr_char [of f] by auto
      interpret g: arrow_of_spans C g
        using assms arr_char [of g] by auto
      interpret h: arrow_of_spans C h
        using assms arr_char [of h] by auto
      interpret fgh: three_composable_arrows_of_spans C prj0 prj1 f g h
        using assms by (unfold_locales, auto)
      interpret fgh: three_composable_identity_arrows_of_spans C prj0 prj1 f g h
        using assms ide_char by (unfold_locales, auto)
      have "α' (f, g, h) = inv (α (f, g, h))"
        using fgh α'.inverts_components
        by (simp add: α_def)
      moreover have "inv (α (f, g, h)) = Chn = C.inv (Chn (α (f, g, h))),
                                          Dom = Cod (α (f, g, h)),
                                          Cod = Dom (α (f, g, h))"
        using fgh α.components_are_iso inv_eq
        by (simp add: α_def fgh.μν.composable fgh.νπ.composable)
      moreover have "... = assoc'SB f g h"
        using assms fgh α_ide [of f g h] fgh.chine_assoc_inverse C.inverse_unique
        by (simp add: α_def)
      ultimately show ?thesis by simp
    qed

    text ‹
      The following give explicit expressions for the unitors,
      derived from their characterizing properties and the definition of the associators.
    ›

    lemma runit_ide_eq:
    assumes "ide f"
    shows "𝗋[f] = Chn = 𝗉1[Leg0 (Dom f), C.cod (Leg0 (Dom f))],
                   Dom = Leg0 = 𝗉0[Leg0 (Dom f), C.cod (Leg0 (Dom f))],
                          Leg1 = Leg1 (Dom f)  𝗉1[Leg0 (Dom f), C.cod (Leg0 (Dom f))],
                   Cod = Cod f"
    proof -
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      interpret src: identity_arrow_of_spans C src f
        using assms ide_char' ide_src by auto
      interpret f_src: two_composable_identity_arrows_of_spans C prj0 prj1 f src f
        using assms by (unfold_locales, simp)
      interpret src_src: two_composable_identity_arrows_of_spans C prj0 prj1 src f src f
        by (unfold_locales, simp)
      interpret f_src_src: three_composable_identity_arrows_of_spans C prj0 prj1 f src f src f
        ..

      let ?rf = "Chn = 𝗉1[f.leg0, f.dsrc],
                  Dom = Leg0 = 𝗉0[f.leg0, f.dsrc], Leg1 = f.leg1  𝗉1[f.leg0, f.dsrc],
                  Cod = Cod f"
      have "?rf = 𝗋[f]"
      proof (intro runit_eqI)
        show "ide f" by fact
        interpret rf: arrow_of_spans C ?rf
        proof -
          interpret dom_rf: span_in_category C
                              Leg0 = 𝗉0[f.leg0, f.dsrc], Leg1 = f.leg1  𝗉1[f.leg0, f.dsrc]
            by (unfold_locales, simp_all)
          show "arrow_of_spans C ?rf"
            using dom_rf.apex_def C.comp_cod_arr C.pullback_commutes [of f.leg0 f.dsrc]
            apply unfold_locales by auto
        qed
        show rf_in_hom: "«?rf : f  src f  f»"
        proof
          show "arr ?rf"
            using rf.arrow_of_spans_axioms arr_char by simp
          show "cod ?rf = f"
            using cod_char rf.arrow_of_spans_axioms arr_char by simp
          show "dom ?rf = f  src f"
            using dom_char rf.arrow_of_spans_axioms src.arrow_of_spans_axioms arr_char hcomp_def
                  f.arrow_of_spans_axioms f_src.composable chine_hcomp_ide_ide src_def ide_char
                  C.comp_cod_arr rf.dom.apex_def
            by simp
        qed
        show "?rf  src f = (f  𝗂[src f])  𝖺[f, src f, src f]"
        proof (intro arr_eqI)
          show par: "par (?rf  src f) ((f  𝗂[src f])  𝖺[f, src f, src f])"
          proof -
            have "«?rf  src f : (f  src f)  src f  f  src f»"
              using f_src_src.composites_are_arrows(2) rf_in_hom src_src.are_identities(1)
              by blast
            thus ?thesis by auto
          qed
          show "Chn (?rf  src f) = Chn ((f  𝗂[src f])  𝖺[f, src f, src f])"
          proof -
            have "Chn (?rf  src f) = f_src_src.Prj11 f.leg0, src.leg1 f_src_src.Prj01"
            proof -
              have "Chn (?rf  src f) =
                    f_src_src.Prj11 f.leg0, src.leg1 𝗉0[f_src.prj0, src.leg1]"
                using assms src_def trg_def hcomp_def arr_char ide_char
                      rf.arrow_of_spans_axioms src.identity_arrow_of_spans_axioms
                      chine_hcomp_arr_ide C.comp_cod_arr
                by (simp add: f.arrow_of_spans_axioms identity_arrow_of_spans_def)
              moreover have "𝗉0[f_src.prj0, src.leg1] = f_src_src.Prj01"
              proof -
                have "src f = Chn = f.dsrc,
                               Dom = Leg0 = f.dsrc, Leg1 = f.dsrc,
                               Cod = Leg0 = f.dsrc, Leg1 = f.dsrc"
                  using assms src_def by simp
                thus ?thesis
                  by (simp add: C.comp_cod_arr C.pullback_commutes')
              qed
              ultimately show ?thesis by auto
            qed
            also have "... = Chn ((f  𝗂[src f])  𝖺[f, src f, src f])"
            proof -
              have "Chn ((f  𝗂[src f])  𝖺[f, src f, src f]) =
                    f_src_src.Prj1 f.leg0, src.leg1 f_src_src.Prj10  f_src_src.chine_assoc"
              proof -
                have "Chn ((f  𝗂[src f])  𝖺[f, src f, src f]) =
                      Chn (f  𝗂[src f])  Chn 𝖺[f, src f, src f]"
                  using par vcomp_eq [of "f  𝗂[src f]" "𝖺[f, src f, src f]"]
                  by simp
                moreover have "Chn (f  𝗂[src f]) =
                               f_src_src.Prj1 f.leg0, src.leg1 f_src_src.Prj10"
                proof -
                  have "𝗂[src f] = Chn = 𝗉1[f.dsrc, f.dsrc],
                                   Dom = Leg0 = 𝗉1[f.dsrc, f.dsrc], Leg1 = 𝗉1[f.dsrc, f.dsrc],
                                   Cod = Leg0 = f.dsrc, Leg1 = f.dsrc"
                    using unit_def src_def trg_def hcomp_def src.arrow_of_spans_axioms arr_char
                          f.arrow_of_spans_axioms C.comp_cod_arr
                    by simp
                  moreover have "arrow_of_spans C 𝗂[src f]"
                    using assms arr_char [of "𝗂[src f]"] by simp
                  ultimately show ?thesis
                    using assms unit_def hcomp_def chine_hcomp_ide_arr
                          rf.arrow_of_spans_axioms src.arrow_of_spans_axioms
                          f.arrow_of_spans_axioms arr_char C.comp_cod_arr
                          src_def trg_def
                    by simp
                qed
                ultimately show ?thesis
                  using α_ide by simp
              qed
              also have "... = f_src_src.Prj1  f_src_src.chine_assoc
                                  f.leg0, src.leg1
                                f_src_src.Prj10  f_src_src.chine_assoc"
                using C.comp_assoc C.comp_tuple_arr C.pullback_commutes'
                      f_src_src.cospan_μν f_src_src.cospan_νπ
                by simp
              also have "... = f_src_src.Prj11 f.leg0, src.leg1 f_src_src.Prj01"
                by simp
              finally show ?thesis by simp
            qed
            finally show ?thesis by simp
          qed
        qed
      qed
      thus ?thesis by simp
    qed

    lemma lunit_ide_eq:
    assumes "ide f"
    shows "𝗅[f] = Chn = 𝗉0[C.cod (Leg1 (Dom f)), Leg1 (Dom f)],
                   Dom = Leg0 = Leg0 (Dom f)  𝗉0[C.cod (Leg1 (Dom f)), Leg1 (Dom f)],
                          Leg1 = 𝗉1[C.cod (Leg1 (Dom f)), Leg1 (Dom f)],
                   Cod = Cod f"
    proof -
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      interpret trg: identity_arrow_of_spans C trg f
        using assms ide_char' ide_trg by auto
      interpret trg_f: two_composable_identity_arrows_of_spans C prj0 prj1 trg f f
        using assms by (unfold_locales, simp)
      interpret trg_trg: two_composable_identity_arrows_of_spans C prj0 prj1 trg f trg f
        by (unfold_locales, simp)
      interpret trg_trg_f: three_composable_identity_arrows_of_spans C prj0 prj1 trg f trg f f
        ..

      let ?lf = "Chn = 𝗉0[f.dtrg, f.leg1],
                  Dom = Leg0 = f.leg0  𝗉0[f.dtrg, f.leg1], Leg1 = 𝗉1[f.dtrg, f.leg1],
                  Cod = Cod f"
      have "?lf = 𝗅[f]"
      proof (intro lunit_eqI)
        show "ide f" by fact
        interpret lf: arrow_of_spans C ?lf
        proof -
          interpret dom_lf: span_in_category C
                              Leg0 = f.leg0  𝗉0[f.dtrg, f.leg1], Leg1 = 𝗉1[f.dtrg, f.leg1]
            by (unfold_locales, simp_all)
          show "arrow_of_spans C ?lf"
            using dom_lf.apex_def C.comp_cod_arr C.pullback_commutes [of f.dtrg f.leg1]
            apply unfold_locales by auto
        qed
        show lf_in_hom: "«?lf : trg f  f  f»"
        proof
          show "arr ?lf"
            using lf.arrow_of_spans_axioms arr_char by simp
          show "cod ?lf = f"
            using cod_char lf.arrow_of_spans_axioms arr_char by simp
          show "dom ?lf = trg f  f"
            using dom_char lf.arrow_of_spans_axioms trg.arrow_of_spans_axioms arr_char hcomp_def
                  f.arrow_of_spans_axioms trg_f.composable chine_hcomp_ide_ide trg_def ide_char
                  C.comp_cod_arr lf.dom.apex_def
            by simp
        qed
        show "trg f  ?lf = (𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]"
        proof (intro arr_eqI)
          show par: "par (trg f  ?lf) ((𝗂[trg f]  f)  𝖺-1[trg f, trg f, f])"
          proof -
            have "«trg f  ?lf : trg f  (trg f  f)  trg f  f»"
            proof -
              have "trg f  ?lf = L ?lf"
                using assms lf_in_hom src_def trg_def arr_char lf.arrow_of_spans_axioms
                      f.arrow_of_spans_axioms
                by simp
              moreover have "«L ?lf : trg f  (trg f  f)  trg f  f»"
                using lf_in_hom L.preserves_hom [of ?lf "trg f  f" f] by simp
              ultimately show ?thesis by auto
            qed
            thus ?thesis by auto
          qed
          show "Chn (trg f  ?lf) = Chn ((𝗂[trg f]  f)  𝖺-1[trg f, trg f, f])"
          proof -
            have "Chn (trg f  ?lf) = trg_trg_f.Prj10 trg.leg0, f.leg1 trg_trg_f.Prj00"
            proof -
              have "Chn (trg f  ?lf) =
                    𝗉1[trg.leg0, trg_f.prj1] trg.leg0, f.leg1 trg_trg_f.Prj00"
                using assms src_def trg_def hcomp_def arr_char ide_char
                      lf.arrow_of_spans_axioms trg.identity_arrow_of_spans_axioms
                      chine_hcomp_ide_arr C.comp_cod_arr
                by (simp add: f.arrow_of_spans_axioms identity_arrow_of_spans_def)
              moreover have "𝗉1[trg.leg0, trg_f.prj1] = trg_trg_f.Prj10"
              proof -
                have "trg f = Chn = f.dtrg,
                               Dom = Leg0 = f.dtrg, Leg1 = f.dtrg,
                               Cod = Leg0 = f.dtrg, Leg1 = f.dtrg"
                  using assms trg_def by simp
                thus ?thesis
                  apply (simp add: C.comp_cod_arr C.pullback_commutes')
                  by (metis C.comp_cod_arr C.pullback_commutes' select_convs(1) select_convs(2)
                      select_convs(3) f.cod_simps(3) lf.cod_trg_eq_dom_trg lf.dom.leg_simps(3)
                      span_data.select_convs(1) span_data.select_convs(2) trg.chine_eq_apex
                      trg_trg_f.cospan_νπ trg_trg_f.prj_simps(10) trg_trg_f.prj_simps(16))
              qed
              ultimately show ?thesis by auto
            qed
            also have "... = Chn ((𝗂[trg f]  f)  𝖺-1[trg f, trg f, f])"
            proof -
              have "Chn ((𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]) =
                    trg_trg_f.Prj01 trg.leg0, f.leg1 trg_trg_f.Prj0  trg_trg_f.chine_assoc'"
              proof -
                have "Chn ((𝗂[trg f]  f)  𝖺-1[trg f, trg f, f]) =
                      Chn (𝗂[trg f]  f)  Chn 𝖺-1[trg f, trg f, f]"
                  using par vcomp_eq [of "𝗂[trg f]  f" "𝖺-1[trg f, trg f, f]"]
                  by simp
                moreover have "Chn (𝗂[trg f]  f) =
                               trg_trg_f.Prj01 trg.leg0, f.leg1 trg_trg_f.Prj0"
                proof -
                  have "𝗂[trg f] = Chn = 𝗉1[f.dtrg, f.dtrg],
                                   Dom = Leg0 = 𝗉1[f.dtrg, f.dtrg], Leg1 = 𝗉1[f.dtrg, f.dtrg],
                                   Cod = Leg0 = f.dtrg, Leg1 = f.dtrg"
                    using unit_def src_def trg_def hcomp_def trg.arrow_of_spans_axioms arr_char
                          f.arrow_of_spans_axioms C.comp_cod_arr
                    by simp
                  moreover have "arrow_of_spans C 𝗂[trg f]"
                    using assms arr_char [of "𝗂[trg f]"] by simp
                  ultimately show ?thesis
                    using assms unit_def hcomp_def chine_hcomp_arr_ide
                          lf.arrow_of_spans_axioms trg.arrow_of_spans_axioms
                          f.arrow_of_spans_axioms arr_char C.comp_cod_arr
                          src_def trg_def
                    by simp
                qed
                moreover have "Chn 𝖺-1[trg f, trg f, f] = trg_trg_f.chine_assoc'"
                proof -
                  have "iso (α (trg f, trg f, f))"
                    by (simp add: α_def)
                  moreover have "C.inv trg_trg_f.chine_assoc = trg_trg_f.chine_assoc'"
                    using trg_trg_f.chine_assoc_inverse C.inv_is_inverse C.inverse_arrow_unique
                    by auto
                  ultimately show ?thesis
                    using assms by (simp add: 𝖺'_def α'_ide)
                qed
                ultimately show ?thesis
                  by simp
              qed
              also have "... = trg_trg_f.Prj01  trg_trg_f.chine_assoc'
                                  trg.leg0, f.leg1
                                trg_trg_f.Prj0  trg_trg_f.chine_assoc'"
              proof -
                have "C.commutative_square trg.leg0 f.leg1 trg_trg_f.Prj01 trg_trg_f.Prj0"
                proof
                  show "C.cospan trg.leg0 f.leg1"
                    using trg_f.legs_form_cospan(1) by auto
                  show "C.span trg_trg_f.Prj01 trg_trg_f.Prj0"
                    using trg_trg_f.prj_in_hom by auto
                  show "C.dom trg.leg0 = C.cod trg_trg_f.Prj01"
                    by simp
                  show "trg.leg0  trg_trg_f.Prj01 = f.leg1  trg_trg_f.Prj0"
                    by (metis C.comp_assoc C.prj0_simps_arr C.pullback_commutes'
                        C.span trg_trg_f.Prj01 trg_trg_f.Prj0)
                qed
                moreover have "C.seq trg_trg_f.Prj01 trg_trg_f.chine_assoc'"
                  by blast
                ultimately show ?thesis
                  using C.comp_tuple_arr [of trg.leg0 f.leg1 trg_trg_f.Prj01 trg_trg_f.Prj0
                                             trg_trg_f.chine_assoc']
                  by auto
              qed
              also have "... = trg_trg_f.Prj10 trg.leg0, f.leg1 trg_trg_f.Prj00"
                by simp
              finally show ?thesis by simp
            qed
            finally show ?thesis by blast
          qed
        qed
      qed
      thus ?thesis by simp
    qed

    lemma runit'_ide_eq:
    assumes "ide f"
    shows "𝗋-1[f] = Chn = Chn f Leg0 (Dom f), C.cod (Leg0 (Dom f)) Leg0 (Dom f),
                    Dom = Cod f,
                    Cod = Leg0 = 𝗉0[Leg0 (Dom f), C.cod (Leg0 (Dom f))],
                           Leg1 = Leg1 (Dom f)  𝗉1[Leg0 (Dom f), C.cod (Leg0 (Dom f))]"
    proof -
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      show "𝗋-1[f] = Chn = f.chine f.leg0, f.dsrc f.leg0, Dom = Cod f,
                     Cod = Leg0 = 𝗉0[f.leg0, f.dsrc], Leg1 = f.leg1  𝗉1[f.leg0, f.dsrc]"
      proof -
        have "C.inverse_arrows 𝗉1[f.leg0, f.dsrc] f.chine f.leg0, f.dsrc f.leg0"
          using C.pullback_arr_cod(1) f.chine_eq_apex f.dom.apex_def f.dom.leg_simps(1)
          by presburger
        hence "C.inv 𝗉1[f.leg0, f.dsrc] = f.chine f.leg0, f.dsrc f.leg0"
          using C.inv_is_inverse C.inverse_arrow_unique by auto
        hence "𝗋-1[f] = Chn = f.chine f.leg0, f.dsrc f.leg0,
                        Dom = Cod 𝗋[f], Cod = Dom 𝗋[f]"
          using assms runit_ide_eq inv_eq [of "𝗋[f]"] iso_runit by simp
        thus ?thesis
          using assms runit_ide_eq by simp
      qed
    qed

    lemma lunit'_ide_eq:
    assumes "ide f"
    shows "𝗅-1[f] = Chn = Leg1 (Dom f) C.cod (Leg1 (Dom f)), Leg1 (Dom f) Chn f,
                    Dom = Cod f,
                    Cod = Leg0 = Leg0 (Dom f)  𝗉0[C.cod (Leg1 (Dom f)), Leg1 (Dom f)],
                           Leg1 = 𝗉1[C.cod (Leg1 (Dom f)), Leg1 (Dom f)]"
    proof -
      interpret f: identity_arrow_of_spans C f
        using assms ide_char' by auto
      show "𝗅-1[f] = Chn = f.leg1 f.dtrg, f.leg1 f.chine, Dom = Cod f,
                     Cod = Leg0 = f.leg0  𝗉0[f.dtrg, f.leg1], Leg1 = 𝗉1[f.dtrg, f.leg1]"
      proof -
        have "C.inverse_arrows 𝗉0[f.dtrg, f.leg1] f.leg1 f.dtrg, f.leg1 f.chine"
          using C.pullback_arr_cod(2) f.chine_eq_apex f.dom.apex_def f.dom.is_span
          by presburger
        hence "C.inv 𝗉0[f.dtrg, f.leg1] = f.leg1 f.dtrg, f.leg1 f.chine"
          using C.inv_is_inverse C.inverse_arrow_unique by auto
        hence "𝗅-1[f] = Chn = f.leg1 f.dtrg, f.leg1 f.chine,
                        Dom = Cod 𝗅[f], Cod = Dom 𝗅[f]"
          using assms lunit_ide_eq inv_eq [of "𝗅[f]"] iso_lunit by simp
        thus ?thesis
          using assms lunit_ide_eq by simp
      qed
    qed

  end

  locale adjunction_data_in_span_bicategory =
     span_bicategory C prj0 prj1 +
     adjunction_data_in_bicategory vcomp hcomp assoc unit src trg f g η ε
  for C :: "'a  'a  'a"         (infixr "" 55)
  and prj0 :: "'a  'a  'a"      ("𝗉0[_, _]")
  and prj1 :: "'a  'a  'a"      ("𝗉1[_, _]")
  and f :: "'a arrow_of_spans_data"
  and g :: "'a arrow_of_spans_data"
  and η :: "'a arrow_of_spans_data"
  and ε :: "'a arrow_of_spans_data"
  begin

    interpretation f: identity_arrow_of_spans C f
      using ide_char' [of f] by auto
    interpretation g: identity_arrow_of_spans C g
      using ide_char' [of g] by auto

    interpretation gf: two_composable_identity_arrows_of_spans C prj0 prj1 g f
      using antipar by (unfold_locales, auto)
    interpretation fg: two_composable_identity_arrows_of_spans C prj0 prj1 f g
      using antipar by (unfold_locales, auto)

    interpretation fgf: three_composable_identity_arrows_of_spans C prj0 prj1 f g f ..
    interpretation gfg: three_composable_identity_arrows_of_spans C prj0 prj1 g f g ..

    interpretation η: arrow_of_spans C η
      using arr_char unit_in_hom by auto
    interpretation ε: arrow_of_spans C ε
      using arr_char counit_in_hom by auto

    lemma chine_unit_in_hom:
    shows "«η.chine : f.dsrc C g.leg0 ↓↓ f.leg1»"
    proof -
      have "«η.chine : η.dom.apex C η.cod.apex»"
        using η.chine_in_hom by simp
      moreover have "η.dom.apex = f.dsrc"
        using η.dom.apex_def dom_char unit_simps src_def by auto
      moreover have "η.cod.apex = g.leg0 ↓↓ f.leg1"
        by (metis arrow_of_spans_data.select_convs(1) cod_char gf.chine_composite
                  unit_simps(1,3))
      ultimately show ?thesis by simp
    qed

    lemma chine_counit_in_hom:
    shows "«ε.chine : f.leg0 ↓↓ g.leg1 C f.dtrg»"
    proof -
      have "«ε.chine : ε.dom.apex C ε.cod.apex»"
        using ε.chine_in_hom by simp
      moreover have "ε.cod.apex = f.dtrg"
        using ε.cod.apex_def cod_char counit_simps trg_def gf.composable by auto
      moreover have "ε.dom.apex = f.leg0 ↓↓ g.leg1"
        by (metis Chn_in_hom ε.chine_simps(2) category.in_homE counit_in_hom(2)
                  fg.chine_composite span_vertical_category_axioms span_vertical_category_def)
      ultimately show ?thesis by simp
    qed

    lemma η_leg_simps:
    shows "η.dom.leg0 = f.dsrc" and "η.dom.leg1 = f.dsrc"
    and "η.cod.leg0 = gf.leg0" and "η.cod.leg1 = gf.leg1"
    proof -
      show "η.dom.leg0 = f.dsrc"
        using dom_char unit_simps(2) src_def by auto
      show "η.dom.leg1 = f.dsrc"
        using dom_char unit_simps(2) src_def by auto
      show "η.cod.leg0 = gf.leg0"
        using cod_char unit_simps(1,3)
        by (metis (no_types, lifting) arrow_of_spans_data.select_convs(2))
      show "η.cod.leg1 = gf.leg1"
        using cod_char unit_simps(1,3)
        by (metis (no_types, lifting) arrow_of_spans_data.select_convs(2))
    qed

    lemma ε_leg_simps:
    shows "ε.cod.leg0 = f.dtrg" and "ε.cod.leg1 = f.dtrg"
    and "ε.dom.leg0 = fg.leg0" and "ε.dom.leg1 = fg.leg1"
    proof -
      show "ε.cod.leg0 = f.dtrg"
        using cod_char counit_simps(3) trg_def gf.composable by auto
      show "ε.cod.leg1 = f.dtrg"
        using cod_char counit_simps(3) trg_def gf.composable by auto
      show "ε.dom.leg0 = fg.leg0"
        using dom_char counit_simps hcomp_def fg.composable by simp
      show "ε.dom.leg1 = fg.leg1"
        using dom_char counit_simps hcomp_def fg.composable by simp
    qed

    lemma Chn_triangle_eq:
    shows "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) = gf.prj0  η.chine  f.leg0"
    and "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) = gf.prj1  η.chine  g.leg1"
    proof -
      have 1: "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) =
               𝗉0[f.dtrg, f.leg1]  chine_hcomp ε f  fgf.chine_assoc'  chine_hcomp f η 
                 f.chine f.leg0, f.dsrc f.leg0"
      proof -
        have "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) =
              Chn 𝗅[f]  Chn (ε  f)  Chn 𝖺-1[f, g, f]  Chn (f  η)  Chn 𝗋-1[f]"
          using antipar Chn_vcomp by auto
        also have "... = 𝗉0[f.dtrg, f.leg1]  chine_hcomp ε f  fgf.chine_assoc' 
                           chine_hcomp f η  f.chine f.leg0, f.dsrc f.leg0"
          using α_ide fg.composable gf.composable fgf.chine_assoc_inverse
                C.inverse_unique inv_eq iso_assoc lunit_ide_eq hcomp_def [of ε f]
                gf.composable hcomp_def [of f η] fg.composable runit'_ide_eq
          by simp
        finally show ?thesis by blast
      qed
      moreover have "C.arr (Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]))"
        by (meson arrI arrow_of_spans.chine_simps(1) arr_char triangle_in_hom(3))
      ultimately have 2: "C.arr (𝗉0[f.dtrg, f.leg1]  chine_hcomp ε f  fgf.chine_assoc' 
                                   chine_hcomp f η  f.chine f.leg0, f.dsrc f.leg0)"
        by simp

      have "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) =
               𝗉0[f.dtrg, f.leg1]  chine_hcomp ε f  fgf.chine_assoc'  chine_hcomp f η 
                 f.chine f.leg0, f.dsrc f.leg0"
        using 1 by simp
      also have
        3: "... = fgf.Prj0  fgf.chine_assoc'  chine_hcomp f η  f.chine f.leg0, f.dsrc f.leg0"
        by (metis (no_types, lifting) C.comp_assoc C.comp_cod_arr ε_leg_simps(1,3)
            chine_hcomp_props(5) counit_simps(1,4) f.chine_eq_apex f.cod_simps(3)
            fg.composite_is_arrow fg.leg0_composite fgf.prj_simps(3,9) hseqE)
      also have 4: "... = fgf.Prj00  chine_hcomp f η  f.chine f.leg0, f.dsrc f.leg0"
        using C.comp_reduce [of fgf.Prj0 fgf.chine_assoc' fgf.Prj00
                                "chine_hcomp f η  f.chine f.leg0, f.dsrc f.leg0"]
              2 fgf.prj_chine_assoc'(3)
        by blast
      also have "... = (gf.prj0  η.chine  𝗉0[f.leg0, f.dsrc])  f.chine f.leg0, f.dsrc f.leg0"
      proof -
        have "fgf.Prj00  chine_hcomp f η = gf.prj0  η.chine  𝗉0[f.leg0, f.dsrc]"
        proof -
          have "fgf.Prj00  chine_hcomp f η =
                (gf.prj0  𝗉0[f.leg0, gf.leg1]) 
                   𝗉1[f.leg0, f.dsrc] f.leg0, gf.leg1 η.chine  𝗉0[f.leg0, f.dsrc]"
            using hcomp_def fg.composable gf.composable chine_hcomp_ide_arr η_leg_simps by auto
          also have "... = gf.prj0  𝗉0[f.leg0, gf.leg1] 
                             𝗉1[f.leg0, f.dsrc] f.leg0, gf.leg1 η.chine  𝗉0[f.leg0, f.dsrc]"
            using C.comp_assoc by simp
          also have "... = gf.prj0  η.chine  𝗉0[f.leg0, f.dsrc]"
          proof -
            have "C.commutative_square f.leg0 gf.leg1 𝗉1[f.leg0, f.dsrc] (η.chine  𝗉0[f.leg0, f.dsrc])"
            proof
              show "C.cospan f.leg0 gf.leg1"
                using hcomp_def gf.composable fgf.prj_in_hom(5) by auto
              show "C.span 𝗉1[f.leg0, f.dsrc] (η.chine  𝗉0[f.leg0, f.dsrc])"
                using chine_unit_in_hom by auto
              show "C.dom f.leg0 = C.cod 𝗉1[f.leg0, f.dsrc]" by simp
              show "f.leg0  𝗉1[f.leg0, f.dsrc] = gf.leg1  η.chine  𝗉0[f.leg0, f.dsrc]"
                by (metis C.comp_assoc C.pullback_commutes' η.cod_trg_eq_dom_trg
                    η.dom.leg_simps(1) η.leg1_commutes η_leg_simps(1-2,4)
                    C.cospan f.leg0 gf.leg1)
            qed
            thus ?thesis by simp
          qed
          finally show ?thesis by simp
        qed
        moreover have "C.seq fgf.Prj00 (chine_hcomp f η)"
          using chine_hcomp_props(1) by (metis 2 3 4 C.match_2 C.seqE)
        moreover have "C.seq (chine_hcomp f η) f.chine f.leg0, f.dsrc f.leg0"
          using chine_hcomp_props(1) by (metis 2 C.seqE)
        ultimately show ?thesis
          using C.comp_reduce by simp
      qed
      also have "... = gf.prj0  η.chine  𝗉0[f.leg0, f.dsrc]  f.chine f.leg0, f.dsrc f.leg0"
        using C.comp_assoc by simp
      also have "... = gf.prj0  η.chine  f.leg0"
        using C.comp_cod_arr f.leg0_commutes by simp
      finally show "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) = gf.prj0  η.chine  f.leg0"
        by simp

      have 1: "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) =
               𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε  gfg.chine_assoc  chine_hcomp η g 
                 g.leg1 g.dtrg, g.leg1 g.chine"
      proof -
        have "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) =
              Chn 𝗋[g]  Chn (g  ε)  Chn 𝖺[g, f, g]  Chn (η  g)  Chn 𝗅-1[g]"
          using antipar Chn_vcomp by auto
        also have "... = 𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε  gfg.chine_assoc  chine_hcomp η g 
                           g.leg1 g.dtrg, g.leg1 g.chine"
          using α_ide gf.composable fg.composable runit_ide_eq hcomp_def [of g ε]
                fg.composable hcomp_def [of η g] gf.composable lunit'_ide_eq
          by simp
        finally show ?thesis by blast
      qed
      hence 2: "C.arr (𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε  gfg.chine_assoc 
                       chine_hcomp η g  g.leg1 g.dtrg, g.leg1 g.chine)"
        by (metis arrI arr_char arrow_of_spans.chine_simps(1) triangle_in_hom(4))

      have "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) =
            𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε  gfg.chine_assoc  chine_hcomp η g 
              g.leg1 g.dtrg, g.leg1 g.chine"
        using 1 by simp
      also have
        "... = gfg.Prj1  gfg.chine_assoc  chine_hcomp η g  g.leg1 g.dtrg, g.leg1 g.chine"
      proof -
        have "𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε = 𝗉1[g.leg0, ε.dom.leg1]"
          by (metis C.comp_cod_arr ε_leg_simps(2) ε_leg_simps(4) arrI chine_hcomp_props(6)
                    fg.leg1_composite g.cod_simps(2) g.identity_arrow_of_spans_axioms
                    gfg.cospan_μν gfg.prj_simps(10) gfg.prj_simps(16) hseqE
                    identity_arrow_of_spans.chine_eq_apex seqE triangle_in_hom(4))
        also have "... = gfg.Prj1"
          using dom_char counit_simps hcomp_def fg.composable by simp
        finally have "𝗉1[g.leg0, g.dsrc]  chine_hcomp g ε = gfg.Prj1"
          by simp
        moreover have "C.seq 𝗉1[g.leg0, g.dsrc] (chine_hcomp g ε)"
          using chine_hcomp_props(1) [of g ε] gf.composable calculation gfg.prj_in_hom(4)
          by auto
        moreover have "C.seq (chine_hcomp g ε)
                             (gfg.chine_assoc  chine_hcomp η g  g.leg1 g.dtrg, g.leg1 g.chine)"
          using chine_hcomp_props(1) gf.composable 2 by (metis C.seqE)
        ultimately show ?thesis
          using C.comp_reduce by simp
      qed
      also have "... = gfg.Prj11  chine_hcomp η g  g.leg1 g.dtrg, g.leg1 g.chine"
        using C.comp_reduce [of gfg.Prj1 gfg.chine_assoc gfg.Prj11
                                "chine_hcomp η g  g.leg1 g.dtrg, g.leg1 g.chine"]
              2 gfg.prj_chine_assoc(1)
        by blast
      also have "... = (gf.prj1  η.chine  𝗉1[g.dtrg, g.leg1])  g.leg1 g.dtrg, g.leg1 g.chine"
        by (metis C.comp_assoc η_leg_simps(1) η_leg_simps(3) arrI chine_hcomp_props(6)
                  g.cod_simps(3) gf.leg0_composite gfg.cospan_νπ hseqE seqE triangle_in_hom(4))
      also have "... = gf.prj1  η.chine  𝗉1[g.dtrg, g.leg1]  g.leg1 g.dtrg, g.leg1 g.chine"
        using C.comp_assoc by simp
      also have "... = gf.prj1  η.chine  g.leg1"
        using C.comp_cod_arr g.leg1_commutes by simp
      finally show "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) = gf.prj1  η.chine  g.leg1"
        by simp
    qed

  end

  subsection "Maps in Span(C)"

  text ‹
    In this section, we chararacterize the maps (\emph{i.e}~the left adjoints)
    in a span bicategory.  This is Proposition 2 of cite"carboni-et-al".
  ›

  context span_bicategory
  begin

    abbreviation adjoint_of_map
    where "adjoint_of_map f  Chn = Chn f,
                               Dom = Leg0 = Leg1 (Dom f), Leg1 = Leg0 (Dom f),
                               Cod = Leg0 = Leg1 (Dom f), Leg1 = Leg0 (Dom f)"

    abbreviation unit_for_map
    where "unit_for_map f  Chn = C.inv (Leg0 (Dom f))
                                      Leg1 (Dom f), Leg1 (Dom f)
                                    C.inv (Leg0 (Dom f)),
                             Dom = Dom (src f),
                             Cod = Dom (hcomp (adjoint_of_map f) f)"

    abbreviation counit_for_map
    where "counit_for_map f  Chn = Leg1 (Dom f)  𝗉0[Leg0 (Dom f), Leg0 (Dom f)],
                               Dom = Dom (hcomp f (adjoint_of_map f)),
                               Cod = Dom (trg f)"

    lemma is_left_adjoint_char:
    shows "is_left_adjoint f  ide f  C.iso (Leg0 (Dom f))"
    and "is_left_adjoint f 
           adjunction_in_bicategory vcomp hcomp assoc unit src trg f
              (adjoint_of_map f) (unit_for_map f) (counit_for_map f)"
    proof
      show 1: "is_left_adjoint f  ide f  C.iso (Leg0 (Dom f))"
      proof
        assume f: "is_left_adjoint f"
        obtain g η ε where adj: "adjunction_in_bicategory vcomp hcomp assoc unit src trg f g η ε"
          using f adjoint_pair_def by blast
        interpret adjunction_in_bicategory vcomp hcomp assoc unit src trg f g η ε
          using adj by auto
        show "ide f" by simp

        interpret f: identity_arrow_of_spans C f
          using ide_char' [of f] by auto
        interpret g: identity_arrow_of_spans C g
          using ide_char' [of g] by auto

        interpret gf: two_composable_identity_arrows_of_spans C prj0 prj1 g f
          using antipar by (unfold_locales, auto)
        interpret fg: two_composable_identity_arrows_of_spans C prj0 prj1 f g
          using antipar by (unfold_locales, auto)

        interpret fgf: three_composable_identity_arrows_of_spans C prj0 prj1 f g f ..

        interpret src_f: arrow_of_spans C src f
          using arr_char gf.are_arrows(2) by blast
        interpret src_f: identity_arrow_of_spans C src f
          using ide_char ide_src src_def by (unfold_locales, simp)

        interpret η: arrow_of_spans C η
          using arr_char unit_in_hom by auto
        interpret ε: arrow_of_spans C ε
          using arr_char counit_in_hom by auto

        interpret adjunction_data_in_span_bicategory C prj0 prj1 f g η ε
          ..
        show "C.iso f.leg0"
        proof -
          have "C.section f.leg0"
          proof -
            have "f.chine = (gf.prj0  η.chine)  f.leg0"
              using triangle_left' Chn_triangle_eq(1) C.comp_assoc by simp
            thus ?thesis
              using f.chine_is_identity by auto
          qed
          moreover have "C.retraction f.leg0"
            using C.retractionI [of f.leg0 "gf.prj0  η.chine"] hcomp_def C.comp_assoc
                  η.leg0_commutes gf.leg0_composite η_leg_simps
            by auto
          ultimately show ?thesis
            by (simp add: C.iso_iff_section_and_retraction)
        qed
      qed
      have 2: "ide f  C.iso (Leg0 (Dom f)) 
                 adjunction_in_bicategory vcomp hcomp assoc unit src trg f
                   (adjoint_of_map f) (unit_for_map f) (counit_for_map f)"

        text ‹
          The right adjoint g› is obtained by exchanging the legs of f›.
          The unit is obtained by tupling C.inv f.leg0› with itself,
          via the pullback of f.leg1› with itself.
          The counit is given by the legs of f ⋆ g›, which are equal,
          because the two legs of a pullback of the isomorphism f.leg0›
          with itself must be equal.
          It then remains to verify the triangle identities.
      ›

      proof -
        assume f: "ide f  C.iso (Leg0 (Dom f))"
        interpret f: identity_arrow_of_spans C f
          using f ide_char' by auto
        interpret Dom_src: span_in_category C Leg0 = f.dsrc, Leg1 = f.dsrc
          using f by (unfold_locales, auto)
        interpret Dom_trg: span_in_category C Leg0 = f.dtrg, Leg1 = f.dtrg
          using f by (unfold_locales, auto)

        define g where "g = adjoint_of_map f"
        interpret Dom_g: span_in_category C Leg0 = f.leg1, Leg1 = f.leg0
          by (unfold_locales, simp)
        interpret g: arrow_of_spans C g
          unfolding g_def
          using Dom_g.apex_def f.leg0_commutes f.leg1_commutes
          by (unfold_locales, auto)
        interpret g: identity_arrow_of_spans C g
          using g_def
          by (unfold_locales, auto)
        have ide_g: "ide g"
          using f ide_char g.arrow_of_spans_axioms by simp

        interpret fg: two_composable_arrows_of_spans C prj0 prj1 f g
          apply unfold_locales
          using g_def src_def trg_def arr_char f.arrow_of_spans_axioms g.arrow_of_spans_axioms
          by auto
        interpret fg: two_composable_identity_arrows_of_spans C prj0 prj1 f g
          ..
        interpret gf: two_composable_arrows_of_spans C prj0 prj1 g f
          apply unfold_locales
          using g_def src_def trg_def arr_char f.arrow_of_spans_axioms g.arrow_of_spans_axioms
          by auto
        interpret gf: two_composable_identity_arrows_of_spans C prj0 prj1 g f
          ..
        have hcomp_fg_eq: "hcomp f g = Chn = f.leg0 ↓↓ f.leg0,
                                         Dom = Leg0 = f.leg1  𝗉1[f.leg0, f.leg0],
                                                Leg1 = f.leg1  𝗉1[f.leg0, f.leg0],
                                         Cod = Leg0 = f.leg1  𝗉1[f.leg0, f.leg0],
                                                Leg1 = f.leg1  𝗉1[f.leg0, f.leg0]"
          using f g_def hcomp_def fg.composable src_def trg_def arr_char f.arrow_of_spans_axioms
                g.arrow_of_spans_axioms chine_hcomp_def gf.are_identities(1) chine_hcomp_ide_ide
                C.pullback_iso_self
          by auto
        have hcomp_gf_eq: "hcomp g f = Chn = f.leg1 ↓↓ f.leg1,
                                         Dom = Leg0 = f.leg0  𝗉0[f.leg1, f.leg1],
                                                Leg1 = f.leg0  𝗉1[f.leg1, f.leg1],
                                         Cod = Leg0 = f.leg0  𝗉0[f.leg1, f.leg1],
                                                Leg1 = f.leg0  𝗉1[f.leg1, f.leg1]"
          using g_def hcomp_def gf.composable src_def trg_def chine_hcomp_ide_ide
                arr_char f.arrow_of_spans_axioms g.arrow_of_spans_axioms ide_char
          by simp

        define η where "η = unit_for_map f"
        interpret Dom_gf: span_in_category C Leg0 = f.leg0  𝗉0[f.leg1, f.leg1],
                                               Leg1 = f.leg0  𝗉1[f.leg1, f.leg1]
          by (unfold_locales, simp_all)
        interpret η: arrow_of_spans C η
          using f g_def η_def hcomp_def src_def trg_def f.arrow_of_spans_axioms
                g.arrow_of_spans_axioms arr_char C.comp_arr_inv'
                C.tuple_in_hom [of f.leg1 f.leg1 "C.inv f.leg0" "C.inv f.leg0"]
                Dom_src.apex_def Dom_gf.apex_def
          apply unfold_locales by (simp_all add: C.comp_assoc)
        have unit_in_hom: "«η : src f  hcomp g f»"
        proof
          show 1: "arr η"
            using arr_char η.arrow_of_spans_axioms by simp
          show "dom η = src f"
            using 1 η_def dom_char src_def Dom_src.apex_def by simp
          show "cod η = hcomp g f"
            using 1 η_def g_def cod_char hcomp_gf_eq Dom_gf.apex_def by simp
        qed

        define ε where "ε = counit_for_map f"
        interpret Dom_fg: span_in_category C Leg0 = f.leg1  𝗉1[f.leg0, f.leg0],
                                               Leg1 = f.leg1  𝗉1[f.leg0, f.leg0]
          by (unfold_locales, simp_all)
        interpret ε: arrow_of_spans C ε
          using f g_def ε_def hcomp_def src_def trg_def f.arrow_of_spans_axioms
                g.arrow_of_spans_axioms arr_char C.comp_cod_arr C.pullback_iso_self
                Dom_trg.apex_def Dom_fg.apex_def
          apply unfold_locales by auto
        have counit_in_hom: "«ε : hcomp f g  trg f»"
        proof
          show 1: "arr ε"
            using arr_char ε.arrow_of_spans_axioms by simp
          show "cod ε = trg f"
            using 1 ε_def cod_char trg_def Dom_trg.apex_def by simp
          show "dom ε = hcomp f g"
            using 1 g_def ε_def dom_char hcomp_fg_eq Dom_fg.apex_def by simp
        qed
        interpret adj: adjunction_data_in_bicategory vcomp hcomp assoc unit src trg f g η ε
          using f ide_g unit_in_hom counit_in_hom gf.composable
          by (unfold_locales, simp_all)
        interpret adjunction_data_in_span_bicategory C prj0 prj1 f g η ε
          ..
        have triangle_left: "(ε  f)  𝖺-1[f, g, f]  (f  η) = 𝗅-1[f]  𝗋[f]"
        proof -
          have "𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f] = f"
          proof (intro arr_eqI)
            show "par (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) f"
              using f ide_in_hom [of f] adj.triangle_in_hom(3)
              by (metis (no_types, lifting) in_homE)
            show "Chn (𝗅[f]  (ε  f)  𝖺-1[f, g, f]  (f  η)  𝗋-1[f]) = f.chine"
              using f g_def η_def Chn_triangle_eq(1) C.comp_tuple_arr C.comp_inv_arr' by simp
          qed
          thus ?thesis
            using adj.triangle_equiv_form by simp
        qed
        have triangle_right: "(g  ε)  𝖺[g, f, g]  (η  g) = 𝗋-1[g]  𝗅[g]"
        proof -
          have "𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g] = g"
          proof (intro arr_eqI)
            show "par (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) g"
              using adj.ide_right ide_in_hom [of g] adj.triangle_in_hom(4)
              by (metis (no_types, lifting) in_homE)
            show "Chn (𝗋[g]  (g  ε)  𝖺[g, f, g]  (η  g)  𝗅-1[g]) = g.chine"
              using f g_def η_def Chn_triangle_eq(2) C.comp_tuple_arr C.comp_inv_arr' by simp
          qed
          thus ?thesis
            using adj.triangle_equiv_form by simp
        qed
        interpret adj: adjunction_in_bicategory vcomp hcomp assoc unit src trg f g η ε
          using triangle_left triangle_right by (unfold_locales, simp_all)
        show "adjunction_in_bicategory vcomp hcomp assoc unit src trg f g η ε" ..
      qed
      show "ide f  C.iso (Leg0 (Dom f))  is_left_adjoint f"
        using 2 adjoint_pair_def by blast
      show "is_left_adjoint f  adjunction_in_bicategory vcomp hcomp assoc unit src trg f
              (adjoint_of_map f) (unit_for_map f) (counit_for_map f)"
        using 1 2 by blast
    qed

  end

end