Theory CZH_ECAT_Rel

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Rel››
theory CZH_ECAT_Rel
  imports 
    CZH_Foundations.CZH_SMC_Rel
    CZH_ECAT_Functor
    CZH_ECAT_Small_Category
begin



subsection‹Background›


text‹
The methodology chosen for the exposition of ‹Rel› as a category is analogous 
to the one used in \<^cite>‹"milehins_category_2021"› 
for the exposition of ‹Rel› as a semicategory. 
The general references for this section are Chapter I-7 in 
\<^cite>‹"mac_lane_categories_2010"› and nLab 
\<^cite>‹"noauthor_nlab_nodate"›\footnote{
\url{https://ncatlab.org/nlab/show/Rel}
}.
›

named_theorems cat_Rel_cs_simps
named_theorems cat_Rel_cs_intros

lemmas (in arr_Rel) [cat_Rel_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Rel) [cat_cs_intros, cat_Rel_cs_intros] = 
  arr_Rel_axioms'

lemmas [cat_Rel_cs_simps] = 
  dg_Rel_shared_cs_simps
  arr_Rel.arr_Rel_length
  arr_Rel_comp_Rel_id_Rel_left
  arr_Rel_comp_Rel_id_Rel_right
  arr_Rel.arr_Rel_converse_Rel_converse_Rel
  arr_Rel_converse_Rel_eq_iff
  arr_Rel_converse_Rel_comp_Rel
  arr_Rel_comp_Rel_converse_Rel_left_if_v11
  arr_Rel_comp_Rel_converse_Rel_right_if_v11

lemmas [cat_Rel_cs_intros] = 
  dg_Rel_shared_cs_intros
  arr_Rel_comp_Rel
  arr_Rel.arr_Rel_converse_Rel

lemmas [cat_cs_simps] = incl_Rel_ArrVal_app



subsection‹‹Rel› as a category›


subsubsection‹Definition and elementary properties›

definition cat_Rel :: "V ⇒ V"
  where "cat_Rel α =
    [
      Vset α,
      set {T. arr_Rel α T},
      (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrDom⦈),
      (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrCod⦈),
      (λST∈⇩∘composable_arrs (dg_Rel α). ST⦇0⦈ ∘⇩R⇩e⇩l ST⦇1⇩ℕ⦈),
      VLambda (Vset α) id_Rel 
    ]⇩∘"


text‹Components.›

lemma cat_Rel_components:
  shows "cat_Rel α⦇Obj⦈ = Vset α"
    and "cat_Rel α⦇Arr⦈ = set {T. arr_Rel α T}"
    and "cat_Rel α⦇Dom⦈ = (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrDom⦈)"
    and "cat_Rel α⦇Cod⦈ = (λT∈⇩∘set {T. arr_Rel α T}. T⦇ArrCod⦈)"
    and "cat_Rel α⦇Comp⦈ = (λST∈⇩∘composable_arrs (dg_Rel α). ST⦇0⦈ ∘⇩R⇩e⇩l ST⦇1⇩ℕ⦈)"
    and "cat_Rel α⦇CId⦈ = VLambda (Vset α) id_Rel"
  unfolding cat_Rel_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_cat_Rel: "cat_smc (cat_Rel α) = smc_Rel α"
proof(rule vsv_eqI)
  show "vsv (cat_smc (cat_Rel α))" unfolding cat_smc_def by auto
  show "vsv (smc_Rel α)" unfolding smc_Rel_def by auto
  have dom_lhs: "𝒟⇩∘ (cat_smc (cat_Rel α)) = 5⇩ℕ" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (smc_Rel α) = 5⇩ℕ"
    unfolding smc_Rel_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cat_smc (cat_Rel α)) = 𝒟⇩∘ (smc_Rel α)"
    unfolding dom_lhs dom_rhs by simp
  show 
    "a ∈⇩∘ 𝒟⇩∘ (cat_smc (cat_Rel α)) ⟹ cat_smc (cat_Rel α)⦇a⦈ = smc_Rel α⦇a⦈"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold cat_smc_def dg_field_simps cat_Rel_def smc_Rel_def
      )
      (auto simp: nat_omega_simps)
qed

