Theory CZH_DG_Rel

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Rel› as a digraph›
theory CZH_DG_Rel
  imports CZH_DG_Small_DGHM
begin



subsection‹Background›


text‹
‹Rel› is usually defined as a category of sets and binary relations
(e.g., see Chapter I-7 in \<^cite>‹"mac_lane_categories_2010"›). However, there
is little that can prevent one from exposing ‹Rel› as a digraph and
provide additional structure gradually later. 
Thus, in this section, ‹α›-‹Rel› is defined as a digraph of sets 
and binary relations in ‹V⇩α›.
›

named_theorems dg_Rel_shared_cs_simps
named_theorems dg_Rel_shared_cs_intros

named_theorems dg_Rel_cs_simps
named_theorems dg_Rel_cs_intros



subsection‹Canonical arrow for \<^typ>‹V››

named_theorems arr_field_simps

definition ArrVal :: V where [arr_field_simps]: "ArrVal = 0"
definition ArrDom :: V where [arr_field_simps]: "ArrDom = 1⇩ℕ"
definition ArrCod :: V where [arr_field_simps]: "ArrCod = 2⇩ℕ"

lemma ArrVal_eq_helper:
  assumes "f = g"
  shows "f⦇ArrVal⦈⦇a⦈ = g⦇ArrVal⦈⦇a⦈"
  using assms by simp



subsection‹Arrow for ‹Rel››


subsubsection‹Definition and elementary properties›

