Theory CategoryOfTransitions

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

section "Categories of Transitions"

theory CategoryOfTransitions
imports Main Category3.EpiMonoIso CategoryWithBoundedPushouts
        ResiduatedTransitionSystem.ResiduatedTransitionSystem
begin

  text‹
    A category of transitions is a category with bounded pushouts in which every
    arrow is an epimorphism and the only isomorphisms are identities.
  ›

  locale category_of_transitions =
    category_with_bounded_pushouts +
  assumes arr_implies_epi: "arr t ⟹ epi t"
  and iso_implies_ide: "iso t ⟹ ide t"
  begin

    (* TODO: Move with rest of commutative_square facts (currently CategoryWithPullbacks). *)
    lemma commutative_square_sym:
    shows "commutative_square f g h k ⟹ commutative_square g f k h"
      by auto

    text ‹
      In this setting, pushouts are uniquely determined.
    ›

    sublocale elementary_category_with_bounded_pushouts C inj0 inj1
      using extends_to_elementary_category_with_bounded_pushouts by blast

    lemma pushouts_unique:
    assumes "pushout_square f g h k"
    shows "f = 𝗂1[h, k]" and "g = 𝗂0[h, k]"
    proof -
      obtain w where w: "w ⋅ 𝗂1[h, k] = f ∧ w ⋅ 𝗂0[h, k] = g"
        using assms pushout_universal pushout_square_def by meson
      obtain w' where w': "w' ⋅ f = 𝗂1[h, k] ∧ w' ⋅ g = 𝗂0[h, k]"
        using assms pushout_universal pushout_square_def pushout_commutes 
          bounded_spanI
        by meson
      have 1: "ide w"
      proof -
        have "commutative_square f g h k"
          using assms pushout_square_def by blast
        hence "ide (w ⋅ w')"
          using assms w w' comp_cod_arr ide_char' comp_assoc
          apply (elim commutative_squareE)
          by (metis arr_implies_epi epi_cancel seqE)
        thus ?thesis
          by (metis ideD(1) ide_is_iso inv_comp_right(2) iso_iff_section_and_epi
              sectionI seqE arr_implies_epi iso_implies_ide)
      qed
      show "f = 𝗂1[h, k]" and "g = 𝗂0[h, k]"
        using 1 w w' by (metis comp_ide_arr ext null_is_zero(2))+
    qed

    lemma inj_sym:
    shows "𝗂0[k, h] = 𝗂1[h, k]"
    proof -
      have "¬ bounded_span h k ⟹ ?thesis"
        using inj0_ext [of k h] inj1_ext [of h k] bounded_span_sym by metis
      moreover have "bounded_span h k ⟹ ?thesis"
      proof -
        assume 1: "bounded_span h k"
        have "(∃l. l ⋅ 𝗂1[h, k] = 𝗂0[k, h]) ∧ (∃l'. l' ⋅ 𝗂0[k, h] = 𝗂1[h, k])"
          by (meson 1 bounded_span_sym commutative_square_sym
              pushout_commutes pushout_universal)
        moreover have "epi 𝗂0[k, h] ∧ epi 𝗂1[h, k]"
          by (meson 1 arr_implies_epi bounded_span_sym
              commutative_squareE pushout_commutes)
        ultimately show ?thesis
          by (metis arr_implies_epi iso_iff_section_and_epi comp_cod_arr
              comp_ide_arr epi_cancel epi_implies_arr ide_cod
              iso_implies_ide comp_assoc sectionI seqE)
      qed
      ultimately show ?thesis by auto
    qed

    lemma inj_arr_self:
    assumes "arr t"
    shows "𝗂0[t, t] = cod t" and "𝗂1[t, t] = cod t"
    proof -
      have 1: "pushout_square (cod t) (cod t) t t"
        using assms comp_arr_dom pushout_universal
        apply (intro pushout_squareI)
            apply auto[4]
        apply auto 
         apply (metis commutative_squareE inj_sym)
        by (metis ide_cod commutative_squareE comp_arr_ide)
      show "𝗂0[t, t] = cod t" and "𝗂1[t, t] = cod t"
        using 1 pushouts_unique by auto
    qed

    lemma inj_arr_dom:
    assumes "arr t"
    shows "𝗂0[t, dom t] = t" and "𝗂1[t, dom t] = cod t"
    proof -
      have 1: "pushout_square (cod t) t t (dom t)"
        using assms comp_arr_dom comp_cod_arr pushout_universal
        apply (intro pushout_squareI)
            apply auto[4]
        apply auto
         apply (metis cod_dom commutative_squareE)
        by (metis arr_implies_epi commutative_squareE epi_cancel)
      show "𝗂0[t, dom t] = t" and "𝗂1[t, dom t] = cod t"
        using 1 pushouts_unique by auto
    qed

    lemma eq_iff_ide_inj:
    assumes "span t u"
    shows "t = u ⟷ ide 𝗂0[t, u] ∧ ide 𝗂0[u, t]"
    proof
      show "t = u ⟹ ide 𝗂0[t, u] ∧ ide 𝗂0[u, t]"
        using assms by (simp add: inj_arr_self(1))
      show "ide 𝗂0[t, u] ∧ ide 𝗂0[u, t] ⟹ t = u"
        by (metis (no_types, lifting) comp_cod_arr commutative_squareE
            ide_char ide_def inj0_ext inj_sym pushout_commutes)
    qed

    lemma inj_comp:
    assumes "bounded_span t (v ⋅ u)"
    shows "𝗂0[t, v ⋅ u] = 𝗂0[𝗂0[t, u], v]"
    and "𝗂0[v ⋅ u, t] = 𝗂0[v, 𝗂0[t, u]] ⋅ 𝗂0[u, t]"
    proof -
      obtain w x where wx: "seq w t ∧ w ⋅ t = x ⋅ v ⋅ u"
        using assms by blast
      have 1: "seq w t ∧ w ⋅ t = (x ⋅ v) ⋅ u"
        using wx comp_assoc by auto
      have 2: "pushout_square 𝗂0[u, t] 𝗂0[t, u] t u"
        by (metis (full_types) 1 bounded_span_def cod_comp
            commutative_squareI dom_comp has_bounded_pushouts inj_sym seqE)
      have 3: "pushout_square 𝗂0[v, 𝗂0[t, u]] 𝗂0[𝗂0[t, u], v] 𝗂0[t, u] v"
      proof -
        have 4: "commutative_square w (x ⋅ v) t u"
          using wx comp_assoc
          by (metis (mono_tags, lifting) cod_comp commutative_square_def
              dom_comp seqE)
        obtain l where l: "l ⋅ 𝗂0[u, t] = w ∧ l ⋅ 𝗂0[t, u] = x ⋅ v"
          using 2 4 pushout_square_def [of "𝗂0[u, t]" "𝗂0[t, u]" t u] by blast
        have "bounded_span 𝗂0[t, u] v"
          by (metis (full_types) 1 l bounded_spanI cod_comp
              commutative_squareI dom_comp seqE)
        thus ?thesis
          using assms has_bounded_pushouts inj_sym by auto
      qed
      show "𝗂0[t, v ⋅ u] = 𝗂0[𝗂0[t, u], v]"
        using assms 2 3 composition_of_pushouts pushouts_unique
        by (metis (full_types))
      show "𝗂0[v ⋅ u, t] = 𝗂0[v, 𝗂0[t, u]] ⋅ 𝗂0[u, t]"
        using assms 2 3 composition_of_pushouts pushouts_unique inj_sym
        by metis
    qed

    lemma inj_prefix:
    assumes "arr (u ⋅ t)"
    shows "𝗂0[u ⋅ t, t] = u" and "𝗂0[t, u ⋅ t] = cod u"
    proof -
      have 1: "bounded_span (u ⋅ t) t"
        by (metis assms ideD(1) ide_cod inj1_ext inj_arr_self(1)
            inj_comp(2) inj_sym not_arr_null seqE)
      show "𝗂0[u ⋅ t, t] = u"
        using assms 1
        by (metis bounded_span_sym seqE comp_arr_dom inj_arr_dom(1)
            inj_arr_self(1) inj_comp(2))
      show "𝗂0[t, u ⋅ t] = cod u"
        using 1
        by (metis assms bounded_span_sym seqE inj_arr_dom(2) inj_arr_self(1)
            inj_comp(1) inj_sym)
    qed

  end