lemmas_with [folded cat_smc_cat_Rel, unfolded slicing_simps]: 
  cat_Rel_Obj_iff = smc_Rel_Obj_iff
  and cat_Rel_Arr_iff[cat_Rel_cs_simps] = smc_Rel_Arr_iff
  and cat_Rel_Dom_vsv[cat_Rel_cs_intros] = smc_Rel_Dom_vsv
  and cat_Rel_Dom_vdomain[cat_Rel_cs_simps] = smc_Rel_Dom_vdomain
  and cat_Rel_Dom_app[cat_Rel_cs_simps] = smc_Rel_Dom_app
  and cat_Rel_Dom_vrange = smc_Rel_Dom_vrange
  and cat_Rel_Cod_vsv[cat_Rel_cs_intros] = smc_Rel_Cod_vsv
  and cat_Rel_Cod_vdomain[cat_Rel_cs_simps] = smc_Rel_Cod_vdomain
  and cat_Rel_Cod_app[cat_Rel_cs_simps] = smc_Rel_Cod_app
  and cat_Rel_Cod_vrange = smc_Rel_Cod_vrange
  and cat_Rel_is_arrI[cat_Rel_cs_intros] = smc_Rel_is_arrI
  and cat_Rel_is_arrD = smc_Rel_is_arrD
  and cat_Rel_is_arrE = smc_Rel_is_arrE
  and cat_Rel_is_arr_ArrValE = smc_Rel_is_arr_ArrValE

lemmas_with [folded cat_smc_cat_Rel, unfolded slicing_simps, unfolded cat_smc_cat_Rel]: 
  cat_Rel_composable_arrs_dg_Rel = smc_Rel_composable_arrs_dg_Rel
  and cat_Rel_Comp = smc_Rel_Comp
  and cat_Rel_Comp_app[cat_Rel_cs_simps] = smc_Rel_Comp_app
  and cat_Rel_Comp_vdomain[simp] = smc_Rel_Comp_vdomain
  and cat_Rel_is_monic_arrI = smc_Rel_is_monic_arrI
  and cat_Rel_is_monic_arrD = smc_Rel_is_monic_arrD
  and cat_Rel_is_monic_arr = smc_Rel_is_monic_arr
  and cat_Rel_is_monic_arr_is_epic_arr = smc_Rel_is_monic_arr_is_epic_arr
  and cat_Rel_is_epic_arr_is_monic_arr = smc_Rel_is_epic_arr_is_monic_arr
  and cat_Rel_is_epic_arrI = smc_Rel_is_epic_arrI
  and cat_Rel_is_epic_arrD = smc_Rel_is_epic_arrD
  and cat_Rel_is_epic_arr = smc_Rel_is_epic_arr

lemmas [cat_cs_simps] = cat_Rel_is_arrD(2,3)

lemmas [cat_Rel_cs_intros] = cat_Rel_is_arrI

lemmas_with (in 𝒵) [folded cat_smc_cat_Rel, unfolded slicing_simps]: 
  cat_Rel_Hom_vifunion_in_Vset = smc_Rel_Hom_vifunion_in_Vset
  and cat_Rel_incl_Rel_is_arr = smc_Rel_incl_Rel_is_arr
  and cat_Rel_incl_Rel_is_arr'[cat_Rel_cs_intros] = smc_Rel_incl_Rel_is_arr'
  and cat_Rel_Comp_vrange = smc_Rel_Comp_vrange
  and cat_Rel_obj_terminal = smc_Rel_obj_terminal
  and cat_Rel_obj_initial = smc_Rel_obj_initial
  and cat_Rel_obj_terminal_obj_initial = smc_Rel_obj_terminal_obj_initial
  and cat_Rel_obj_null = smc_Rel_obj_null
  and cat_Rel_is_zero_arr = smc_Rel_is_zero_arr

lemmas [cat_Rel_cs_intros] = 𝒵.cat_Rel_incl_Rel_is_arr'


subsubsection‹Identity›

lemma (in 𝒵) cat_Rel_CId_app[cat_Rel_cs_simps]:
  assumes "T ∈⇩∘ Vset α"
  shows "cat_Rel α⦇CId⦈⦇T⦈ = id_Rel T"
  using assms unfolding cat_Rel_components by simp

lemmas [cat_Rel_cs_simps] = 𝒵.cat_Rel_CId_app


subsubsection‹‹Rel› is a category›