locale arr_Rel = 𝒵 α + vfsequence T + ArrVal: vbrelation ‹T⦇ArrVal⦈› for α T +
  assumes arr_Rel_length[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: 
    "vcard T = 3⇩ℕ" 
    and arr_Rel_ArrVal_vdomain: "𝒟⇩∘ (T⦇ArrVal⦈) ⊆⇩∘ T⦇ArrDom⦈"
    and arr_Rel_ArrVal_vrange: "ℛ⇩∘ (T⦇ArrVal⦈) ⊆⇩∘ T⦇ArrCod⦈"
    and arr_Rel_ArrDom_in_Vset: "T⦇ArrDom⦈ ∈⇩∘ Vset α"
    and arr_Rel_ArrCod_in_Vset: "T⦇ArrCod⦈ ∈⇩∘ Vset α"

lemmas [dg_Rel_shared_cs_simps, dg_Rel_cs_simps] = arr_Rel.arr_Rel_length


text‹Components.›

lemma arr_Rel_components[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
  shows "[f, A, B]⇩∘⦇ArrVal⦈ = f"
    and "[f, A, B]⇩∘⦇ArrDom⦈ = A"
    and "[f, A, B]⇩∘⦇ArrCod⦈ = B"
  unfolding arr_field_simps by (simp_all add: nat_omega_simps)


text‹Rules.›

lemma (in arr_Rel) arr_Rel_axioms'[dg_cs_intros, dg_Rel_cs_intros]:
  assumes "α' = α"
  shows "arr_Rel α' T"
  unfolding assms by (rule arr_Rel_axioms)

mk_ide rf arr_Rel_def[unfolded arr_Rel_axioms_def]
  |intro arr_RelI|
  |dest arr_RelD[dest]|
  |elim arr_RelE[elim!]|

lemma (in 𝒵) arr_Rel_vfsequenceI: 
  assumes "vbrelation r" 
    and "𝒟⇩∘ r ⊆⇩∘ a"
    and "ℛ⇩∘ r ⊆⇩∘ b"
    and "a ∈⇩∘ Vset α"
    and "b ∈⇩∘ Vset α"
  shows "arr_Rel α [r, a, b]⇩∘"
  by (intro arr_RelI) 
    (insert assms, auto simp: nat_omega_simps arr_Rel_components)


text‹Elementary properties.›

lemma arr_Rel_eqI:
  assumes "arr_Rel α S" 
    and "arr_Rel α T"
    and "S⦇ArrVal⦈ = T⦇ArrVal⦈"
    and "S⦇ArrDom⦈ = T⦇ArrDom⦈"
    and "S⦇ArrCod⦈ = T⦇ArrCod⦈"
  shows "S = T"
proof-
  interpret S: arr_Rel α S by (rule assms(1))
  interpret T: arr_Rel α T by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    show "𝒟⇩∘ S = 𝒟⇩∘ T" 
      by (simp add: S.vfsequence_vdomain T.vfsequence_vdomain dg_Rel_cs_simps) 
    have dom_lhs: "𝒟⇩∘ S = 3⇩ℕ" 
      by (simp add: S.vfsequence_vdomain dg_Rel_cs_simps)
    show "a ∈⇩∘ 𝒟⇩∘ S ⟹ S⦇a⦈ = T⦇a⦈" for a 
      by (unfold dom_lhs, elim_in_numeral, insert assms)
        (auto simp: arr_field_simps)
  qed auto
qed

lemma (in arr_Rel) arr_Rel_def: "T = [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]⇩∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ T = 3⇩ℕ" by (simp add: vfsequence_vdomain dg_Rel_cs_simps)
  have dom_rhs: "𝒟⇩∘ [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]⇩∘ = 3⇩ℕ"
    by (simp add: nat_omega_simps)
  then show "𝒟⇩∘ T = 𝒟⇩∘ [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]⇩∘"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈⇩∘ 𝒟⇩∘ T ⟹ T⦇a⦈ = [T⦇ArrVal⦈, T⦇ArrDom⦈, T⦇ArrCod⦈]⇩∘⦇a⦈" for a
    unfolding dom_lhs
    by elim_in_numeral (simp_all add: arr_field_simps nat_omega_simps)
qed (auto simp: vsv_axioms)


text‹Size.›

lemma (in arr_Rel) arr_Rel_ArrVal_in_Vset: "T⦇ArrVal⦈ ∈⇩∘ Vset α"
proof-
  from arr_Rel_ArrVal_vdomain arr_Rel_ArrDom_in_Vset have 
    "𝒟⇩∘ (T⦇ArrVal⦈) ∈⇩∘ Vset α"
    by auto
  moreover from arr_Rel_ArrVal_vrange arr_Rel_ArrCod_in_Vset have 
    "ℛ⇩∘ (T⦇ArrVal⦈) ∈⇩∘ Vset α"
    by auto
  ultimately show "T⦇ArrVal⦈ ∈⇩∘ Vset α" 
    by (simp add: ArrVal.vbrelation_Limit_in_VsetI)
qed

lemma (in arr_Rel) arr_Rel_in_Vset: "T ∈⇩∘ Vset α"
proof-
  note [dg_Rel_cs_intros] = 
    arr_Rel_ArrVal_in_Vset arr_Rel_ArrDom_in_Vset arr_Rel_ArrCod_in_Vset
  show ?thesis
    by (subst arr_Rel_def)
      (cs_concl cs_shallow cs_intro: dg_Rel_cs_intros V_cs_intros) 
qed

lemma small_arr_Rel[simp]: "small {T. arr_Rel α T}"
  by (rule down[of _ ‹Vset α›]) (auto intro!: arr_Rel.arr_Rel_in_Vset)


text‹Other elementary properties.›

lemma set_Collect_arr_Rel[simp]: 
  "x ∈⇩∘ set (Collect (arr_Rel α)) ⟷ arr_Rel α x" 
  by auto

lemma (in arr_Rel) arr_Rel_ArrVal_vsubset_ArrDom_ArrCod:
  "T⦇ArrVal⦈ ⊆⇩∘ T⦇ArrDom⦈ ×⇩∘ T⦇ArrCod⦈"
proof
  fix ab assume "ab ∈⇩∘ T⦇ArrVal⦈"
  then obtain a b where "ab = ⟨a, b⟩" 
    and "a ∈⇩∘ 𝒟⇩∘ (T⦇ArrVal⦈)" 
    and "b ∈⇩∘ ℛ⇩∘ (T⦇ArrVal⦈)" 
    by (blast elim: ArrVal.vbrelation_vinE)
  with arr_Rel_ArrVal_vdomain arr_Rel_ArrVal_vrange show 
    "ab ∈⇩∘ T⦇ArrDom⦈ ×⇩∘ T⦇ArrCod⦈"
    by auto
qed


subsubsection‹Composition›


text‹See Chapter I-7 in \<^cite>‹"mac_lane_categories_2010"›.›

definition comp_Rel :: "V ⇒ V ⇒ V" (infixl ‹∘⇩R⇩e⇩l› 55)
  where "comp_Rel S T = [S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈, T⦇ArrDom⦈, S⦇ArrCod⦈]⇩∘"


text‹Components.›

lemma comp_Rel_components:
  shows "(S ∘⇩R⇩e⇩l T)⦇ArrVal⦈ = S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: 
      "(S ∘⇩R⇩e⇩l T)⦇ArrDom⦈ = T⦇ArrDom⦈"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
      "(S ∘⇩R⇩e⇩l T)⦇ArrCod⦈ = S⦇ArrCod⦈"
  unfolding comp_Rel_def arr_field_simps by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemma comp_Rel_vsv[dg_Rel_shared_cs_intros, dg_Rel_cs_intros]: 
  "vsv (S ∘⇩R⇩e⇩l T)"
  unfolding comp_Rel_def by auto

lemma arr_Rel_comp_Rel[dg_Rel_cs_intros]:
  assumes "arr_Rel α S" and "arr_Rel α T"
  shows "arr_Rel α (S ∘⇩R⇩e⇩l T)"
proof-
  interpret S: arr_Rel α S by (rule assms(1))
  interpret T: arr_Rel α T by (rule assms(2))
  show ?thesis
  proof(intro arr_RelI)
    show "vfsequence (S ∘⇩R⇩e⇩l T)" unfolding comp_Rel_def by simp
    show "vcard (S ∘⇩R⇩e⇩l T) = 3⇩ℕ"
      unfolding comp_Rel_def by (simp add: nat_omega_simps)
    from T.arr_Rel_ArrVal_vdomain show 
      "𝒟⇩∘ ((S ∘⇩R⇩e⇩l T)⦇ArrVal⦈) ⊆⇩∘ (S ∘⇩R⇩e⇩l T)⦇ArrDom⦈"
      unfolding comp_Rel_components by auto
    show "ℛ⇩∘ ((S ∘⇩R⇩e⇩l T)⦇ArrVal⦈) ⊆⇩∘ (S ∘⇩R⇩e⇩l T)⦇ArrCod⦈"
      unfolding comp_Rel_components 
    proof(intro vsubsetI)
      fix z assume "z ∈⇩∘ ℛ⇩∘ (S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈)"
      then obtain x y where "⟨y, z⟩ ∈⇩∘ S⦇ArrVal⦈" and "⟨x, y⟩ ∈⇩∘ T⦇ArrVal⦈"
        by (meson vcomp_obtain_middle vrange_iff_vdomain)
      with S.arr_Rel_ArrVal_vrange show "z ∈⇩∘ S⦇ArrCod⦈" by auto
    qed
  qed 
    (
      auto simp: 
        comp_Rel_components T.arr_Rel_ArrDom_in_Vset S.arr_Rel_ArrCod_in_Vset
    ) 
qed

lemma arr_Rel_comp_Rel_assoc[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
  "(H ∘⇩R⇩e⇩l G) ∘⇩R⇩e⇩l F = H ∘⇩R⇩e⇩l (G ∘⇩R⇩e⇩l F)" 
  by (simp add: comp_Rel_def vcomp_assoc arr_field_simps nat_omega_simps)


subsubsection‹Inclusion arrow›


text‹
The definition of the inclusion arrow is based on the concept of the 
inclusion map, e.g., see \<^cite>‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Inclusion_map}
}›

definition "incl_Rel A B = [vid_on A, A, B]⇩∘"


text‹Components.›

lemma incl_Rel_components:
  shows "incl_Rel A B⦇ArrVal⦈ = vid_on A"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "incl_Rel A B⦇ArrDom⦈ = A"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "incl_Rel A B⦇ArrCod⦈ = B"
  unfolding incl_Rel_def arr_field_simps by (simp_all add: nat_omega_simps)


text‹Arrow value.›

lemma incl_Rel_ArrVal_vsv[dg_Rel_shared_cs_intros, dg_Rel_cs_intros]: 
  "vsv (incl_Rel A B⦇ArrVal⦈)"
  unfolding incl_Rel_components by simp

lemma incl_Rel_ArrVal_vdomain[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
  "𝒟⇩∘ (incl_Rel A B⦇ArrVal⦈) = A"
  unfolding incl_Rel_components by simp

lemma incl_Rel_ArrVal_app[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
  assumes "a ∈⇩∘ A"
  shows "incl_Rel A B⦇ArrVal⦈⦇a⦈ = a"
  using assms unfolding incl_Rel_components by simp


text‹Elementary properties.›

lemma incl_Rel_vfsequence[dg_Rel_shared_cs_intros, dg_Rel_cs_intros]: 
  "vfsequence (incl_Rel A B)" 
  unfolding incl_Rel_def by simp

lemma incl_Rel_vcard[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: 
  "vcard (incl_Rel A B) = 3⇩ℕ" 
  unfolding incl_Rel_def incl_Rel_def by (simp add: nat_omega_simps)

lemma (in 𝒵) arr_Rel_incl_RelI:
  assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "A ⊆⇩∘ B"
  shows "arr_Rel α (incl_Rel A B)"
proof(intro arr_RelI)
  show "vfsequence (incl_Rel A B)" unfolding incl_Rel_def by simp
  show "vcard (incl_Rel A B) = 3⇩ℕ" 
    unfolding incl_Rel_def by (simp add: nat_omega_simps)
qed (auto simp: incl_Rel_components assms)


subsubsection‹Identity›


text‹See Chapter I-7 in \<^cite>‹"mac_lane_categories_2010"›.›

definition id_Rel :: "V ⇒ V"
  where "id_Rel A = incl_Rel A A"


text‹Components.›

lemma id_Rel_components:
  shows "id_Rel A⦇ArrVal⦈ = vid_on A"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "id_Rel A⦇ArrDom⦈ = A"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "id_Rel A⦇ArrCod⦈ = A"
  unfolding id_Rel_def incl_Rel_components by simp_all


text‹Elementary properties.›

lemma id_Rel_vfsequence[dg_Rel_shared_cs_intros, dg_Rel_cs_intros]: 
  "vfsequence (id_Rel A)" 
  unfolding id_Rel_def by (simp add: dg_Rel_cs_intros)

lemma id_Rel_vcard[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: 
  "vcard (id_Rel A) = 3⇩ℕ" 
  unfolding id_Rel_def by (simp add: dg_Rel_cs_simps)

lemma (in 𝒵) arr_Rel_id_RelI:
  assumes "A ∈⇩∘ Vset α"
  shows "arr_Rel α (id_Rel A)"
  by (intro arr_RelI)
    (auto simp: id_Rel_components(1) assms dg_Rel_cs_intros dg_Rel_cs_simps)

lemma id_Rel_ArrVal_app[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]:
  assumes "a ∈⇩∘ A"
  shows "id_Rel A⦇ArrVal⦈⦇a⦈ = a"
  using assms unfolding id_Rel_components by simp

lemma arr_Rel_comp_Rel_id_Rel_left[dg_Rel_cs_simps]:
  assumes "arr_Rel α F" and "F⦇ArrCod⦈ = A"
  shows "id_Rel A ∘⇩R⇩e⇩l F = F"
proof(rule arr_Rel_eqI [of α])
  interpret F: arr_Rel α F by (rule assms(1))
  from assms(2) have "A ∈⇩∘ Vset α" by (auto intro: F.arr_Rel_ArrCod_in_Vset)
  with assms(1) show "arr_Rel α (id_Rel A ∘⇩R⇩e⇩l F)" 
    by (blast intro: F.arr_Rel_id_RelI intro!: arr_Rel_comp_Rel)
  from assms(2) F.arr_Rel_ArrVal_vrange show  
    "(id_Rel A ∘⇩R⇩e⇩l F)⦇ArrVal⦈ = F⦇ArrVal⦈"
    unfolding comp_Rel_components id_Rel_components by auto
qed 
  (
    use assms(2) in 
      ‹auto simp: assms(1) comp_Rel_components id_Rel_components›
  )

lemma arr_Rel_comp_Rel_id_Rel_right[dg_Rel_cs_simps]:
  assumes "arr_Rel α F" and "F⦇ArrDom⦈ = A"
  shows "F ∘⇩R⇩e⇩l id_Rel A = F"
proof(rule arr_Rel_eqI[of α])
  interpret F: arr_Rel α F by (rule assms(1))
  from assms(2) have "A ∈⇩∘ Vset α" by (auto intro: F.arr_Rel_ArrDom_in_Vset)
  with assms(1) show "arr_Rel α (F ∘⇩R⇩e⇩l id_Rel A)"
    by (blast intro: F.arr_Rel_id_RelI intro!: arr_Rel_comp_Rel)
  show "arr_Rel α F" by (simp add: assms(1))
  from assms(2) F.arr_Rel_ArrVal_vdomain show  
    "(F ∘⇩R⇩e⇩l id_Rel A)⦇ArrVal⦈ = F⦇ArrVal⦈"
    unfolding comp_Rel_components id_Rel_components by auto
qed (use assms(2) in ‹auto simp: comp_Rel_components id_Rel_components›)


subsubsection‹Converse›


text‹
As mentioned in Chapter I-7 in \<^cite>‹"mac_lane_categories_2010"›, the 
category ‹Rel› is usually equipped with an additional structure that is
the operation of taking a converse of a relation.
The operation is meant to be used almost exclusively as part of 
the dagger functor for ‹Rel›.
›

definition converse_Rel :: "V ⇒ V" ("(_¯⇩R⇩e⇩l)" [1000] 999)
  where "converse_Rel T = [(T⦇ArrVal⦈)¯⇩∘, T⦇ArrCod⦈, T⦇ArrDom⦈]⇩∘"

lemma converse_Rel_components:
  shows "T¯⇩R⇩e⇩l⦇ArrVal⦈ = (T⦇ArrVal⦈)¯⇩∘"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "T¯⇩R⇩e⇩l⦇ArrDom⦈ = T⦇ArrCod⦈"
    and [dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: "T¯⇩R⇩e⇩l⦇ArrCod⦈ = T⦇ArrDom⦈"
  unfolding converse_Rel_def arr_field_simps by (simp_all add: nat_omega_simps)


text‹Elementary properties.›

lemma (in arr_Rel) arr_Rel_converse_Rel: "arr_Rel α (T¯⇩R⇩e⇩l)"
proof(rule arr_RelI, unfold converse_Rel_components)
  show "vfsequence (T¯⇩R⇩e⇩l)" unfolding converse_Rel_def by simp
  show "vcard (T¯⇩R⇩e⇩l) = 3⇩ℕ"
    unfolding converse_Rel_def by (simp add: nat_omega_simps)
qed 
  (
    auto simp: 
      converse_Rel_components(1)   
      arr_Rel_ArrDom_in_Vset 
      arr_Rel_ArrCod_in_Vset
      arr_Rel_ArrVal_vdomain
      arr_Rel_ArrVal_vrange
  )

lemmas [dg_Rel_cs_intros] = 
  arr_Rel.arr_Rel_converse_Rel

lemma (in arr_Rel) 
  arr_Rel_converse_Rel_converse_Rel[dg_Rel_shared_cs_simps, dg_Rel_cs_simps]: 
  "(T¯⇩R⇩e⇩l)¯⇩R⇩e⇩l = T"
proof(rule arr_Rel_eqI)
  from arr_Rel_axioms show "arr_Rel α ((T¯⇩R⇩e⇩l)¯⇩R⇩e⇩l)"
    by (cs_intro_step dg_Rel_cs_intros)+
qed (simp_all add: arr_Rel_axioms converse_Rel_components)

lemmas [dg_Rel_cs_simps] = 
  arr_Rel.arr_Rel_converse_Rel_converse_Rel

lemma arr_Rel_converse_Rel_eq_iff[dg_Rel_cs_simps]:
  assumes "arr_Rel α F" and "arr_Rel α G"
  shows "F¯⇩R⇩e⇩l = G¯⇩R⇩e⇩l ⟷ F = G"
proof(rule iffI)
  show "F¯⇩R⇩e⇩l = G¯⇩R⇩e⇩l ⟹ F = G"
    by (metis arr_Rel.arr_Rel_converse_Rel_converse_Rel assms)
qed simp

lemma arr_Rel_converse_Rel_comp_Rel[dg_Rel_cs_simps]:
  assumes "arr_Rel α G" and "arr_Rel α F"
  shows "(F ∘⇩R⇩e⇩l G)¯⇩R⇩e⇩l = G¯⇩R⇩e⇩l ∘⇩R⇩e⇩l F¯⇩R⇩e⇩l"
proof(rule arr_Rel_eqI, unfold converse_Rel_components comp_Rel_components)
  from assms show "arr_Rel α (G¯⇩R⇩e⇩l ∘⇩R⇩e⇩l F¯⇩R⇩e⇩l)"
    by (cs_concl cs_shallow cs_intro: dg_Rel_cs_intros)
  from assms show "arr_Rel α ((F ∘⇩R⇩e⇩l G)¯⇩R⇩e⇩l)"
    by (cs_intro_step dg_Rel_cs_intros)+
qed (simp_all add: vconverse_vcomp)

lemma (in 𝒵) arr_Rel_converse_Rel_id_Rel: 
  assumes "c ∈⇩∘ Vset α"
  shows "arr_Rel α ((id_Rel c)¯⇩R⇩e⇩l)"
  using assms 𝒵_axioms 
  by (cs_concl cs_shallow cs_intro: dg_Rel_cs_intros arr_Rel_id_RelI)+

lemma (in 𝒵) arr_Rel_converse_Rel_id_Rel_eq_id_Rel[
    dg_Rel_shared_cs_simps, dg_Rel_cs_simps
    ]: 
  assumes "c ∈⇩∘ Vset α"
  shows "(id_Rel c)¯⇩R⇩e⇩l = id_Rel c"
  by (rule arr_Rel_eqI[of α], unfold converse_Rel_components id_Rel_components)
    (simp_all add: assms arr_Rel_id_RelI arr_Rel_converse_Rel_id_Rel)

lemmas [dg_Rel_shared_cs_simps, dg_Rel_cs_simps] = 
  𝒵.arr_Rel_converse_Rel_id_Rel_eq_id_Rel

lemma arr_Rel_comp_Rel_converse_Rel_left_if_v11[dg_Rel_cs_simps]:
  assumes "arr_Rel α T" 
    and "𝒟⇩∘ (T⦇ArrVal⦈) = A"
    and "T⦇ArrDom⦈ = A"
    and "v11 (T⦇ArrVal⦈)" 
    and "A ∈⇩∘ Vset α"
  shows "T¯⇩R⇩e⇩l ∘⇩R⇩e⇩l T = id_Rel A"
proof-
  interpret T: arr_Rel α T by (rule assms(1))
  interpret v11: v11 ‹T⦇ArrVal⦈› by (rule assms(4))
  show ?thesis
    by (rule arr_Rel_eqI[of α])
      (
        auto simp: 
          converse_Rel_components 
          comp_Rel_components 
          id_Rel_components 
          assms(1,3,5)
          arr_Rel.arr_Rel_converse_Rel 
          arr_Rel_comp_Rel  
          T.arr_Rel_id_RelI
          v11.v11_vcomp_vconverse[unfolded assms(2)] 
      )
qed

lemma arr_Rel_comp_Rel_converse_Rel_right_if_v11[dg_Rel_cs_simps]:
  assumes "arr_Rel α T" 
    and "ℛ⇩∘ (T⦇ArrVal⦈) = A"
    and "T⦇ArrCod⦈ = A"
    and "v11 (T⦇ArrVal⦈)" 
    and "A ∈⇩∘ Vset α"
  shows "T ∘⇩R⇩e⇩l T¯⇩R⇩e⇩l = id_Rel A"
proof-
  interpret T: arr_Rel α T by (rule assms(1))
  interpret v11: v11 ‹T⦇ArrVal⦈› by (rule assms(4))
  show ?thesis
    by (rule arr_Rel_eqI[of α])
      (
        auto simp: 
          assms(1,3,5)
          comp_Rel_components 
          converse_Rel_components 
          id_Rel_components 
          v11.v11_vcomp_vconverse'[unfolded assms(2)] 
          T.arr_Rel_id_RelI 
          arr_Rel.arr_Rel_converse_Rel
          arr_Rel_comp_Rel 
      )
qed



subsection‹‹Rel› as a digraph›


subsubsection‹Definition and elementary properties›

definition dg_Rel :: "V ⇒ V"
  where "dg_Rel α =
    [
      Vset α,
      set {T. arr_Rel α T},
      (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrDom⦈),
      (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrCod⦈)
    ]⇩∘"


text‹Components.›

lemma dg_Rel_components:
  shows "dg_Rel α⦇Obj⦈ = Vset α"
    and "dg_Rel α⦇Arr⦈ = set {T. arr_Rel α T}"
    and "dg_Rel α⦇Dom⦈ = (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrDom⦈)"
    and "dg_Rel α⦇Cod⦈ = (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrCod⦈)"
  unfolding dg_Rel_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object›

lemma dg_Rel_Obj_iff: "x ∈⇩∘ dg_Rel α⦇Obj⦈ ⟷ x ∈⇩∘ Vset α" 
  unfolding dg_Rel_components by auto


subsubsection‹Arrow›

lemma dg_Rel_Arr_iff[dg_Rel_cs_simps]: "x ∈⇩∘ dg_Rel α⦇Arr⦈ ⟷ arr_Rel α x" 
  unfolding dg_Rel_components by auto


subsubsection‹Domain›

mk_VLambda dg_Rel_components(3)
  |vsv dg_Rel_Dom_vsv[dg_Rel_cs_intros]|
  |vdomain dg_Rel_Dom_vdomain[dg_Rel_cs_simps]|
  |app dg_Rel_Dom_app[unfolded set_Collect_arr_Rel, dg_Rel_cs_simps]|

lemma dg_Rel_Dom_vrange: "ℛ⇩∘ (dg_Rel α⦇Dom⦈) ⊆⇩∘ dg_Rel α⦇Obj⦈"
  unfolding dg_Rel_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Rel) auto


subsubsection‹Codomain›

mk_VLambda dg_Rel_components(4)
  |vsv dg_Rel_Cod_vsv[dg_Rel_cs_intros]|
  |vdomain dg_Rel_Cod_vdomain[dg_Rel_cs_simps]|
  |app dg_Rel_Cod_app[unfolded set_Collect_arr_Rel, dg_Rel_cs_simps]|

lemma dg_Rel_Cod_vrange: "ℛ⇩∘ (dg_Rel α⦇Cod⦈) ⊆⇩∘ dg_Rel α⦇Obj⦈"
  unfolding dg_Rel_components
  by (rule vrange_VLambda_vsubset, unfold set_Collect_arr_Rel) auto


subsubsection‹Arrow with a domain and a codomain›


text‹Rules.›

lemma dg_Rel_is_arrI[dg_Rel_cs_intros]:
  assumes "arr_Rel α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  shows "S : A ↦⇘dg_Rel α⇙ B"
  using assms by (intro is_arrI, unfold dg_Rel_components) simp_all

lemma dg_Rel_is_arrD:
  assumes "S : A ↦⇘dg_Rel α⇙ B"
  shows "arr_Rel α S" 
    and [dg_cs_simps]: "S⦇ArrDom⦈ = A" 
    and [dg_cs_simps]: "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Rel_components by simp_all

lemma dg_Rel_is_arrE:
  assumes "S : A ↦⇘dg_Rel α⇙ B"
  obtains "arr_Rel α S" and "S⦇ArrDom⦈ = A" and "S⦇ArrCod⦈ = B"
  using is_arrD[OF assms] unfolding dg_Rel_components by simp_all


text‹Elementary properties.›

lemma (in 𝒵) dg_Rel_incl_Rel_is_arr:
  assumes "A ∈⇩∘ Vset α" and "B ∈⇩∘ Vset α" and "A ⊆⇩∘ B"
  shows "incl_Rel A B : A ↦⇘dg_Rel α⇙ B"
proof(rule dg_Rel_is_arrI)
  show "arr_Rel α (incl_Rel A B)" by (intro arr_Rel_incl_RelI assms)
qed (simp_all add: incl_Rel_components)

lemma (in 𝒵) dg_Rel_incl_Rel_is_arr'[dg_Rel_cs_intros]:
  assumes "A ∈⇩∘ Vset α" 
    and "B ∈⇩∘ Vset α" 
    and "A ⊆⇩∘ B"
    and "A' = A"
    and "B' = B"
  shows "incl_Rel A B : A' ↦⇘dg_Rel α⇙ B'"
  using assms(1-3) unfolding assms(4,5) by (rule dg_Rel_incl_Rel_is_arr)

lemmas [dg_Rel_cs_intros] = 𝒵.dg_Rel_incl_Rel_is_arr'

lemma dg_Rel_is_arr_ArrValE:
  assumes "T : A ↦⇘dg_Rel α⇙ B" and "ab ∈⇩∘ T⦇ArrVal⦈"
  obtains a b 
    where "ab = ⟨a, b⟩" and "a ∈⇩∘ 𝒟⇩∘ (T⦇ArrVal⦈)" and "b ∈⇩∘ ℛ⇩∘ (T⦇ArrVal⦈)"
proof-
  note T = dg_Rel_is_arrD[OF assms(1)]
  then interpret T: arr_Rel α T 
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = B"
    by simp_all
  from assms(2) obtain a b
    where "ab = ⟨a, b⟩" and "a ∈⇩∘ 𝒟⇩∘ (T⦇ArrVal⦈)" and "b ∈⇩∘ ℛ⇩∘ (T⦇ArrVal⦈)"
    by (blast elim: T.ArrVal.vbrelation_vinE)
  with that show ?thesis by simp
qed


subsubsection‹‹Rel› is a digraph›

lemma (in 𝒵) dg_Rel_Hom_vifunion_in_Vset:
  assumes "X ∈⇩∘ Vset α" and "Y ∈⇩∘ Vset α"
  shows "(⋃⇩∘A∈⇩∘X. ⋃⇩∘B∈⇩∘Y. Hom (dg_Rel α) A B) ∈⇩∘ Vset α"
proof-
  define Q where
    "Q i = (if i = 0 then VPow (⋃⇩∘X ×⇩∘ ⋃⇩∘Y) else if i = 1⇩ℕ then X else Y)" 
    for i
  have 
    "{[r, A, B]⇩∘ |r A B. r ⊆⇩∘ ⋃⇩∘X ×⇩∘ ⋃⇩∘Y ∧ A ∈⇩∘ X ∧ B ∈⇩∘ Y} ⊆
      elts (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
  proof(intro subsetI, unfold mem_Collect_eq, elim exE conjE)
    fix F r A B assume prems: 
      "F = [r, A, B]⇩∘" 
      "r ⊆⇩∘ ⋃⇩∘X ×⇩∘ ⋃⇩∘Y"
      "A ∈⇩∘ X"
      "B ∈⇩∘ Y"
    show "F ∈⇩∘ (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
    proof(intro vproductI, unfold Ball_def; (intro allI impI)?)
      show "𝒟⇩∘ F = set {0, 1⇩ℕ, 2⇩ℕ}" 
        by (simp add: three prems(1) nat_omega_simps)
      fix i assume "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}"
      then consider ‹i = 0› | ‹i = 1⇩ℕ› | ‹i = 2⇩ℕ› by auto
      then show "F⦇i⦈ ∈⇩∘ Q i" by cases (auto simp: Q_def prems nat_omega_simps)
    qed (auto simp: prems(1))
  qed
  moreover then have small[simp]: 
    "small {[r, A, B]⇩∘ | r A B. r ⊆⇩∘⋃⇩∘X ×⇩∘ ⋃⇩∘Y ∧ A ∈⇩∘ X ∧ B ∈⇩∘ Y}"
    by (rule down)
  ultimately have
    "set {[r, A, B]⇩∘ |r A B. r ⊆⇩∘ ⋃⇩∘X ×⇩∘ ⋃⇩∘Y ∧ A ∈⇩∘ X ∧ B ∈⇩∘ Y} ⊆⇩∘
      (∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i)"
    by auto
  moreover have "(∏⇩∘i∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}. Q i) ∈⇩∘ Vset α"
  proof(rule Limit_vproduct_in_VsetI)
    show "set {0, 1⇩ℕ, 2⇩ℕ} ∈⇩∘ Vset α"
      by (auto simp: three[symmetric] intro!: Axiom_of_Infinity)
    from assms(1,2) have "VPow (⋃⇩∘X ×⇩∘ ⋃⇩∘Y) ∈⇩∘ Vset α"
      by (intro Limit_VPow_in_VsetI Limit_vtimes_in_VsetI) auto
    then show "Q i ∈⇩∘ Vset α" if "i ∈⇩∘ set {0, 1⇩ℕ, 2⇩ℕ}" for i
      using that assms(1,2) unfolding Q_def by (auto simp: nat_omega_simps)
  qed auto
  moreover have
    "(⋃⇩∘A∈⇩∘X. ⋃⇩∘B∈⇩∘Y. Hom (dg_Rel α) A B) ⊆⇩∘
      set {[r, A, B]⇩∘ | r A B. r ⊆⇩∘⋃⇩∘X ×⇩∘ ⋃⇩∘Y ∧ A ∈⇩∘ X ∧ B ∈⇩∘ Y}"
  proof(rule vsubsetI)
    fix F assume prems: "F ∈⇩∘ (⋃⇩∘A∈⇩∘X. ⋃⇩∘B∈⇩∘Y. Hom (dg_Rel α) A B)"
    then obtain A where A: "A ∈⇩∘ X" and F_b: "F ∈⇩∘ (⋃⇩∘B∈⇩∘Y. Hom (dg_Rel α) A B)" 
      unfolding vifunion_iff by auto
    then obtain B where B: "B ∈⇩∘ Y" and F_fba: "F ∈⇩∘ Hom (dg_Rel α) A B" 
      by fastforce
    then have "F : A ↦⇘dg_Rel α⇙ B" by simp
    note F = dg_Rel_is_arrD[OF this]
    interpret F: arr_Rel α F rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
      by (intro F)+
    show "F ∈⇩∘ set {[r, A, B]⇩∘ | r A B. r ⊆⇩∘⋃⇩∘X ×⇩∘ ⋃⇩∘Y ∧ A ∈⇩∘ X ∧ B ∈⇩∘ Y}"
    proof(intro in_set_CollectI small exI conjI)
      from F.arr_Rel_def show "F = [F⦇ArrVal⦈, A, B]⇩∘" unfolding F(2,3) by simp
      from A B have "A ×⇩∘ B ⊆⇩∘ ⋃⇩∘X ×⇩∘ ⋃⇩∘Y" by auto
      moreover then have "F⦇ArrVal⦈ ⊆⇩∘ A ×⇩∘ B"
        by (auto simp: F.arr_Rel_ArrVal_vsubset_ArrDom_ArrCod)
      ultimately show "F⦇ArrVal⦈ ⊆⇩∘ ⋃⇩∘X ×⇩∘ ⋃⇩∘Y" by auto
    qed (intro A B)+
  qed
  ultimately show "(⋃⇩∘A∈⇩∘X. ⋃⇩∘B∈⇩∘Y. Hom (dg_Rel α) A B) ∈⇩∘ Vset α" by blast
qed

lemma (in 𝒵) digraph_dg_Rel: "digraph α (dg_Rel α)"
proof(intro digraphI)
  show "vfsequence (dg_Rel α)" unfolding dg_Rel_def by clarsimp
  show "vcard (dg_Rel α) = 4⇩ℕ" 
    unfolding dg_Rel_def by (simp add: nat_omega_simps)
  show "ℛ⇩∘ (dg_Rel α⦇Dom⦈) ⊆⇩∘ dg_Rel α⦇Obj⦈" by (simp add: dg_Rel_Dom_vrange)
  show "ℛ⇩∘ (dg_Rel α⦇Cod⦈) ⊆⇩∘ dg_Rel α⦇Obj⦈" by (simp add: dg_Rel_Cod_vrange)
qed (auto simp: dg_Rel_components dg_Rel_Hom_vifunion_in_Vset dg_Rel_Dom_vrange)



subsection‹Canonical dagger for ‹Rel››


text‹
Dagger categories are exposed explicitly later. 
In the context of this section, the ``dagger'' is viewed merely as 
an explicitly defined homomorphism. A definition of a dagger functor, upon
which the definition presented in this section is based, can be found in nLab 
\<^cite>‹"noauthor_nlab_nodate"›\footnote{\url{https://ncatlab.org/nlab/show/Rel})}.
This reference also contains the majority of the results that are presented
in this subsection.
›


subsubsection‹Definition and elementary properties›

definition dghm_dag_Rel :: "V ⇒ V" (‹†⇩D⇩G⇩.⇩R⇩e⇩l›)
  where "†⇩D⇩G⇩.⇩R⇩e⇩l α = 
    [
      vid_on (dg_Rel α⦇Obj⦈), 
      VLambda (dg_Rel α⦇Arr⦈) converse_Rel, 
      op_dg (dg_Rel α), 
      dg_Rel α
    ]⇩∘"


text‹Components.›

lemma dghm_dag_Rel_components:
  shows "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈ = vid_on (dg_Rel α⦇Obj⦈)"
    and "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈ = VLambda (dg_Rel α⦇Arr⦈) converse_Rel"
    and "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇HomDom⦈ = op_dg (dg_Rel α)"
    and "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇HomCod⦈ = dg_Rel α"
  unfolding dghm_dag_Rel_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda dghm_dag_Rel_components(1)[folded VLambda_vid_on]
  |vsv dghm_dag_Rel_ObjMap_vsv[dg_Rel_cs_intros]|
  |vdomain 
    dghm_dag_Rel_ObjMap_vdomain[unfolded dg_Rel_components, dg_Rel_cs_simps]
  |
  |app dghm_dag_Rel_ObjMap_app[unfolded dg_Rel_components, dg_Rel_cs_simps]|

lemma dghm_dag_Rel_ObjMap_vrange[dg_cs_simps]: "ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈) = Vset α"
  unfolding dghm_dag_Rel_components dg_Rel_components by simp


subsubsection‹Arrow map›

mk_VLambda dghm_dag_Rel_components(2)
  |vsv dghm_dag_Rel_ArrMap_vsv[dg_Rel_cs_intros]|
  |vdomain dghm_dag_Rel_ArrMap_vdomain[dg_Rel_cs_simps]|
  |app dghm_dag_Rel_ArrMap_app[unfolded dg_Rel_cs_simps, dg_Rel_cs_simps]|

lemma dghm_dag_Rel_ArrMap_app_vdomain[dg_cs_simps]:
  assumes "T : A ↦⇘dg_Rel α⇙ B"
  shows "𝒟⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈) = ℛ⇩∘ (T⦇ArrVal⦈)"
proof-
  from assms interpret T: arr_Rel α T by (simp add: dg_Rel_is_arrD)
  from dg_Rel_is_arrD(1)[OF assms] show ?thesis
    by (cs_concl cs_simp: dg_Rel_cs_simps V_cs_simps converse_Rel_components(1))
qed

lemma dghm_dag_Rel_ArrMap_app_vrange[dg_cs_simps]:
  assumes "T : A ↦⇘dg_Rel α⇙ B"
  shows "ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈) = 𝒟⇩∘ (T⦇ArrVal⦈)"
proof-
  from assms interpret T: arr_Rel α T by (simp add: dg_Rel_is_arrD)
  from dg_Rel_is_arrD(1)[OF assms] show ?thesis
    by (cs_concl cs_simp: dg_Rel_cs_simps V_cs_simps converse_Rel_components(1))
qed

lemma dghm_dag_Rel_ArrMap_app_iff[dg_cs_simps]:
  assumes "T : A ↦⇘dg_Rel α⇙ B" 
  shows "⟨a, b⟩ ∈⇩∘ †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈ ⟷ ⟨b, a⟩ ∈⇩∘ T⦇ArrVal⦈"
proof-
  from assms interpret T: arr_Rel α T by (simp add: dg_Rel_is_arrD)
  note T = dg_Rel_is_arrD[OF assms]
  note [dg_Rel_cs_simps] = converse_Rel_components
  show ?thesis
  proof(intro iffI)
    assume prems: "⟨a, b⟩ ∈⇩∘ †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈"
    then have a: "a ∈⇩∘ 𝒟⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈)"
      and b: "b ∈⇩∘ ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈)"
      by auto
    with assms have a: "a ∈⇩∘ ℛ⇩∘ (T⦇ArrVal⦈)" and b: "b ∈⇩∘ 𝒟⇩∘ (T⦇ArrVal⦈)"
      by (simp_all add: dg_cs_simps)
    from prems T(1) have "⟨a, b⟩ ∈⇩∘ (T⦇ArrVal⦈)¯⇩∘"
      by (cs_prems cs_shallow cs_simp: dg_Rel_cs_simps)
    then show "⟨b, a⟩ ∈⇩∘ T⦇ArrVal⦈" by clarsimp
  next
    assume "⟨b, a⟩ ∈⇩∘ T⦇ArrVal⦈"
    then have "⟨a, b⟩ ∈⇩∘ (T⦇ArrVal⦈)¯⇩∘" by auto
    with T(1) show "⟨a, b⟩ ∈⇩∘ †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈"
      by (cs_concl cs_shallow cs_simp: dg_Rel_cs_simps)
  qed
qed


subsubsection‹Further properties›

lemma dghm_dag_Rel_ArrMap_vrange[dg_Rel_cs_simps]: 
  "ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈) = dg_Rel α⦇Arr⦈"
proof(intro vsubset_antisym vsubsetI)
  interpret ArrMap: vsv ‹†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈› 
    unfolding dghm_dag_Rel_components by simp
  fix T assume "T ∈⇩∘ ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈)"
  then obtain S where T_def: "T = †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇S⦈" 
    and S: "S ∈⇩∘ 𝒟⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈)"
    by (blast dest: ArrMap.vrange_atD)
  from S show "T ∈⇩∘ dg_Rel α⦇Arr⦈" 
    by 
      (
        simp add:
          T_def 
          dghm_dag_Rel_components 
          dg_Rel_components 
          arr_Rel.arr_Rel_converse_Rel
      )
next
  interpret ArrMap: vsv ‹†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈› 
    unfolding dghm_dag_Rel_components by simp
  fix T assume "T ∈⇩∘ dg_Rel α⦇Arr⦈"
  then have "arr_Rel α T" by (simp add: dg_Rel_components)
  then have "(T¯⇩R⇩e⇩l)¯⇩R⇩e⇩l = T" and "arr_Rel α (T¯⇩R⇩e⇩l)"
    by 
      (
        auto simp: 
          arr_Rel.arr_Rel_converse_Rel_converse_Rel arr_Rel.arr_Rel_converse_Rel
      )
  then have "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T¯⇩R⇩e⇩l⦈ = T" "T¯⇩R⇩e⇩l ∈⇩∘ 𝒟⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈)"
    by (simp_all add: dg_Rel_components(2) dghm_dag_Rel_components(2))
  then show "T ∈⇩∘ ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈)" by blast
qed

lemma dghm_dag_Rel_ArrMap_app_is_arr:
  assumes "T : b ↦⇘dg_Rel α⇙ a"
  shows 
    "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ : †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇a⦈ ↦⇘dg_Rel α⇙ †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇b⦈"
proof(intro is_arrI)
  from assms have a: "a ∈⇩∘ Vset α" and b: "b ∈⇩∘ Vset α"
    unfolding dg_Rel_components by (fastforce simp: dg_Rel_components)+
  from assms have T: "arr_Rel α T" by (auto simp: dg_Rel_is_arrD(1))
  then show dag_T: "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ ∈⇩∘ dg_Rel α⦇Arr⦈"
    by (cs_concl cs_shallow cs_simp: dg_Rel_cs_simps cs_intro: dg_Rel_cs_intros)
  from a assms T show "dg_Rel α⦇Dom⦈⦇†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦈ = †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇a⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps dg_Rel_cs_simps cs_intro: dg_Rel_cs_intros
      )
  from b assms T show "dg_Rel α⦇Cod⦈⦇†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦈ = †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇b⦈"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: dg_cs_simps dg_Rel_cs_simps cs_intro: dg_Rel_cs_intros
      )
qed


subsubsection‹Canonical dagger for ‹Rel› is a digraph isomorphism›

lemma (in 𝒵) dghm_dag_Rel_is_iso_dghm: 
  "†⇩D⇩G⇩.⇩R⇩e⇩l α : op_dg (dg_Rel α) ↦↦⇩D⇩G⇩.⇩i⇩s⇩o⇘α⇙ dg_Rel α"
proof(rule is_iso_dghmI)
  interpret digraph α ‹dg_Rel α› by (simp add: digraph_dg_Rel)
  show "†⇩D⇩G⇩.⇩R⇩e⇩l α : op_dg (dg_Rel α) ↦↦⇩D⇩G⇘α⇙ dg_Rel α"
  proof(rule is_dghmI, unfold dg_op_simps dghm_dag_Rel_components(3,4))
    show "vfsequence (†⇩D⇩G⇩.⇩R⇩e⇩l α)"
      unfolding dghm_dag_Rel_def by (simp add: nat_omega_simps)
    show "vcard (†⇩D⇩G⇩.⇩R⇩e⇩l α) = 4⇩ℕ"
      unfolding dghm_dag_Rel_def by (simp add: nat_omega_simps)
    fix T a b assume "T : b ↦⇘dg_Rel α⇙ a" 
    then show
      "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ : †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇a⦈ ↦⇘dg_Rel α⇙ †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇b⦈"
      by (rule dghm_dag_Rel_ArrMap_app_is_arr)
  qed (auto simp: dghm_dag_Rel_components intro: dg_cs_intros dg_op_intros)
  show "v11 (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈)"
  proof
    (
      intro vsv.vsv_valeq_v11I,
      unfold dghm_dag_Rel_ArrMap_vdomain dg_Rel_Arr_iff
    )
    fix S T assume prems: 
      "arr_Rel α S" 
      "arr_Rel α T" 
      "†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇S⦈ = †⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈" 
    from prems show "S = T"
      by 
        (
          auto simp: 
            dg_Rel_components 
            dg_Rel_cs_simps
            dghm_dag_Rel_ArrMap_app[OF prems(1)] 
            dghm_dag_Rel_ArrMap_app[OF prems(2)]
        )
  qed (auto intro: dg_Rel_cs_intros)
  show "ℛ⇩∘ (†⇩D⇩G⇩.⇩R⇩e⇩l α⦇ArrMap⦈) = dg_Rel α⦇Arr⦈" by (simp add: dg_Rel_cs_simps)
qed (simp_all add: dghm_dag_Rel_components)


subsubsection‹Further properties of the canonical dagger›

lemma (in 𝒵) dghm_cn_comp_dghm_dag_Rel_dghm_dag_Rel: 
  "†⇩D⇩G⇩.⇩R⇩e⇩l α ⇩D⇩G⇩H⇩M∘ †⇩D⇩G⇩.⇩R⇩e⇩l α = dghm_id (dg_Rel α)"
proof-
  interpret digraph α ‹dg_Rel α› by (simp add: digraph_dg_Rel)
  from dghm_dag_Rel_is_iso_dghm have dag: 
    "†⇩D⇩G⇩.⇩R⇩e⇩l α : dg_Rel α ⇩D⇩G↦↦⇘α⇙ dg_Rel α"
    by (simp add: is_iso_dghm_def)
  show ?thesis
  proof(rule dghm_eqI)
    show "(†⇩D⇩G⇩.⇩R⇩e⇩l α ⇩D⇩G⇩H⇩M∘ †⇩D⇩G⇩.⇩R⇩e⇩l α)⦇ArrMap⦈ = dghm_id (dg_Rel α)⦇ArrMap⦈"
    proof(rule vsv_eqI)
      show "vsv ((†⇩D⇩G⇩.⇩R⇩e⇩l α ⇩D⇩G⇩H⇩M∘ †⇩D⇩G⇩.⇩R⇩e⇩l α)⦇ArrMap⦈)"
        by (auto simp: dghm_cn_comp_components dghm_dag_Rel_components)
      fix a assume "a ∈⇩∘ 𝒟⇩∘ ((†⇩D⇩G⇩.⇩R⇩e⇩l α ⇩D⇩G⇩H⇩M∘ †⇩D⇩G⇩.⇩R⇩e⇩l α)⦇ArrMap⦈)"
      then have a: "arr_Rel α a" 
        unfolding dg_Rel_cs_simps dghm_cn_comp_ArrMap_vdomain[OF dag dag] by simp
      from a dghm_dag_Rel_is_iso_dghm show 
        "(†⇩D⇩G⇩.⇩R⇩e⇩l α ⇩D⇩G⇩H⇩M∘ †⇩D⇩G⇩.⇩R⇩e⇩l α)⦇ArrMap⦈⦇a⦈ = dghm_id (dg_Rel α)⦇ArrMap⦈⦇a⦈"
        by
          (
            cs_concl 
              cs_simp: dg_Rel_cs_simps dg_cs_simps dg_cn_cs_simps 
              cs_intro: dg_Rel_cs_intros dghm_cs_intros 
          )
    qed (simp_all add: dghm_cn_comp_components dghm_id_components dg_Rel_cs_simps)
    show "dghm_id (dg_Rel α) : dg_Rel α ↦↦⇩D⇩G⇘α⇙ dg_Rel α"
      by (simp_all add: digraph.dg_dghm_id_is_dghm digraph_axioms)
  qed 
    (
      auto simp: 
        dghm_cn_comp_is_dghm[OF digraph_axioms dag dag] 
        dghm_cn_comp_components 
        dghm_dag_Rel_components 
        dghm_id_components
    )
qed

text‹\newpage›

end