section "Extensional RTS's with Composites as Categories"

  text ‹
    An extensional RTS with composites can be regarded as a category in an obvious way.
  ›

  locale extensional_rts_with_composites_as_category =
    A: extensional_rts_with_composites
  begin

    text ‹
      Because we've defined RTS composition to take its arguments in diagram order,
      the ordering has to be reversed to match the way it is done for categories.
    ›

    abbreviation comp
    where "comp ≡ λu t. t ⋅ u"

    interpretation Category.partial_magma comp
      using A.comp_null by unfold_locales metis
    interpretation Category.partial_composition comp ..

    lemma null_char:
    shows "null = A.null"
      by (metis A.comp_nullCC(1) null_is_zero(2))

    lemma ide_char:
    shows "ide a ⟷ A.ide a"
    proof
      assume a: "A.ide a"
      show "ide a"
      proof (unfold ide_def, intro conjI allI impI)
        show "a ⋅ a ≠ null"
          using a null_char by auto
        show "⋀t. t ⋅ a ≠ null ⟹ t ⋅ a = t"
          using a
          by (metis A.comp_def A.comp_is_composite_of(2) A.composable_def
              A.composite_of_def A.cong_char null_char)
        show "⋀t. a ⋅ t ≠ null ⟹ a ⋅ t = t"
          using a
          by (metis A.arr_comp A.ide_iff_trg_self A.comp_src_arr null_char
              A.comp_def A.arr_compEEC)
      qed
      next
      assume a: "ide a"
      show "A.ide a"
        using a
        by (metis A.arr_comp A.comp_def A.comp_eqI A.cong_reflexive
            ide_def null_char)
    qed

    lemma src_in_domains:
    assumes "A.arr t"
    shows "A.src t ∈ domains t"
      unfolding domains_def
      using assms ide_char null_char by force

    lemma trg_in_codomains:
    assumes "A.arr t"
    shows "A.trg t ∈ codomains t"
      unfolding codomains_def
      using assms ide_char null_char by force

    lemma arr_char:
    shows "arr = A.arr"
    proof
      fix t
      show "arr t ⟷ A.arr t"
      proof
        show "A.arr t ⟹ arr t"
          using src_in_domains trg_in_codomains arr_def by auto
        assume t: "arr t"
        have 1: "domains t ≠ {} ∨ codomains t ≠ {}"
          using t arr_def by simp
        show "A.arr t"
        proof (cases "domains t ≠ {}")
          case True
          obtain a where a: "a ∈ domains t"
            using True by auto
          show "A.arr t"
            using a t A.composable_iff_seq [of a t] A.comp_def domains_def
                  null_char
            by auto
          next
          case False
          obtain a where a: "a ∈ codomains t"
            using False 1 by auto
          show "A.arr t"
            using a t A.composable_iff_seq [of t a] A.comp_def codomains_def
                  null_char
            by auto
        qed
      qed
    qed

    lemma seq_char:
    shows "seq u t ⟷ A.seq t u"
      using arr_char by auto

    sublocale category comp
    proof
      show "⋀g f. f ⋅ g ≠ null ⟹ seq g f"
        using A.composable_iff_comp_not_null null_char seq_char by auto
      show "⋀f. (domains f ≠ {}) = (codomains f ≠ {})"
        using arr_char arr_def src_in_domains trg_in_codomains empty_iff by metis
      fix f g h
      show 1: "f ⋅ (g ⋅ h) = (f ⋅ g) ⋅ h"
        using A.comp_assocEC by blast
      show "⟦seq h g; seq (g ⋅ h) f⟧ ⟹ seq g f"
        using A.comp_assocEC seq_char by auto
      show "⟦seq h (f ⋅ g); seq g f⟧ ⟹ seq h g"
        by (metis 1 A.arr_compEEC arr_char)
      show "⟦seq g f; seq h g⟧ ⟹ seq (g ⋅ h) f"
        using seq_char by fastforce
    qed

    proposition is_category:
    shows "category comp"
      ..

    lemma cod_char:
    shows "cod = A.trg"
      unfolding A.trg_def
      by (metis arr_char cod_def cod_eqI' codomains_char null_char
          A.con_implies_arr(2) trg_in_codomains A.conI A.trg_def)

    lemma dom_char:
    shows "dom = A.src"
      unfolding A.src_def
      by (metis A.src_def arr_char arr_def dom_eqI' dom_def null_char
          src_in_domains)

    lemma arr_implies_epi:
    assumes "arr t"
    shows "epi t"
      using assms
      by (metis arr_char epiI A.comp_cancel_left)

    lemma iso_implies_ide:
    assumes "iso t"
    shows "ide t"
      by (metis A.ide_backward_stable A.src_ide arr_char arr_inv assms
          comp_inv_arr' dom_char dom_inv ide_char' iso_is_arr A.ide_src
          A.prfx_comp seqI)

  end

  section "Characterization"

  text ‹
    The categories arising from extensional RTS's with composites are categories
    of transitions.
  ›

  context extensional_rts_with_composites_as_category
  begin

    lemma has_bounded_pushouts:
    assumes "bounded_span h k"
    shows "pushout_square (k \\ h) (h \\ k) h k"
    proof
      have con: "h ⌢ k"
        using assms
        by (metis A.bounded_imp_conE A.cong_reflexive arr_char
            bounded_span_def commutative_squareE seqI)
      show "cospan (k \\ h) (h \\ k)"
        by (simp add: con A.apex_sym A.con_sym arr_char cod_char)
      show "span h k"
        using assms by blast
      show "dom (k \\ h) = cod h"
        using A.join_expansion(2) con seq_char by blast
      show "h ⋅ k \\ h = k ⋅ h \\ k"
        using A.diamond_commutes by blast
      show "⋀f g h k. commutative_square f g h k
                         ⟹ ∃!l. k \\ h ⋅ l = f ∧ h \\ k ⋅ l = g"
      proof -
        fix f g h k
        assume 1: "commutative_square f g h k"
        hence 2: "h ⋅ f = k ⋅ g"
          using dom_char cod_char by auto
        hence 3: "h ⌢ k"
          by (metis "1" A.bounded_imp_conE A.prfx_reflexive arr_char
              commutative_squareE seqI)
        let ?l = "(h ⋅ f) \\ (h ⊔ k)"
        have 4: "(k \\ h) ⋅ ?l = f"
        proof -
          have "A.joinable h k"
            using 3 by simp
          thus ?thesis
            by (metis 1 A.comp_assocEC A.comp_resid_prfx A.induced_arrow(2)
                A.join_expansion(1) A.seq_implies_arr_comp commutative_squareE
                seqI seq_char)
        qed
        moreover have "(h \\ k) ⋅ ?l = g"
          by (metis "1" A.comp_resid_prfx A.induced_arrow(2)
              A.seq_implies_arr_comp calculation commutative_squareE
              seqI seq_char)
        ultimately have "∃l. (k \\ h) ⋅ ?l = f ∧ (h \\ k) ⋅ ?l = g"
          by simp
        moreover have "⋀l'. (k \\ h) ⋅ l' = f ∧ (h \\ k) ⋅ l' = g ⟹ l' = ?l"
          by (metis 1 4 A.comp_cancel_left arr_char commutative_square_def)
        ultimately show "∃!l. (k \\ h) ⋅ l = f ∧ (h \\ k) ⋅ l = g" by auto
      qed
    qed

    sublocale category_of_transitions comp
      using has_bounded_pushouts arr_implies_epi iso_implies_ide
      by unfold_locales auto

    proposition is_category_of_transitions:
    shows "category_of_transitions comp"
      ..

  end

  text ‹
    Every category of transitions is derived from an underlying extensional RTS,
    obtained by using pushouts to define residuation.
  ›

  locale underlying_rts =
    C: category_of_transitions
  begin

    interpretation ResiduatedTransitionSystem.partial_magma ‹λh k. 𝗂0[h, k]›
      using C.inj0_ext C.inj1_ext C.commutative_squareE C.not_arr_null C.pushout_commutes
      by unfold_locales metis

    lemma null_char:
    shows "null = C.null"
      using null_eqI C.inj0_ext C.not_arr_null C.pushout_commutes
      by (metis C.commutative_squareE)

    interpretation residuation ‹λh k. 𝗂0[h, k]›
    proof
      show 0: "⋀t u. 𝗂0[t, u] ≠ null ⟹ 𝗂0[u, t] ≠ null"
        by (metis C.inj0_ext C.inj_sym C.not_arr_null C.pushout_commutes
            C.commutative_squareE null_char)
      show "⋀t u. 𝗂0[t, u] ≠ null ⟹ 𝗂0[𝗂0[t, u], 𝗂0[t, u]] ≠ null"
        by (metis C.commutative_squareE C.eq_iff_ide_inj C.ideD(1) C.inj0_ext
            C.not_arr_null C.pushout_commutes null_char)
      have *: "⋀t u v. ⟦𝗂0[t, u] ≠ null; 𝗂0[t, v] ≠ null; 𝗂0[𝗂0[v, t], 𝗂0[u, t]] ≠ null⟧
                          ⟹ ∃w. 𝗂0[𝗂0[v, t], 𝗂0[u, t]] = w ⋅ 𝗂0[𝗂0[v, u], 𝗂0[t, u]]"
      proof -
        fix t u v
        assume tu: "𝗂0[t, u] ≠ null" and tv: "𝗂0[t, v] ≠ null"
        and vt_ut: "𝗂0[𝗂0[v, t], 𝗂0[u, t]] ≠ null"
        have 1: "(𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u]) ⋅ u = (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v]) ⋅ v"
        proof -
          have "(𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u]) ⋅ u = 𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u] ⋅ u"
            using C.comp_assoc by simp
          also have "... =  𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[u, t] ⋅ t"
            using tu C.pushout_commutes
            by (metis C.commutative_squareE C.inj0_ext C.inj_sym null_char)
          also have "... = (𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[u, t]) ⋅ t"
            using C.comp_assoc by simp
          also have "... = (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[v, t]) ⋅ t"
            using vt_ut C.pushout_commutes
            by (metis (no_types, lifting) C.commutative_squareE C.inj0_ext C.inj_sym null_char)
          also have "... = 𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[v, t] ⋅ t"
            using C.comp_assoc by simp
          also have "... = 𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v] ⋅ v"
            using tv C.pushout_commutes
            by (metis C.commutative_squareE C.inj0_ext C.inj_sym null_char)
          also have "... = (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v]) ⋅ v"
            using C.comp_assoc by simp
          finally show ?thesis by blast
        qed
        have 2: "C.commutative_square (𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u])
                  (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v]) u v"
        proof -
          have "C.span u v"
            by (metis (mono_tags, opaque_lifting) C.commutative_square_def
                C.inj0_ext C.pushout_commutes null_char tu tv)
          moreover have "C.cospan (𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u])
                                  (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v])"
          proof (intro conjI)
            show 3: "C.seq 𝗂0[𝗂0[v, t], 𝗂0[u, t]] 𝗂0[t, u]"
            proof
              show "«𝗂0[t, u] : C.cod u → C.cod 𝗂0[u, t]»"
                using C.pushout_commutes [of t u]
                by (metis C.commutative_squareE C.in_homI C.inj0_ext C.inj_sym null_char tu)
              show "«𝗂0[𝗂0[v, t], 𝗂0[u, t]] : C.cod 𝗂0[u, t] → C.cod 𝗂0[𝗂0[v, t], 𝗂0[u, t]]»"
                using C.pushout_commutes [of "𝗂0[v, t]" "𝗂0[u, t]"]
                      C.arr_iff_in_hom C.commutative_square_def C.inj0_ext null_char vt_ut
                by force
            qed
            show 4: "C.seq 𝗂0[𝗂0[u, t], 𝗂0[v, t]] 𝗂0[t, v]"
              by (metis 1 3 C.dom_inj(1) C.inj0_ext C.seqE C.seqI calculation
                  C.dom_comp null_char tu)
            show "C.cod (𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u]) =
                  C.cod (𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v])"
              by (metis 3 4 C.cod_inj C.inj0_ext C.inj_sym C.cod_comp)
          qed
          moreover have "C.dom (𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u]) = C.cod u"
            by (metis C.dom_comp C.dom_inj(1) C.inj0_ext calculation(2)
                null_char tu)
          ultimately show ?thesis
            using 1 by blast
        qed
        hence "C.bounded_span u v"
          by blast
        obtain l where l: "l ⋅ 𝗂0[v, u] = 𝗂0[𝗂0[v, t], 𝗂0[u, t]] ⋅ 𝗂0[t, u] ∧
                           l ⋅ 𝗂0[u, v] = 𝗂0[𝗂0[u, t], 𝗂0[v, t]] ⋅ 𝗂0[t, v]"
          using 2 C.pushout_universal by (metis C.inj_sym)
        have 3: "C.commutative_square 𝗂0[𝗂0[v, t], 𝗂0[u, t]] l 𝗂0[t, u] 𝗂0[v, u]"
          using tu tv vt_ut l 2
          by (metis (mono_tags, lifting) C.cod_comp C.commutative_square_def
              C.dom_comp C.seqE)
        obtain w where "𝗂0[𝗂0[v, t], 𝗂0[u, t]] = w ⋅ 𝗂0[𝗂0[v, u], 𝗂0[t, u]] ∧
                        l = w ⋅ 𝗂0[𝗂0[t, u], 𝗂0[v, u]]"
          using 3 C.pushout_universal by (metis C.inj_sym)
        thus "∃w. 𝗂0[𝗂0[v, t], 𝗂0[u, t]] = w ⋅ 𝗂0[𝗂0[v, u], 𝗂0[t, u]]" by auto
      qed
      show "⋀t u v. 𝗂0[𝗂0[v, t], 𝗂0[u, t]] ≠ null
                       ⟹ 𝗂0[𝗂0[v, t], 𝗂0[u, t]] = 𝗂0[𝗂0[v, u], 𝗂0[t, u]]"
      proof -
        fix t u v
        assume vt_ut: "𝗂0[𝗂0[v, t], 𝗂0[u, t]] ≠ null"
        have tu: "𝗂0[t, u] ≠ null"
          using vt_ut
          by (metis ‹⋀u t. 𝗂0[t, u] ≠ null ⟹ 𝗂0[u, t] ≠ null› null_is_zero(2))
        have tv: "𝗂0[t, v] ≠ null"
          using vt_ut
          by (metis ‹⋀u t. 𝗂0[t, u] ≠ null ⟹ 𝗂0[u, t] ≠ null› null_is_zero(1))
        obtain w where w: "𝗂0[𝗂0[v, t], 𝗂0[u, t]] = w ⋅ 𝗂0[𝗂0[v, u], 𝗂0[t, u]]"
          using tu tv vt_ut * by blast
        have vu_tu: "𝗂0[𝗂0[v, u], 𝗂0[t, u]] ≠ null"
          using w null_char vt_ut by fastforce
        obtain w' where w': "𝗂0[𝗂0[v, u], 𝗂0[t, u]] = w' ⋅ 𝗂0[𝗂0[v, t], 𝗂0[u, t]]"
          using 0 vu_tu * null_is_zero(2) by metis
        have "C.ide (w ⋅ w')"
          using w w' vt_ut
          by (metis C.comp_cod_arr C.ext C.ide_cod C.inj_prefix(1-2) C.seqE
              null_char)
        hence "C.ide w"
          using w w'
          by (metis C.comp_arr_ide C.ide_compE C.inj_arr_dom(1) C.inj_prefix(2)
              C.seqE)
        thus "𝗂0[𝗂0[v, t], 𝗂0[u, t]] = 𝗂0[𝗂0[v, u], 𝗂0[t, u]]"
          using w C.comp_ide_arr
          by (metis C.ext null_char vt_ut)
      qed
    qed

    lemma con_char:
    shows "con t u ⟷ C.bounded_span t u"
      by (metis C.commutative_squareE C.inj0_ext C.not_arr_null
          C.pushout_commutes con_def null_char)

    lemma arr_char:
    shows "arr t ⟷ C.arr t"
      by (metis C.arr_cod C.inj_arr_self(1) C.not_arr_null C.pushout_commutes
          arr_def C.commutative_squareE con_char con_def null_char)

    lemma ide_char:
    shows "ide a ⟷ C.ide a"
      by (metis C.ide_char C.ide_char' C.ide_def C.inj_arr_self(1) arr_char ide_def
          null_char con_def ide_implies_arr)

    interpretation rts ‹λh k. 𝗂0[h, k]›
    proof
      show "⋀a t. ⟦ide a; con t a⟧ ⟹ 𝗂0[t, a] = t"
        using C.inj_arr_dom con_char ide_char by fastforce
      thus "⋀a t. ⟦ide a; con a t⟧ ⟹ ide 𝗂0[a, t]"
        by (metis con_sym cube ide_def con_def)
      show "⋀t. arr t ⟹ ide (trg t)"
        by (metis arr_char C.eq_iff_ide_inj ide_char resid_arr_self)
      thus "⋀t u. con t u ⟹ ∃a. ide a ∧ con a t ∧ con a u"
        using con_char ide_char
        by (metis C.ide_dom C.inj_arr_dom(1) C.pushout_commutes
            C.commutative_squareE con_implies_arr(1) con_sym arr_resid_iff_con)
      show "⋀t u v. ⟦ide 𝗂0[t, u]; con u v⟧ ⟹ con 𝗂0[t, u] 𝗂0[v, u]"
        by (metis (no_types, lifting) C.dom_inj(1) C.ideD(2) C.inj_arr_dom(1)
            arr_char con_char ide_char arr_resid_iff_con con_sym ide_implies_arr)
    qed

    interpretation extensional_rts ‹λh k. 𝗂0[h, k]›
      by unfold_locales
         (metis C.ideD(2) C.inj_sym C.pushout_commutes prfx_implies_con
                C.commutative_squareE C.comp_cod_arr con_char ide_char)

    lemma src_char:
    assumes "arr t"
    shows "src t = C.dom t"
      by (metis C.ide_dom C.inj_arr_dom(1) arr_char arr_resid_iff_con assms
          con_imp_eq_src ide_char src_ide)

    lemma trg_char:
    assumes "arr t"
    shows "trg t = C.cod t"
      by (metis assms C.inj_arr_self(1) resid_arr_self arr_char)

    lemma seq_char:
    shows "seq t u ⟷ C.seq u t"
      using seq_def sources_charWE targets_charWE arr_char src_char trg_char
      by auto

    lemma comp_char:
    shows "comp t u = u ⋅ t"
      by (metis C.cod_comp C.ext C.inj_arr_self(1) C.inj_prefix(1-2)
          arr_char composable_imp_seq cong_reflexive comp_def null_char
          prfx_decomp seq_char)

    sublocale extensional_rts_with_composites ‹λh k. 𝗂0[h, k]›
      by unfold_locales
         (metis C.not_arr_null composable_iff_comp_not_null comp_char null_char
           seq_char)

    proposition is_extensional_rts_with_composites:
    shows "extensional_rts_with_composites (λh k. 𝗂0[h, k])"
      ..

  end

end