lemma (in 𝒵) category_cat_Rel: "category α (cat_Rel α)"
proof(rule categoryI, unfold cat_smc_cat_Rel)

  interpret Rel: semicategory α ‹cat_smc (cat_Rel α)›
    unfolding cat_smc_cat_Rel by (simp add: semicategory_smc_Rel)

  show "vfsequence (cat_Rel α)" unfolding cat_Rel_def by simp
  show "vcard (cat_Rel α) = 6⇩ℕ"
    unfolding cat_Rel_def by (simp add: nat_omega_simps)
  show "cat_Rel α⦇CId⦈⦇A⦈ : A ↦⇘cat_Rel α⇙ A"
    if "A ∈⇩∘ cat_Rel α⦇Obj⦈" for A
    using that 
    unfolding cat_Rel_Obj_iff
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_Rel_cs_simps cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI 
      )
  show "cat_Rel α⦇CId⦈⦇B⦈ ∘⇩A⇘cat_Rel α⇙ F = F"
    if "F : A ↦⇘cat_Rel α⇙ B" for F A B
  proof-
    from that have "arr_Rel α F" "A ∈⇩∘ Vset α" "B ∈⇩∘ Vset α"
      by (auto elim: cat_Rel_is_arrE simp: cat_Rel_cs_simps)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Rel_cs_simps 
            cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI
        )
  qed
  
  show "F ∘⇩A⇘cat_Rel α⇙ cat_Rel α⦇CId⦈⦇B⦈ = F"
    if "F : B ↦⇘cat_Rel α⇙ C" for F B C
  proof-
    from that have "arr_Rel α F" "B ∈⇩∘ Vset α" "C ∈⇩∘ Vset α"
      by (auto elim: cat_Rel_is_arrE simp: cat_Rel_cs_simps)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Rel_cs_simps
            cs_intro: cat_Rel_cs_intros arr_Rel_id_RelI
        )
  qed

qed (auto simp: semicategory_smc_Rel cat_Rel_components)

lemma (in 𝒵) category_cat_Rel'[cat_Rel_cs_intros]: 
  assumes "α' = α" and "α'' = α"
  shows "category α' (cat_Rel α'')"
  unfolding assms by (rule category_cat_Rel)

lemmas [cat_Rel_cs_intros] = 𝒵.category_cat_Rel'



subsection‹Canonical dagger for ‹Rel››


subsubsection‹Definition and elementary properties›

definition cf_dag_Rel :: "V ⇒ V" (‹†⇩C⇩.⇩R⇩e⇩l›)
  where "†⇩C⇩.⇩R⇩e⇩l α = 
    [
      vid_on (cat_Rel α⦇Obj⦈), 
      VLambda (cat_Rel α⦇Arr⦈) converse_Rel, 
      op_cat (cat_Rel α), 
      cat_Rel α
    ]⇩∘"


text‹Components.›

lemma cf_dag_Rel_components:
  shows "†⇩C⇩.⇩R⇩e⇩l α⦇ObjMap⦈ = vid_on (cat_Rel α⦇Obj⦈)"
    and "†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈ = VLambda (cat_Rel α⦇Arr⦈) converse_Rel"
    and "†⇩C⇩.⇩R⇩e⇩l α⦇HomDom⦈ = op_cat (cat_Rel α)"
    and "†⇩C⇩.⇩R⇩e⇩l α⦇HomCod⦈ = cat_Rel α"
  unfolding cf_dag_Rel_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cf_smcf_cf_dag_Rel: "cf_smcf (†⇩C⇩.⇩R⇩e⇩l α) = †⇩S⇩M⇩C⇩.⇩R⇩e⇩l α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟⇩∘ (cf_smcf (†⇩C⇩.⇩R⇩e⇩l α)) = 4⇩ℕ" 
    unfolding cf_smcf_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟⇩∘ (†⇩S⇩M⇩C⇩.⇩R⇩e⇩l α) = 4⇩ℕ"
    unfolding smcf_dag_Rel_def by (simp add: nat_omega_simps)
  show "𝒟⇩∘ (cf_smcf (†⇩C⇩.⇩R⇩e⇩l α)) = 𝒟⇩∘ (†⇩S⇩M⇩C⇩.⇩R⇩e⇩l α)"
    unfolding dom_lhs dom_rhs by simp
  show "A ∈⇩∘ 𝒟⇩∘ (cf_smcf (†⇩C⇩.⇩R⇩e⇩l α)) ⟹ cf_smcf (†⇩C⇩.⇩R⇩e⇩l α)⦇A⦈ = †⇩S⇩M⇩C⇩.⇩R⇩e⇩l α⦇A⦈"
    for A
    by
      (
        unfold dom_lhs,
        elim_in_numeral,
        unfold dghm_field_simps[symmetric],
        unfold 
          cat_smc_cat_Rel
          slicing_commute[symmetric]
          cf_smcf_components 
          smcf_dag_Rel_components
          cf_dag_Rel_components
          smc_Rel_components
          cat_Rel_components
      )
      simp_all
qed (auto simp: cf_smcf_def smcf_dag_Rel_def) 

lemmas_with [folded cat_smc_cat_Rel cf_smcf_cf_dag_Rel, unfolded slicing_simps]: 
  cf_dag_Rel_ObjMap_vsv[cat_Rel_cs_intros] = smcf_dag_Rel_ObjMap_vsv
  and cf_dag_Rel_ObjMap_vdomain[cat_Rel_cs_simps] = smcf_dag_Rel_ObjMap_vdomain
  and cf_dag_Rel_ObjMap_app[cat_Rel_cs_simps] = smcf_dag_Rel_ObjMap_app
  and cf_dag_Rel_ObjMap_vrange[cat_Rel_cs_simps] = smcf_dag_Rel_ObjMap_vrange
  and cf_dag_Rel_ArrMap_vsv[cat_Rel_cs_intros] = smcf_dag_Rel_ArrMap_vsv
  and cf_dag_Rel_ArrMap_vdomain[cat_Rel_cs_simps] = smcf_dag_Rel_ArrMap_vdomain
  and cf_dag_Rel_ArrMap_app[cat_Rel_cs_simps] = smcf_dag_Rel_ArrMap_app
  and cf_dag_Rel_ArrMap_vrange[cat_Rel_cs_simps] = smcf_dag_Rel_ArrMap_vrange
  and cf_dag_Rel_app_is_arr[cat_Rel_cs_intros] = smcf_dag_Rel_app_is_arr
  and cf_dag_Rel_ArrMap_app_vdomain[cat_cs_simps] =
    smcf_dag_Rel_ArrMap_app_vdomain
  and cf_dag_Rel_ArrMap_app_vrange[cat_cs_simps] =
    smcf_dag_Rel_ArrMap_app_vrange
  and cf_dag_Rel_ArrMap_app_iff[cat_cs_simps] = smcf_dag_Rel_ArrMap_app_iff
  and cf_dag_Rel_ArrMap_smc_Rel_Comp[cat_Rel_cs_simps] = 
    smcf_dag_Rel_ArrMap_smc_Rel_Comp


subsubsection‹Canonical dagger is a contravariant isomorphism of ‹Rel››

lemma (in 𝒵) cf_dag_Rel_is_iso_functor: 
  "†⇩C⇩.⇩R⇩e⇩l α : op_cat (cat_Rel α) ↦↦⇩C⇩.⇩i⇩s⇩o⇘α⇙ cat_Rel α"
proof
  (
    rule is_iso_functorI, 
    unfold 
      cat_smc_cat_Rel 
      cf_smcf_cf_dag_Rel 
      cat_Rel_components 
      cat_op_simps 
      slicing_commute[symmetric]
  )

  interpret is_iso_semifunctor α ‹op_smc (smc_Rel α)› ‹smc_Rel α› ‹†⇩S⇩M⇩C⇩.⇩R⇩e⇩l α›
    by (rule smcf_dag_Rel_is_iso_semifunctor)
  interpret Rel: category α ‹cat_Rel α› by (rule category_cat_Rel)
  
  show "†⇩C⇩.⇩R⇩e⇩l α : op_cat (cat_Rel α) ↦↦⇩C⇘α⇙ cat_Rel α"
  proof
    (
      rule is_functorI, 
      unfold 
        cat_smc_cat_Rel 
        cf_smcf_cf_dag_Rel 
        cat_op_simps 
        slicing_commute[symmetric] 
        cf_dag_Rel_components(3,4)
    )
    show "vfsequence (†⇩C⇩.⇩R⇩e⇩l α)"
      unfolding cf_dag_Rel_def by (simp add: nat_omega_simps)
    show "vcard (†⇩C⇩.⇩R⇩e⇩l α) = 4⇩ℕ" 
      unfolding cf_dag_Rel_def by (simp add: nat_omega_simps)
    show "†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇cat_Rel α⦇CId⦈⦇C⦈⦈ = cat_Rel α⦇CId⦈⦇†⇩C⇩.⇩R⇩e⇩l α⦇ObjMap⦈⦇C⦈⦈"
      if "C ∈⇩∘ cat_Rel α⦇Obj⦈" for C
    proof-
      from that have "C ∈⇩∘ Vset α" 
        by (auto elim: cat_Rel_is_arrE simp: cat_Rel_Obj_iff)
      with that show ?thesis
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_Rel_cs_simps cs_intro: cat_cs_intros arr_Rel_id_RelI
          )
    qed
  qed (auto simp: cat_cs_intros intro: smc_cs_intros)

  show "†⇩S⇩M⇩C⇩.⇩R⇩e⇩l α : op_smc (smc_Rel α) ↦↦⇩S⇩M⇩C⇩.⇩i⇩s⇩o⇘α⇙ smc_Rel α"
    by (rule smcf_dag_Rel_is_iso_semifunctor)

qed

lemma (in 𝒵) cf_dag_Rel_is_iso_functor'[cat_cs_intros]: 
  assumes "𝔄' = op_cat (cat_Rel α)"
    and "𝔅' = cat_Rel α"
    and "α' = α"
  shows "†⇩C⇩.⇩R⇩e⇩l α : 𝔄' ↦↦⇩C⇩.⇩i⇩s⇩o⇘α'⇙ 𝔅'"
  unfolding assms by (rule cf_dag_Rel_is_iso_functor)

lemmas [cat_cs_intros] = 𝒵.cf_dag_Rel_is_iso_functor'


subsubsection‹Further properties of the canonical dagger›

lemma (in 𝒵) cf_cn_comp_cf_dag_Rel_cf_dag_Rel: 
  "†⇩C⇩.⇩R⇩e⇩l α ⇩C⇩F∘ †⇩C⇩.⇩R⇩e⇩l α = cf_id (cat_Rel α)"
proof(rule cf_smcf_eqI)
  interpret category α ‹cat_Rel α› by (rule category_cat_Rel)
  from cf_dag_Rel_is_iso_functor have dag:
    "†⇩C⇩.⇩R⇩e⇩l α : op_cat (cat_Rel α) ↦↦⇩C⇘α⇙ cat_Rel α"
    by (simp add: is_iso_functor.axioms(1))
  from cf_cn_comp_is_functorI[OF category_axioms dag dag] show 
    "†⇩C⇩.⇩R⇩e⇩l α ⇩C⇩F∘ †⇩C⇩.⇩R⇩e⇩l α : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α" .
  show "cf_id (cat_Rel α) : cat_Rel α ↦↦⇩C⇘α⇙ cat_Rel α"
    by (auto simp: category.cat_cf_id_is_functor category_axioms)
  show "cf_smcf (†⇩C⇩.⇩R⇩e⇩l α ⇩C⇩F∘ †⇩C⇩.⇩R⇩e⇩l α) = cf_smcf (smcf_id (cat_Rel α))"
    unfolding slicing_commute[symmetric] cat_smc_cat_Rel cf_smcf_cf_dag_Rel
    by (simp add: smcf_cn_comp_smcf_dag_Rel_smcf_dag_Rel)
qed simp_all



subsection‹Isomorphism›

context
begin

private lemma cat_Rel_is_iso_arr_right_vsubset:
  assumes "S : B ↦⇘cat_Rel α⇙ A"
    and "T : A ↦⇘cat_Rel α⇙ B"
    and "S ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A⦈"
    and "T ∘⇩A⇘cat_Rel α⇙ S = cat_Rel α⦇CId⦈⦇B⦈"
  shows "S⦇ArrVal⦈ ⊆⇩∘ (T⦇ArrVal⦈)¯⇩∘"
proof(rule vsubset_antisym vsubsetI)

  interpret S: arr_Rel α S
    rewrites "S⦇ArrDom⦈ = B" and "S⦇ArrCod⦈ = A"
    by (intro cat_Rel_is_arrD[OF assms(1)])+
  interpret T: arr_Rel α T
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = B"
    by (intro cat_Rel_is_arrD[OF assms(2)])+

  interpret Rel: category α ‹cat_Rel α› by (simp add: S.category_cat_Rel)

  interpret dag: is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†⇩C⇩.⇩R⇩e⇩l α›
    by (auto simp: S.cf_dag_Rel_is_iso_functor)

  from assms(2) have A: "A ∈⇩∘ cat_Rel α⦇Obj⦈" by auto
  from assms(3) have "(S ∘⇩A⇘cat_Rel α⇙ T)⦇ArrVal⦈ = cat_Rel α⦇CId⦈⦇A⦈⦇ArrVal⦈"
    by simp
  with A have [simp]: "S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈ = vid_on A"
    unfolding cat_Rel_Comp_app[OF assms(1,2)]
    by (simp add: id_Rel_components comp_Rel_components cat_Rel_components)

  from assms(2) have B: "B ∈⇩∘ cat_Rel α⦇Obj⦈" by auto
  from assms(4) have "(T ∘⇩A⇘cat_Rel α⇙ S)⦇ArrVal⦈ = cat_Rel α⦇CId⦈⦇B⦈⦇ArrVal⦈"
    by simp
  with B have [simp]: "T⦇ArrVal⦈ ∘⇩∘ S⦇ArrVal⦈ = vid_on B"
    unfolding cat_Rel_Comp_app[OF assms(2,1)]
    by (simp add: id_Rel_components comp_Rel_components cat_Rel_components)

  fix ab assume ab: "ab ∈⇩∘ S⦇ArrVal⦈"
  with S.vbrelation obtain a b where ab_def: "ab = ⟨a, b⟩" and "a ∈⇩∘ B" 
    by (metis S.arr_Rel_ArrVal_vdomain S.ArrVal.vbrelation_vinE vsubsetE)
  then have "⟨a, a⟩ ∈⇩∘ T⦇ArrVal⦈ ∘⇩∘ S⦇ArrVal⦈" by auto
  then obtain c where "⟨a, c⟩ ∈⇩∘ S⦇ArrVal⦈" and ca[intro]: "⟨c, a⟩ ∈⇩∘ T⦇ArrVal⦈" 
    by blast
  have "⟨b, a⟩ ∈⇩∘ T⦇ArrVal⦈"
  proof(rule ccontr)
    assume "⟨b, a⟩ ∉⇩∘ T⦇ArrVal⦈"
    with ca have "c ≠ b" by clarsimp
    moreover from ab have "⟨c, b⟩ ∈⇩∘ S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈" 
      unfolding ab_def by blast
    ultimately show False by (simp add: vid_on_iff)
  qed
  then show "ab ∈⇩∘ (T⦇ArrVal⦈)¯⇩∘" unfolding ab_def by clarsimp

qed

private lemma cat_Rel_is_iso_arr_left_vsubset:
  assumes "S : B ↦⇘cat_Rel α⇙ A" 
    and "T : A ↦⇘cat_Rel α⇙ B" 
    and "S ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A⦈"
    and "T ∘⇩A⇘cat_Rel α⇙ S = cat_Rel α⦇CId⦈⦇B⦈"
  shows "(T⦇ArrVal⦈)¯⇩∘ ⊆⇩∘ S⦇ArrVal⦈"
  using assms(2,3,4) cat_Rel_is_iso_arr_right_vsubset[OF assms(2,1)] 
  by auto

private lemma is_iso_arr_dag: 
  assumes "S : B ↦⇘cat_Rel α⇙ A" 
    and "T : A ↦⇘cat_Rel α⇙ B" 
    and "S ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A⦈"
    and "T ∘⇩A⇘cat_Rel α⇙ S = cat_Rel α⦇CId⦈⦇B⦈"
  shows "S = †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈"
proof(rule arr_Rel_eqI[of α])

  interpret S: arr_Rel α S by (intro cat_Rel_is_arrD(1)[OF assms(1)])
  interpret Rel: category α ‹cat_Rel α› by (rule S.category_cat_Rel)
  interpret dag: is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†⇩C⇩.⇩R⇩e⇩l α›
    by (auto simp: S.cf_dag_Rel_is_iso_functor)

  from assms(1) show S: "arr_Rel α S" by (fastforce simp: cat_Rel_components(2))
  from cf_dag_Rel_app_is_arr[OF assms(2)] show "arr_Rel α (†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈)"
    by (auto elim!: cat_Rel_is_arrE)
  from assms(2) have T: "arr_Rel α T" by (auto simp: cat_Rel_is_arrD(1))
  from S T assms show "S⦇ArrVal⦈ = †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈"
    unfolding cf_dag_Rel_ArrMap_app[OF T] converse_Rel_components
    by (intro vsubset_antisym) 
      (
        simp_all add: 
          cat_Rel_is_iso_arr_left_vsubset 
          cat_Rel_is_iso_arr_right_vsubset
      )
  from T assms show "S⦇ArrDom⦈ = †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrDom⦈"
    unfolding cf_dag_Rel_components 
    by (auto simp: cat_cs_simps cat_Rel_cs_simps converse_Rel_components(1))
  from S assms show "S⦇ArrCod⦈ = †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈⦇ArrCod⦈"
    by 
      (
        cs_concl 
          cs_intro: cat_op_intros cat_cs_intros 
          cs_simp: cat_Rel_cs_simps cat_cs_simps
      )

qed

lemma cat_Rel_is_iso_arrI[intro]:
  assumes "T : A ↦⇘cat_Rel α⇙ B" 
    and "v11 (T⦇ArrVal⦈)"
    and "𝒟⇩∘ (T⦇ArrVal⦈) = A"
    and "ℛ⇩∘ (T⦇ArrVal⦈) = B"
  shows "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
proof(rule is_iso_arrI[where ?g = ‹†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈›])

  interpret T: arr_Rel α T by (intro cat_Rel_is_arrD[OF assms(1)])+
  interpret Rel: category α ‹cat_Rel α› by (rule T.category_cat_Rel)
  interpret v11: v11 ‹T⦇ArrVal⦈› by (rule assms(2))

  interpret is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†⇩C⇩.⇩R⇩e⇩l α›
    by (simp add: T.cf_dag_Rel_is_iso_functor)

  show "T : A ↦⇘cat_Rel α⇙ B" by (rule assms(1))

  show "is_inverse (cat_Rel α) (†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈) T"
  proof(intro is_inverseI)
    from assms(1) show dag_T: "†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ : B ↦⇘cat_Rel α⇙ A"
      by 
        (
          cs_concl 
            cs_simp: cat_op_simps cat_Rel_cs_simps 
            cs_intro: cat_cs_intros
        )
    show T: "T : A ↦⇘cat_Rel α⇙ B" by (rule assms(1))
    from T T.arr_Rel_axioms v11.v11_axioms assms(3) show 
      "†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_Rel_cs_simps  
            cs_intro: cat_cs_intros cat_Rel_cs_intros
        )
    from T T.arr_Rel_axioms v11.v11_axioms assms(4) show 
      "T ∘⇩A⇘cat_Rel α⇙ †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈ = cat_Rel α⦇CId⦈⦇B⦈"
      by 
        (
          cs_concl 
            cs_simp: cat_cs_simps cat_Rel_cs_simps  
            cs_intro: cat_cs_intros cat_Rel_cs_intros
        )
  qed

qed

lemma cat_Rel_is_iso_arrD[dest]:
  assumes "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
  shows "T : A ↦⇘cat_Rel α⇙ B" 
    and "v11 (T⦇ArrVal⦈)"
    and "𝒟⇩∘ (T⦇ArrVal⦈) = A"
    and "ℛ⇩∘ (T⦇ArrVal⦈) = B"
proof-

  from assms show T: "T : A ↦⇘cat_Rel α⇙ B" 
    by (simp add: is_iso_arr_def)

  interpret T: arr_Rel α T
    rewrites [simp]: "T⦇ArrDom⦈ = A" and [simp]: "T⦇ArrCod⦈ = B"
    by (intro cat_Rel_is_arrD[OF T])+
  interpret is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†⇩C⇩.⇩R⇩e⇩l α›
    by (simp add: T.cf_dag_Rel_is_iso_functor)

  from is_iso_arrD[OF assms(1)] obtain S where 
    "is_inverse (cat_Rel α) S T"
    by clarsimp
  from is_inverseD[OF this] obtain A' B' where "S : B' ↦⇘cat_Rel α⇙ A'" 
    and "T : A' ↦⇘cat_Rel α⇙ B'"
    and "S ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A'⦈" 
    and "T ∘⇩A⇘cat_Rel α⇙ S = cat_Rel α⦇CId⦈⦇B'⦈"
    by auto
  moreover with T have "A' = A" "B' = B" by auto
  ultimately have S: "S : B ↦⇘cat_Rel α⇙ A" 
    and ST: "S ∘⇩A⇘cat_Rel α⇙ T = cat_Rel α⦇CId⦈⦇A⦈" 
    and TS: "T ∘⇩A⇘cat_Rel α⇙ S = cat_Rel α⦇CId⦈⦇B⦈"
    by auto
  
  from S T ST TS have S_def: "S = †⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈"
    by (rule is_iso_arr_dag)

  interpret S: arr_Rel α ‹†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈›
    rewrites "(†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈)⦇ArrDom⦈ = B" 
      and "(†⇩C⇩.⇩R⇩e⇩l α⦇ArrMap⦈⦇T⦈)⦇ArrCod⦈ = A"
    by (fold S_def, insert S, all‹elim cat_Rel_is_arrE›) 
      (simp_all add: cat_Rel_components)

  from T.arr_Rel_axioms S_def have S_T: "S⦇ArrVal⦈ = (T⦇ArrVal⦈)¯⇩∘"
    by (simp add: cf_dag_Rel_ArrMap_app converse_Rel_components(1))

  from S have A: "A ∈⇩∘ cat_Rel α⦇Obj⦈" and B: "B ∈⇩∘ cat_Rel α⦇Obj⦈" by auto

  from B TS A ST have 
    "(T ∘⇩R⇩e⇩l S)⦇ArrVal⦈ = id_Rel B⦇ArrVal⦈"
    "(S ∘⇩R⇩e⇩l T)⦇ArrVal⦈ = id_Rel A⦇ArrVal⦈"
    unfolding cat_Rel_Comp_app[OF S T] cat_Rel_Comp_app[OF T S]
    unfolding cat_Rel_components
    by simp_all

  then have val_ST: "S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈ = vid_on A" 
    and val_TS: "T⦇ArrVal⦈ ∘⇩∘ S⦇ArrVal⦈ = vid_on B"
    unfolding comp_Rel_components id_Rel_components by simp_all

  show "v11 (T⦇ArrVal⦈)"
  proof(rule v11I)
  
    show "vsv (T⦇ArrVal⦈)"
    proof(rule vsvI)
      fix a b c assume prems: "⟨a, b⟩ ∈⇩∘ T⦇ArrVal⦈" "⟨a, c⟩ ∈⇩∘ T⦇ArrVal⦈"
      from prems(1) S_T have "⟨b, a⟩ ∈⇩∘ S⦇ArrVal⦈" by auto
      with prems(2) val_TS have "⟨b, c⟩ ∈⇩∘ vid_on B" by auto
      then show "b = c" by clarsimp
    qed (auto simp: T.ArrVal.vbrelation_axioms)

    show "vsv ((T⦇ArrVal⦈)¯⇩∘)"
    proof(rule vsvI)
      fix a b c 
      assume prems: "⟨a, b⟩ ∈⇩∘ (T⦇ArrVal⦈)¯⇩∘" "⟨a, c⟩ ∈⇩∘ (T⦇ArrVal⦈)¯⇩∘"
      with S_T have "⟨a, b⟩ ∈⇩∘ S⦇ArrVal⦈" and "⟨a, c⟩ ∈⇩∘ S⦇ArrVal⦈" by auto
      moreover from prems have "⟨b, a⟩ ∈⇩∘ T⦇ArrVal⦈" and "⟨c, a⟩ ∈⇩∘ T⦇ArrVal⦈" 
        by auto
      ultimately have "⟨b, c⟩ ∈⇩∘ vid_on A" using val_ST by auto
      then show "b = c" by clarsimp
    qed auto

  qed

  show "𝒟⇩∘ (T⦇ArrVal⦈) = A"
  proof(intro vsubset_antisym vsubsetI)
    fix a assume "a ∈⇩∘ A"
    with val_ST have "⟨a, a⟩ ∈⇩∘ S⦇ArrVal⦈ ∘⇩∘ T⦇ArrVal⦈" by auto 
    then show "a ∈⇩∘ 𝒟⇩∘ (T⦇ArrVal⦈)" by auto
  qed (use T.arr_Rel_ArrVal_vdomain in auto)

  show "ℛ⇩∘ (T⦇ArrVal⦈) = B"
  proof(intro vsubset_antisym vsubsetI)
    fix b assume "b ∈⇩∘ B"
    with val_TS have "⟨b, b⟩ ∈⇩∘ T⦇ArrVal⦈ ∘⇩∘ S⦇ArrVal⦈" by auto
    then show "b ∈⇩∘ ℛ⇩∘ (T⦇ArrVal⦈)" by auto
  qed (use T.arr_Rel_ArrVal_vrange in auto)

qed

end 

lemmas [cat_Rel_cs_simps] = cat_Rel_is_iso_arrD(3,4)

lemma cat_Rel_is_iso_arr:
  "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B ⟷
    T : A ↦⇘cat_Rel α⇙ B ∧
    v11 (T⦇ArrVal⦈) ∧
    𝒟⇩∘ (T⦇ArrVal⦈) = A ∧
    ℛ⇩∘ (T⦇ArrVal⦈) = B"
  by auto



subsection‹The inverse arrow›

lemma cat_Rel_the_inverse[cat_Rel_cs_simps]:
  assumes "T : A ↦⇩i⇩s⇩o⇘cat_Rel α⇙ B"
  shows "T¯⇩C⇘cat_Rel α⇙ = T¯⇩R⇩e⇩l"
  unfolding the_inverse_def
proof(rule the_equality)
  from assms have T: "T : A ↦⇘cat_Rel α⇙ B" by auto
  interpret T: arr_Rel α T by (intro cat_Rel_is_arrD[OF T])+
  interpret Rel: category α ‹cat_Rel α› by (rule T.category_cat_Rel)
  from assms T T.arr_Rel_axioms cat_Rel_is_iso_arrD(2)[OF assms] 
  show inv_T_T: "is_inverse (cat_Rel α) (T¯⇩R⇩e⇩l) T"
    by (intro is_inverseI[where a=A and b=B])
      (
        cs_concl 
          cs_simp: cat_cs_simps cat_Rel_cs_simps
          cs_intro: cat_Rel_cs_intros cat_cs_intros
      )+
  fix S assume "is_inverse (cat_Rel α) S T"
  then show "S = T¯⇩R⇩e⇩l"
    by (rule category.cat_is_inverse_eq[OF Rel.category_axioms _ inv_T_T])
qed

text‹\newpage›

end