Theory CZH_ECAT_Set

(* Copyright 2021 (C) Mihails Milehins *)

sectionSet›
theory CZH_ECAT_Set
  imports 
    CZH_Foundations.CZH_SMC_Set
    CZH_ECAT_Par
    CZH_ECAT_Subcategory
    CZH_ECAT_PCategory
begin



subsection‹Background›


text‹
The methodology chosen for the exposition of Set› as a category is 
analogous to the one used in cite"milehins_category_2021" 
for the exposition of Set› as a semicategory. 
›

named_theorems cat_Set_cs_simps
named_theorems cat_Set_cs_intros

lemmas (in arr_Set) [cat_Set_cs_simps] = 
  dg_Rel_shared_cs_simps

lemmas (in arr_Set) [cat_cs_intros, cat_Set_cs_intros] = 
  arr_Set_axioms'

lemmas [cat_Set_cs_simps] =
  dg_Rel_shared_cs_simps
  arr_Set.arr_Set_ArrVal_vdomain
  arr_Set_comp_Set_id_Set_left
  arr_Set_comp_Set_id_Set_right

lemmas [cat_Set_cs_intros] = 
  dg_Rel_shared_cs_intros
  arr_Set_comp_Set

(*
Certain lemmas are applicable to any of the categories among
Rel, Par, Set. If these lemmas are included in general-purpose
collections like cat_cs_simps/cat_cs_intros, then backtracking
can become slow. The following collections were created to resolve
such issues.
*)
named_theorems cat_rel_par_Set_cs_intros
named_theorems cat_rel_par_Set_cs_simps
named_theorems cat_rel_Par_set_cs_intros
named_theorems cat_rel_Par_set_cs_simps
named_theorems cat_Rel_par_set_cs_intros
named_theorems cat_Rel_par_set_cs_simps



subsectionSet› as a category›


subsubsection‹Definition and elementary properties›

definition cat_Set :: "V  V"
  where "cat_Set α =
    [
      Vset α,
      set {T. arr_Set α T},
      (λTset {T. arr_Set α T}. TArrDom),
      (λTset {T. arr_Set α T}. TArrCod),
      (λSTcomposable_arrs (dg_Set α). ST0 Rel ST1),
      VLambda (Vset α) id_Set 
    ]"


text‹Components.›

lemma cat_Set_components:
  shows "cat_Set αObj = Vset α"
    and "cat_Set αArr = set {T. arr_Set α T}"
    and "cat_Set αDom = (λTset {T. arr_Set α T}. TArrDom)"
    and "cat_Set αCod = (λTset {T. arr_Set α T}. TArrCod)"
    and "cat_Set αComp =
      (λSTcomposable_arrs (dg_Set α). ST0 Par ST1)"
    and "cat_Set αCId = VLambda (Vset α) id_Set"
  unfolding cat_Set_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_cat_Set: "cat_smc (cat_Set α) = smc_Set α"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟 (cat_smc (cat_Set α)) = 5" 
    unfolding cat_smc_def by (simp add: nat_omega_simps)
  have dom_rhs: "𝒟 (smc_Set α) = 5"
    unfolding smc_Set_def by (simp add: nat_omega_simps)
  show "𝒟 (cat_smc (cat_Set α)) = 𝒟 (smc_Set α)"
    unfolding dom_lhs dom_rhs by simp
  show "a  𝒟 (cat_smc (cat_Set α))  cat_smc (cat_Set α)a = smc_Set αa"
    for a
    by 
      (
        unfold dom_lhs, 
        elim_in_numeral, 
        unfold cat_smc_def dg_field_simps cat_Set_def smc_Set_def
      )
      (auto simp: nat_omega_simps)
qed (auto simp: cat_smc_def smc_Set_def)

lemmas_with [folded cat_smc_cat_Set, unfolded slicing_simps]:
  cat_Set_Obj_iff = smc_Set_Obj_iff
  and cat_Set_Arr_iff[cat_Set_cs_simps] = smc_Set_Arr_iff
  and cat_Set_Dom_vsv[intro] = smc_Set_Dom_vsv
  and cat_Set_Dom_vdomain[simp] = smc_Set_Dom_vdomain
  and cat_Set_Dom_vrange = smc_Set_Dom_vrange
  and cat_Set_Dom_app = smc_Set_Dom_app
  and cat_Set_Cod_vsv[intro] = smc_Set_Cod_vsv
  and cat_Set_Cod_vdomain[simp] = smc_Set_Cod_vdomain
  and cat_Set_Cod_vrange = smc_Set_Cod_vrange
  and cat_Set_Cod_app[cat_Set_cs_simps] = smc_Set_Cod_app
  and cat_Set_is_arrI = smc_Set_is_arrI
  and cat_Set_is_arrD = smc_Set_is_arrD
  and cat_Set_is_arrE = smc_Set_is_arrE
  and cat_Set_ArrVal_vdomain[cat_cs_simps] = smc_Set_ArrVal_vdomain
  and cat_Set_ArrVal_app_vrange[cat_Set_cs_intros] = smc_Set_ArrVal_app_vrange

lemmas [cat_cs_simps] = cat_Set_is_arrD(2,3)

lemmas [cat_Set_cs_intros] = 
  cat_Set_is_arrI

lemmas_with [folded cat_smc_cat_Set, unfolded slicing_simps]: 
  cat_Set_composable_arrs_dg_Set = smc_Set_composable_arrs_dg_Set
  and cat_Set_Comp = smc_Set_Comp
  and cat_Set_Comp_app[cat_Set_cs_simps] = smc_Set_Comp_app
  and cat_Set_Comp_vdomain[cat_Set_cs_simps] = smc_Set_Comp_vdomain
  and cat_Set_is_monic_arrI = smc_Set_is_monic_arrI
  and cat_Set_is_monic_arrD = smc_Set_is_monic_arrD
  and cat_Set_is_monic_arr = smc_Set_is_monic_arr
  and cat_Set_is_epic_arrI = smc_Set_is_epic_arrI
  and cat_Set_is_epic_arrD = smc_Set_is_epic_arrD
  and cat_Set_is_epic_arr = smc_Set_is_epic_arr

lemmas_with (in 𝒵) [folded cat_smc_cat_Set, unfolded slicing_simps]:
  cat_Set_Hom_vifunion_in_Vset = smc_Set_Hom_vifunion_in_Vset
  and cat_Set_incl_Set_is_arr = smc_Set_incl_Set_is_arr
  and cat_Set_Comp_ArrVal = smc_Set_Comp_ArrVal
  and cat_Set_Comp_vrange = smc_Set_Comp_vrange
  and cat_Set_obj_terminal = smc_Set_obj_terminal
  and cat_Set_obj_initial = smc_Set_obj_initial
  and cat_Set_obj_null = smc_Set_obj_null
  and cat_Set_is_zero_arr = smc_Set_is_zero_arr

lemmas [cat_cs_simps] = 
  𝒵.cat_Set_Comp_ArrVal

lemma (in 𝒵) cat_Set_incl_Set_is_arr'[cat_cs_intros, cat_Set_cs_intros]:
  assumes "A  cat_Set αObj"
    and "B  cat_Set αObj"
    and "A  B"
    and "A' = A"
    and "B' = B"
    and "ℭ' = cat_Set α"
  shows "incl_Set A B : A' ℭ'B'"
  using assms(1-3) unfolding assms(4-6) by (rule cat_Set_incl_Set_is_arr)

lemmas [cat_Set_cs_intros] = 𝒵.cat_Set_incl_Set_is_arr'


subsubsection‹Identity›

lemma cat_Set_CId_app[cat_Set_cs_simps]:
  assumes "A  Vset α"
  shows "cat_Set αCIdA = id_Set A"
  using assms unfolding cat_Set_components by simp

lemma cat_Set_CId_app_app[cat_cs_simps]:
  assumes "A  cat_Set αObj" and "a  A"
  shows "cat_Set αCIdAArrVala = a"
  unfolding 
    cat_Set_CId_app[OF assms(1)[unfolded cat_Set_components(1)]] 
    id_Rel_ArrVal_app[OF assms(2)] 
  by simp


subsubsectionSet› is a category›

lemma (in 𝒵) category_cat_Set: "category α (cat_Set α)"
proof(rule categoryI, unfold cat_smc_cat_Par cat_smc_cat_Set)

  interpret Set: semicategory α cat_smc (cat_Set α)
    unfolding cat_smc_cat_Set by (simp add: semicategory_smc_Set)

  show "vfsequence (cat_Set α)" unfolding cat_Set_def by simp
  show "vcard (cat_Set α) = 6"
    unfolding cat_Set_def by (simp add: nat_omega_simps)
  show "semicategory α (smc_Set α)" by (simp add: semicategory_smc_Set)
  show "cat_Set αCIdA : A cat_Set αA"
    if "A  cat_Set αObj" for A
    using that
    unfolding cat_Set_Obj_iff
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_Set_cs_simps cs_intro: cat_Set_cs_intros arr_Set_id_SetI
      )

  show "cat_Set αCIdB Acat_Set αF = F" 
    if "F : A cat_Set αB" for F A B
  proof-
    from that have "arr_Set α F" "B  Vset α" by (auto elim: cat_Set_is_arrE)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Set_cs_simps
            cs_intro: cat_Set_cs_intros arr_Set_id_SetI
        )
  qed

  show "F Acat_Set αcat_Set αCIdB = F"
    if "F : B cat_Set αC" for F B C
  proof-
    from that have "arr_Set α F" "B  Vset α" by (auto elim: cat_Set_is_arrE)
    with that show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_cs_simps cat_Set_cs_simps
            cs_intro: cat_Set_cs_intros arr_Set_id_SetI
        )
  qed

qed (auto simp: cat_Set_components)

lemma (in 𝒵) category_cat_Set':
  assumes "β = α"
  shows "category β (cat_Set α)"
  unfolding assms by (rule category_cat_Set)

lemmas [cat_cs_intros] = 𝒵.category_cat_Set'


subsubsectionSet› is a wide replete subcategory of Par›

lemma (in 𝒵) wide_replete_subcategory_cat_Set_cat_Par: 
  "cat_Set α C.wrαcat_Par α"
proof(intro wide_replete_subcategoryI)
  show wide_subcategory_cat_Set_cat_Par: "cat_Set α C.wideαcat_Par α"
  proof(intro wide_subcategoryI, unfold cat_smc_cat_Par cat_smc_cat_Set)
    interpret Par: category α cat_Par α by (rule category_cat_Par)
    interpret Set: category α cat_Set α by (rule category_cat_Set)
    interpret wide_subsemicategory α smc_Set α smc_Par α
      by (simp add: wide_subsemicategory_smc_Set_smc_Par)
    show "cat_Set α Cαcat_Par α"
    proof(intro subcategoryI, unfold cat_smc_cat_Par cat_smc_cat_Set)
      show "smc_Set α SMCαsmc_Par α" by (simp add: subsemicategory_axioms)
      fix A assume "A  cat_Set αObj"
      then show "cat_Set αCIdA = cat_Par αCIdA"
        unfolding cat_Set_components cat_Par_components by simp
    qed 
      (
        auto simp: 
          subsemicategory_axioms Par.category_axioms Set.category_axioms
      )
  qed (rule wide_subsemicategory_smc_Set_smc_Par)
  show "cat_Set α C.repαcat_Par α"
  proof(intro replete_subcategoryI)
    interpret wide_subcategory α cat_Set α cat_Par α
      by (rule wide_subcategory_cat_Set_cat_Par)
    show "cat_Set α Cαcat_Par α" by (rule subcategory_axioms)    
    fix A B F assume "F : A isocat_Par αB"
    note arr_Par = cat_Par_is_iso_arrD[OF this]
    from arr_Par show "F : A cat_Set αB"
      by (intro cat_Set_is_arrI arr_Set_arr_ParI cat_Par_is_arrD[OF arr_Par(1)])
        (auto simp: cat_Par_is_arrD(2))
  qed
qed


subsubsectionSet› is a subcategory of Set›

lemma (in 𝒵) subcategory_cat_Set_cat_Set:(*TODO: generalize*)
  assumes "𝒵 β" and "α  β"
  shows "cat_Set α Cβcat_Set β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  show ?thesis  
  proof(intro subcategoryI')
    show "category β (cat_Set α)"
      by (rule category.cat_category_if_ge_Limit, insert assms(2))
        (cs_concl cs_intro: cat_cs_intros cat_Rel_cs_intros)+
    show "A  cat_Set βObj" if "A  cat_Set αObj" for A 
      using that 
      unfolding cat_Set_components(1)
      by (meson assms(2) Vset_in_mono β.Axiom_of_Extensionality(3))
    show is_arr_if_is_arr: 
      "F : A cat_Set βB" if "F : A cat_Set αB" for A B F
    proof-
      note f = cat_Set_is_arrD[OF that]
      interpret f: arr_Set α F by (rule f(1))
      show ?thesis
      proof(intro cat_Set_is_arrI arr_SetI)
        show " (FArrVal)  FArrCod"  
           by (auto simp: f.arr_Set_ArrVal_vrange)
        show "FArrDom  Vset β"
          by (auto intro!: f.arr_Set_ArrDom_in_Vset Vset_in_mono assms(2))
        show "FArrCod  Vset β"
          by (auto intro!: f.arr_Set_ArrCod_in_Vset Vset_in_mono assms(2))
      qed 
        (
          auto simp: 
            f f.arr_Set_ArrVal_vdomain f.vfsequence_axioms f.arr_Set_length
        )
    qed
    show "G Acat_Set αF = G Acat_Set βF"
      if "G : B cat_Set αC" and "F : A cat_Set αB" for B C G A F
    proof-
      note g = cat_Set_is_arrD[OF that(1)] and f = cat_Set_is_arrD[OF that(2)]      
      from that have α_gf_is_arr: "G Acat_Set αF : A cat_Set βC"
        by (cs_concl cs_intro: cat_cs_intros is_arr_if_is_arr)
      from that have β_gf_is_arr: "G Acat_Set βF : A cat_Set βC"
        by (cs_concl cs_intro: cat_cs_intros is_arr_if_is_arr)
      note α_gf = cat_Set_is_arrD[OF α_gf_is_arr]
        and β_gf = cat_Set_is_arrD[OF β_gf_is_arr]
      show ?thesis
      proof(rule arr_Set_eqI)
        show "arr_Set β (G Acat_Set αF)" by (rule α_gf(1))
        then interpret arr_Set_α_gf: arr_Set β (G Acat_Set αF) by simp
        from α_gf_is_arr have dom_lhs: "𝒟 ((G Acat_Set αF)ArrVal) = A"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        show "arr_Set β (G Acat_Set βF)" by (rule β_gf(1))
        then interpret arr_Set_β_gf: arr_Set β (G Acat_Set βF) by simp
        from β_gf_is_arr have dom_rhs: "𝒟 ((G Acat_Set βF)ArrVal) = A"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        show "(G Acat_Set αF)ArrVal = (G Acat_Set βF)ArrVal"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume "a  A"
          from that this show 
            "(G Acat_Set αF)ArrVala = (G Acat_Set βF)ArrVala"
            by 
              (
                cs_concl cs_shallow
                  cs_simp: cat_cs_simps cs_intro: cat_cs_intros is_arr_if_is_arr
              )
        qed auto
      qed 
        (
          use α_gf_is_arr β_gf_is_arr in 
            cs_concl cs_shallow cs_simp: cat_cs_simps
        )+
    qed
  qed 
    (
      auto simp: 
        assms(2) cat_Set_components Vset_trans Vset_in_mono cat_cs_intros
    )
qed


subsubsection‹Further properties›

lemma cat_Set_Comp_ArrVal_vrange: (*FIXME: generalize/migrate*)
  assumes "S : B cat_Set αC" and "T : A cat_Set αB" 
  shows " ((S Acat_Set αT)ArrVal)   (SArrVal)" 
proof(intro vsubsetI)
  note SD = cat_Set_is_arrD[OF assms(1)]
  interpret S: arr_Set α S 
    rewrites "SArrDom = B" and "SArrCod = C"
    by (intro SD)+
  from assms(1,2) have "S Acat_Set αT : A cat_Set αC"
    by (cs_concl cs_intro: cat_cs_intros)
  note ST = cat_Set_is_arrD[OF this]
  interpret ST: arr_Set α S Acat_Set αT
    rewrites "(S Acat_Set αT)ArrDom = A" 
      and "(S Acat_Set αT)ArrCod = C"
    by (intro ST)+
  fix y assume prems: "y   ((S Acat_Set αT)ArrVal)"
  with ST.arr_Set_ArrVal_vdomain obtain x 
    where x: "x  A" and y_def: "y = (S Acat_Set αT)ArrValx"
    by force
  show "y   (SArrVal)"
  proof(intro S.ArrVal.vsv_vimageI2', unfold cat_Set_cs_simps)
    from assms(1,2) x show "y = SArrValTArrValx"
      unfolding y_def 
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(2) x show "TArrValx  B"
      by (cs_concl cs_intro: cat_Set_cs_intros)
  qed
qed



subsection‹Isomorphism›

lemma cat_Set_is_iso_arrI[intro]:
  ―‹
  See \cite{noauthor_nlab_nodate}\footnote{\url{
  https://ncatlab.org/nlab/show/isomorphism
  }}).
  ›
  assumes "T : A cat_Set αB" 
    and "v11 (TArrVal)"
    and "𝒟 (TArrVal) = A"
    and " (TArrVal) = B"
  shows "T : A isocat_Set αB"
proof-
  interpret T: arr_Set α T by (rule cat_Set_is_arrD(1)[OF assms(1)])
  note [cat_cs_intros] = cat_Par_is_iso_arrI
  from T.wide_replete_subcategory_cat_Set_cat_Par assms have 
    "T : A isocat_Par αB"
    by (cs_concl cs_intro: cat_cs_intros cat_sub_cs_intros cat_sub_fw_cs_intros)
  with T.wide_replete_subcategory_cat_Set_cat_Par assms show 
    "T : A isocat_Set αB"
    by (cs_concl cs_shallow cs_simp: cat_sub_bw_cs_simps)
qed

lemma cat_Set_is_iso_arrD[dest]:
  assumes "T : A isocat_Set αB"
  shows "T : A cat_Set αB"
    and "v11 (TArrVal)"
    and "𝒟 (TArrVal) = A"
    and " (TArrVal) = B"
proof-
  from assms have T: "T : A cat_Set αB" by auto
  interpret T: arr_Set α T by (rule cat_Set_is_arrD(1)[OF T])
  from T.wide_replete_subcategory_cat_Set_cat_Par assms have T: 
    "T : A isocat_Par αB"
    by (cs_concl cs_shallow cs_intro: cat_sub_cs_intros cat_sub_fw_cs_intros)
  show "v11 (TArrVal)" "𝒟 (TArrVal) = A" " (TArrVal) = B"
    by (intro cat_Par_is_iso_arrD[OF T])+
qed (rule is_iso_arrD(1)[OF assms])

lemma cat_Set_is_iso_arr:
  "T : A isocat_Set αB  
    T : A cat_Set αB 
    v11 (TArrVal)  
    𝒟 (TArrVal) = A  
     (TArrVal) = B"
  by auto

lemma (in 𝒵) cat_Set_is_iso_arr_if_monic_and_epic:
  assumes "F : A moncat_Set αB" and "F : A epicat_Set αB"
  shows "F : A isocat_Set αB"
proof-
  note cat_Set_is_monic_arrD[OF assms(1)] cat_Set_is_epic_arrD[OF assms(2)]
  note FD = this(1,2,3,5) cat_Set_is_arrD[OF this(1)]
  show ?thesis by (intro cat_Set_is_iso_arrI FD)
qed



subsection‹The inverse arrow›

lemma cat_Set_ArrVal_app_is_arr[cat_cs_intros]:
  assumes "f : a 𝔄b" 
    and "category α 𝔄" (*the order of premises is important*)
    and "F : Hom 𝔄 a b cat_Set αHom 𝔅 c d"
  shows "FArrValf : c 𝔅d"
proof-
  interpret 𝔄: category α 𝔄 by (rule assms(2))
  interpret F: arr_Set α F by (rule cat_Set_is_arrD[OF assms(3)])  
  from assms have "FArrValf  Hom 𝔅 c d"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Set_cs_intros)
  then show ?thesis unfolding in_Hom_iff by simp
qed

abbreviation (input) converse_Set :: "V  V" ("(_¯Set)" [1000] 999)
  where "a¯Set  a¯Rel"

lemma cat_Set_the_inverse[cat_Set_cs_simps]:
  assumes "T : A isocat_Set αB"
  shows "T¯Ccat_Set α= T¯Set"
proof-
  from assms have T: "T : A cat_Set αB" by auto
  interpret arr_Set α T by (rule cat_Set_is_arrD(1)[OF T])
  from wide_replete_subcategory_cat_Set_cat_Par assms have T:
    "T : A isocat_Par αB"
    by (cs_concl cs_shallow cs_intro: cat_sub_cs_intros cat_sub_fw_cs_intros)
  from wide_replete_subcategory_cat_Set_cat_Par assms 
  have [symmetric, cat_cs_simps]: "T¯Ccat_Par α= T¯Ccat_Set α⇙"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_sub_bw_cs_simps cs_intro: cat_sub_cs_intros
      )
  from T show "T¯Ccat_Set α= T¯Set"
    by (cs_concl cs_shallow cs_simp: cat_Par_cs_simps cat_cs_simps cs_intro: 𝒵_β)
qed

lemma cat_Set_the_inverse_app[cat_cs_intros]:
  assumes "T : A isocat_Set αB"
    and "a  A"
    and [cat_cs_simps]: "TArrVala = b"
  shows "(T¯Ccat_Set α)ArrValb = a"
proof-
  from assms have T: "T : A cat_Set αB" by auto
  interpret arr_Set α T by (rule cat_Set_is_arrD(1)[OF T])
  note T = cat_Set_is_iso_arrD[OF assms(1)]
  interpret T: v11 TArrVal by (rule T(2))
  from T.v11_axioms assms(1,2) show "T¯Ccat_Set αArrValb = a"
    by
      (
        cs_concl cs_shallow
          cs_simp: 
            converse_Rel_components V_cs_simps cat_Set_cs_simps cat_cs_simps 
          cs_intro: cat_arrow_cs_intros cat_cs_intros
      )
qed
                                                          
lemma cat_Set_ArrVal_app_the_inverse_is_arr[cat_cs_intros]:
  assumes "f : c 𝔅d" 
    and "category α 𝔅" (*the order of premises is important*)
    and "F : Hom 𝔄 a b isocat_Set αHom 𝔅 c d"
  shows "F¯Ccat_Set αArrValf : a 𝔄b"
proof-
  interpret 𝔅: category α 𝔅 by (rule assms(2))
  from cat_Set_is_iso_arrD[OF assms(3)] interpret F: arr_Set α F 
    by (simp add: cat_Set_is_arrD)  
  from assms have "F¯Ccat_Set αArrValf  Hom 𝔄 a b"
    by (cs_concl cs_intro: cat_cs_intros cat_arrow_cs_intros)
  then show ?thesis unfolding in_Hom_iff by simp
qed

lemma cat_Set_app_the_inverse_app[cat_cs_simps]:
  assumes "F : A isocat_Set αB" and "b  B"
  shows "FArrValF¯Ccat_Set αArrValb = b"
proof-
  note F = cat_Set_is_iso_arrD[OF assms(1)]
  note F = F cat_Set_is_arrD[OF F(1)]
  interpret F: arr_Set α F by (rule cat_Set_is_arrD[OF F(1)])  
  from assms have [cat_cs_simps]: 
    "F Acat_Set αF¯Ccat_Set α= cat_Set αCIdB"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms have [cat_cs_simps]: 
    "FArrValF¯Ccat_Set αArrValb = 
      (F Acat_Set αF¯Ccat_Set α)ArrValb"
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cs_intro: cat_arrow_cs_intros cat_cs_intros
      )
  from assms F(1) F.arr_Par_ArrCod_in_Vset[unfolded F] show ?thesis
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed

lemma cat_Set_the_inverse_app_app[cat_cs_simps]:
  assumes "F : A isocat_Set αB" and "a  A"
  shows "F¯Ccat_Set αArrValFArrVala = a"
proof-
  note F = cat_Set_is_iso_arrD[OF assms(1)]
  note F = F cat_Set_is_arrD[OF F(1)]
  interpret F: arr_Set α F by (rule cat_Set_is_arrD[OF F(1)])  
  from assms have [cat_cs_simps]:
    "F¯Ccat_Set αAcat_Set αF = cat_Set αCIdA"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms have [cat_cs_simps]: 
    "F¯Ccat_Set αArrValFArrVala =
      (F¯Ccat_Set αAcat_Set αF)ArrVala"
    by
      (
        cs_concl 
          cs_simp: cat_cs_simps cs_intro: cat_arrow_cs_intros cat_cs_intros
      )
  from assms F(1) F.arr_Par_ArrDom_in_Vset[unfolded F] show ?thesis
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
qed



subsection‹Conversion of a single-valued relation to an arrow in Set›


subsubsection‹Definition and elementary properties›


definition cat_Set_arr_of_vsv :: "V  V  V"
  where "cat_Set_arr_of_vsv f B = [f, 𝒟 f, B]"


text‹Components.›

lemma cat_Set_arr_of_vsv_components:
  shows [cat_Set_cs_simps]: "cat_Set_arr_of_vsv f BArrVal = f"
    and [cat_Set_cs_simps]: "cat_Set_arr_of_vsv f BArrDom = 𝒟 f"
    and [cat_cs_simps, cat_Set_cs_simps]: "cat_Set_arr_of_vsv f BArrCod = B"
  unfolding cat_Set_arr_of_vsv_def arr_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹
Conversion of a single-valued relation to an arrow in Set› is an arrow in Set›

lemma (in 𝒵) cat_Set_arr_of_vsv_is_arr:
  assumes "vsv r" 
    and " r  B" 
    and "𝒟 r  cat_Set αObj" 
    and "B  cat_Set αObj"
  shows "cat_Set_arr_of_vsv r B : 𝒟 r cat_Set αB"
proof-
  interpret r: vsv r by (rule assms)
  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI, unfold cat_Set_arr_of_vsv_components)
    show "vfsequence (cat_Set_arr_of_vsv r B)"
      unfolding cat_Set_arr_of_vsv_def by auto
    show "vcard (cat_Set_arr_of_vsv r B) = 3"
      unfolding cat_Set_arr_of_vsv_def by (auto simp: nat_omega_simps)
  qed (use assms in auto simp: cat_Set_components)
qed



subsection‹Left restriction for Set›


subsubsection‹Definition and elementary properties›

definition vlrestriction_Set :: "V  V  V" (infixr lSet 80)
  where "T lSet C = [TArrVal l C, C, TArrCod]"


text‹Components.›

lemma vlrestriction_Set_components:
  shows [cat_Set_cs_simps]: "(T lSet C)ArrVal = TArrVal l C"
    and [cat_cs_simps, cat_Set_cs_simps]: "(T lSet C)ArrDom = C"
    and [cat_cs_simps, cat_Set_cs_simps]: "(T lSet C)ArrCod = TArrCod"
  unfolding vlrestriction_Set_def arr_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

lemma vlrestriction_Set_ArrVal_vdomain[cat_cs_simps]:
  assumes "T : A cat_Set αB" and "C  A" 
  shows "𝒟 ((T lSet C)ArrVal) = C"
proof-
  note TD = cat_Set_is_arrD[OF assms(1)]
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro TD)+
  from assms show ?thesis
    unfolding vlrestriction_Set_components
    by (cs_concl cs_simp: V_cs_simps cat_cs_simps cs_intro: V_cs_intros)
qed

lemma vlrestriction_Set_ArrVal_app[cat_cs_simps]:
  assumes "T : A cat_Set αB" and "C  A" and "x  C" 
  shows "(T lSet C)ArrValx = TArrValx"
proof-
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro cat_Set_is_arrD[OF assms(1)])+
  from assms have x: "x  A" by auto
  with assms show ?thesis 
    unfolding vlrestriction_Set_components
    by (cs_concl cs_simp: V_cs_simps cat_cs_simps cs_intro: V_cs_intros)
qed


subsubsection‹Left restriction for Set› is an arrow in Set›

lemma vlrestriction_Set_is_arr:
  assumes "T : A cat_Set αB" and "C  A"
  shows "T lSet C : C cat_Set αB"
proof-
  note TD = cat_Set_is_arrD[OF assms(1)]
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro TD)+
  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI, unfold cat_Set_cs_simps TD(2,3))
    show "vfsequence (T lSet C)"
      unfolding vlrestriction_Set_def by auto
    show "vcard (T lSet C) = 3"
      unfolding vlrestriction_Set_def by (simp add: nat_omega_simps)
    from assms show "𝒟 (TArrVal l C) = C"
      by (cs_concl cs_simp: V_cs_simps cat_cs_simps cs_intro: cat_cs_intros)
    show " (TArrVal l C)  B"
      unfolding app_vimage_def[symmetric]
    proof(intro vsubsetI)
      fix x assume prems: "x  TArrVal ` C"
      then obtain c where "c  C" and x_def: "x = TArrValc" by auto
      with assms(2) have c: "c  A" by auto
      from c assms show "x  B"
        unfolding x_def by (cs_concl cs_intro: cat_Set_cs_intros)
    qed
    from assms(2) show "C  Vset α"
      using vsubset_in_VsetI by (auto simp: T.arr_Set_ArrDom_in_Vset)
  qed (auto simp: T.arr_Set_ArrCod_in_Vset)
qed

lemma (in 𝒵) vlrestriction_Set_is_monic_arr:
  assumes "T : A moncat_Set αB" and "C  A"
  shows "T lSet C : C moncat_Set αB"
proof-
  note cat_Set_is_monic_arrD[OF assms(1)]
  note TD = this cat_Set_is_arrD[OF this(1)]
  interpret F: arr_Set α T by (intro TD)+
  interpret ArrVal: v11 TArrVal by (rule TD(2))
  show ?thesis
  proof
    (
      intro 
        cat_Set_is_monic_arrI 
        vlrestriction_Set_is_arr[OF TD(1) assms(2)],
      unfold cat_Set_cs_simps
    )
    from TD(1) assms(2) show "𝒟 (TArrVal l C) = C"
      by (cs_concl cs_simp: V_cs_simps cat_cs_simps)
  qed auto
qed



subsection‹Right restriction for Set›


subsubsection‹Definition and elementary properties›

definition vrrestriction_Set :: "V  V  V" (infixr rSet 80)
  where "T rSet C = [TArrVal r C, TArrDom, C]"


text‹Components.›

lemma vrrestriction_Set_components:
  shows [cat_Set_cs_simps]: "(T rSet C)ArrVal = TArrVal r C"
    and [cat_cs_simps, cat_Set_cs_simps]: "(T rSet C)ArrDom = TArrDom"
    and [cat_cs_simps, cat_Set_cs_simps]: "(T rSet C)ArrCod = C"
  unfolding vrrestriction_Set_def arr_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

lemma vrrestriction_Set_ArrVal_app[cat_cs_simps]:
  assumes "T : A cat_Set αB" and " (TArrVal)  C" 
  shows "(T rSet C)ArrVal = TArrVal"
proof-
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro cat_Set_is_arrD[OF assms(1)])+
  from assms show ?thesis unfolding cat_Set_cs_simps by simp
qed


subsubsection‹Right restriction for Set› is an arrow in Set›

lemma vrrestriction_Set_is_arr:
  assumes "T : A cat_Set αB" 
    and " (TArrVal)  C" 
    and "C  cat_Set αObj"
  shows "T rSet C : A cat_Set αC"
proof-
  note TD = cat_Set_is_arrD[OF assms(1)]
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro TD)+
  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI, unfold cat_Set_cs_simps)
    show "vfsequence (T rSet C)" unfolding vrrestriction_Set_def by auto
    show "vcard (T rSet C) = 3"
      unfolding vrrestriction_Set_def by (simp add: nat_omega_simps)
  qed
    (
      use assms(2,3) in
        auto simp:
            TD(2)
            cat_Set_components
            T.arr_Set_ArrVal_vdomain
            T.arr_Set_ArrDom_in_Vset
    )
qed

lemma vrrestriction_Set_is_arr'[cat_cs_intros]:
  assumes "T : A cat_Set αB" 
    and " (TArrVal)  C" 
    and "C  cat_Set αObj"
    and "C' = C"
    and "ℭ' = cat_Set α"
  shows "T rSet C : A ℭ'C'"
  using assms(1-3) unfolding assms(4,5) by (rule vrrestriction_Set_is_arr)


subsubsection‹Further properties›

lemma 
  assumes "T : A cat_Set αB" 
  shows vrrestriction_Set_vrange_is_arr: 
      "T rSet  (TArrVal) : A cat_Set α (TArrVal)"
    and vrrestriction_Set_vrange_ArrVal_app[cat_cs_simps, cat_Set_cs_simps]: 
      "(T rSet  (TArrVal))ArrVal = TArrVal"
proof(intro vrrestriction_Set_is_arr, rule assms)
  note TD = cat_Set_is_arrD[OF assms(1)]
  interpret T: arr_Set α T
    rewrites "TArrDom = A" and "TArrCod = B"
    by (intro TD)+
  show " (TArrVal)  cat_Set αObj"
    by (auto simp: cat_Set_components T.arr_Rel_ArrVal_in_Vset vrange_in_VsetI)
qed (auto intro: vrrestriction_Set_ArrVal_app[OF assms])

lemma (in 𝒵) vrrestriction_Set_vrange_is_iso_arr:
  assumes "T : A moncat_Set αB" 
  shows "T rSet  (TArrVal) : A isocat_Set α (TArrVal)"
proof-
  note cat_Set_is_monic_arrD[OF assms]
  note TD = this cat_Set_is_arrD[OF this(1)]
  interpret T: arr_Set α T by (intro TD)+
  show ?thesis
    by 
      (
        intro cat_Set_is_iso_arrI vrrestriction_Set_vrange_is_arr[OF TD(1)],
        unfold cat_Set_cs_simps
      )
      (simp_all add: TD(2,3))
qed


subsubsection‹Connections›

lemma cat_Set_Comp_vrrestriction_Set:
  assumes "S : B cat_Set αC" 
    and "T : A cat_Set αB" 
    and " (SArrVal)  D"
    and "D  cat_Set αObj"
  shows "S rSet D Acat_Set αT = (S Acat_Set αT) rSet D"
proof-

  note SD = cat_Set_is_arrD[OF assms(1)]
  interpret S: arr_Set α S 
    rewrites [cat_cs_simps]: "SArrDom = B" and [cat_cs_simps]: "SArrCod = C"
    by (intro SD)+
  note TD = cat_Set_is_arrD[OF assms(2)]
  interpret T: arr_Set α T 
    rewrites [cat_cs_simps]: "TArrDom = A" and [cat_cs_simps]: "TArrCod = B"
    by (intro TD)+

  from assms(3) S.arr_Par_ArrVal_vrange have RS_D: " (SArrVal)  D" by auto

  from assms(1,2) have "S Acat_Set αT : A cat_Set αC"
    by (cs_concl cs_intro: cat_cs_intros)

  from assms(1,2) have " ((S Acat_Set αT)ArrVal)   (SArrVal)" 
    by (intro cat_Set_Comp_ArrVal_vrange)
  with assms(3) have RST: " ((S Acat_Set αT)ArrVal)  D" by auto

  from assms(1,2,4) RS_D have SD_T: 
    "S rSet D Acat_Set αT : A cat_Set αD" 
    by (cs_concl cs_intro: cat_cs_intros) 
  then have dom_lhs: "𝒟 ((S rSet D Acat_Set αT)ArrVal) = A"
    by (simp add: cat_cs_simps)

  from assms(1,2,4) RST have ST_D: 
    "(S Acat_Set αT) rSet D : A cat_Set αD"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟 (((S Acat_Set αT) rSet D)ArrVal) = A"
    by (simp add: cat_cs_simps)

  show "S rSet D Acat_Set αT = (S Acat_Set αT) rSet D"
  proof(rule arr_Set_eqI[of α])
    show 
      "(S rSet D Acat_Set αT)ArrVal =
        ((S Acat_Set αT) rSet D)ArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a  A"
      with assms(1,2,4) RST RS_D show
        "(S rSet D Acat_Set αT)ArrVala = 
          ((S Acat_Set αT) rSet D)ArrVala"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use SD_T ST_D in auto dest: cat_Set_is_arrD) 
  qed (use SD_T ST_D in auto simp: cat_Set_is_arrD) 

qed

lemma (in 𝒵) cat_Set_CId_vrrestriction_Set[cat_cs_simps]:
  assumes "A  B" and "B  cat_Set αObj"
  shows "cat_Set αCIdA rSet B = incl_Set A B"
proof-

  from assms have A: "A  cat_Set αObj"
    unfolding cat_Set_components by auto
  from A have CId_A: "cat_Set αCIdA : A cat_Set αA"
    by (cs_concl cs_intro: cat_cs_intros)
  with cat_Set_is_arrD[OF CId_A] assms(1) have RA_B:
    " (cat_Set αCIdAArrVal)  B"
    by (auto intro: arr_Set.arr_Set_ArrVal_vrange)

  with assms A assms(1,2) have lhs_is_arr:
    "cat_Set αCIdA rSet B : A cat_Set αB"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟 ((cat_Set αCIdA rSet B)ArrVal) = A"
    by (simp add: cat_cs_simps)

  from A assms(1,2) have rhs_is_arr: "incl_Set A B : A cat_Set αB"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_rhs: "𝒟 ((incl_Set A B)ArrVal) = A"
    by (simp add: cat_cs_simps)

  show ?thesis
  proof(rule arr_Set_eqI[of α])
    show "(cat_Set αCIdA rSet B)ArrVal = incl_Rel A BArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a  A"
      with A RA_B show 
        "(cat_Set αCIdA rSet B)ArrVala = incl_Rel A BArrVala"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use lhs_is_arr rhs_is_arr in auto dest: cat_Set_is_arrD)
  qed (use lhs_is_arr rhs_is_arr in auto simp: cat_Set_is_arrD)

qed

lemma cat_Set_Comp_incl_Rel_vrrestriction_Set[cat_cs_simps]:
  assumes "F : A cat_Set αB" and "C  B" and " (FArrVal)  C"
  shows "incl_Rel C B Acat_Set αF rSet C = F"
proof-
  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret F: arr_Set α F 
    rewrites [cat_cs_simps]: "FArrDom = A" and [cat_cs_simps]: "FArrCod = B"
    by (intro FD)+
  from assms(2) have C: "C  cat_Set αObj"
    unfolding cat_Set_components(1) by (auto intro: F.arr_Par_ArrCod_in_Vset)
  from assms C have lhs_is_arr:
    "incl_Rel C B Acat_Set αF rSet C : A cat_Set αB"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟 ((incl_Rel C B Acat_Set αF rSet C)ArrVal) = A"
    by (cs_concl cs_simp: cat_cs_simps)
  from assms(1) have dom_rhs: "𝒟 (FArrVal) = A" 
    by (cs_concl cs_simp: cat_cs_simps)
  show ?thesis
  proof(rule arr_Set_eqI[of α])
    show "(incl_Rel C B Acat_Set αF rSet C)ArrVal = FArrVal"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems: "a  A"
      with assms F.ArrVal.vsv_vimageI2 have "FArrVala  C"
        by (auto simp: F.arr_Set_ArrVal_vdomain)
      with prems assms C show 
        "(incl_Rel C B Acat_Set αF rSet C)ArrVala = FArrVala"
        by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    qed (use assms(1) lhs_is_arr in auto dest: cat_Set_is_arrD)
  qed (use assms(1) lhs_is_arr in auto dest: cat_Set_is_arrD)
qed



subsection‹Projection arrows for vtimes›


subsubsection‹Definition and elementary properties›

definition vfst_arrow :: "V  V  V"
  where "vfst_arrow A B = [(λabA × B. vfst ab), A × B, A]"

definition vsnd_arrow :: "V  V  V"
  where "vsnd_arrow A B = [(λabA × B. vsnd ab), A × B, B]"


text‹Components.›

lemma vfst_arrow_components: 
  shows "vfst_arrow A BArrVal = (λabA × B. vfst ab)"
    and [cat_cs_simps]: "vfst_arrow A BArrDom = A × B"
    and [cat_cs_simps]: "vfst_arrow A BArrCod = A"
  unfolding vfst_arrow_def arr_field_simps by (simp_all add: nat_omega_simps)

lemma vsnd_arrow_components: 
  shows "vsnd_arrow A BArrVal = (λabA × B. vsnd ab)"
    and [cat_cs_simps]: "vsnd_arrow A BArrDom = A × B"
    and [cat_cs_simps]: "vsnd_arrow A BArrCod = B"
  unfolding vsnd_arrow_def arr_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda vfst_arrow_components(1)
  |vsv vfst_arrow_ArrVal_vsv[cat_cs_intros]|
  |vdomain vfst_arrow_ArrVal_vdomain[cat_cs_simps]|
  |app vfst_arrow_ArrVal_app'|

mk_VLambda vsnd_arrow_components(1)
  |vsv vsnd_arrow_ArrVal_vsv[cat_cs_intros]|
  |vdomain vsnd_arrow_ArrVal_vdomain[cat_cs_simps]|
  |app vsnd_arrow_ArrVal_app'|

lemma vfst_arrow_ArrVal_app[cat_cs_simps]:
  assumes "ab = a, b" and "ab  A × B"
  shows "vfst_arrow A BArrValab = a"
  using assms(2) unfolding assms(1) by (simp add: vfst_arrow_ArrVal_app')

lemma vfst_arrow_vrange: " (vfst_arrow A BArrVal)  A"
  unfolding vfst_arrow_components
proof(intro vrange_VLambda_vsubset)
  fix ab assume "ab  A × B"
  then obtain a b where ab_def: "ab = a, b" and a: "a  A" by clarsimp
  from a show "vfst ab  A" unfolding ab_def by simp
qed

lemma vsnd_arrow_ArrVal_app[cat_cs_simps]:
  assumes "ab = a, b" and "ab  A × B"
  shows "vsnd_arrow A BArrValab = b"
  using assms(2) unfolding assms(1) by (simp add: vsnd_arrow_ArrVal_app')

lemma vsnd_arrow_vrange: " (vsnd_arrow A BArrVal)  B"
  unfolding vsnd_arrow_components
proof(intro vrange_VLambda_vsubset)
  fix ab assume "ab  A × B"
  then obtain a b where ab_def: "ab = a, b" and b: "b  B" by clarsimp
  from b show "vsnd ab  B" unfolding ab_def by simp
qed


subsubsection‹Projection arrows are arrows in the category Set›

lemma (in 𝒵) vfst_arrow_is_cat_Set_arr_Vset:
  assumes "A  Vset α" and "B  Vset α"
  shows "vfst_arrow A B : A × B cat_Set αA"
proof(intro cat_Set_is_arrI arr_SetI, unfold cat_cs_simps)
  show "vfsequence (vfst_arrow A B)" unfolding vfst_arrow_def by simp
  show "vcard (vfst_arrow A B) = 3"
    unfolding vfst_arrow_def by (simp add: nat_omega_simps)
  show " (vfst_arrow A BArrVal)  A" by (rule vfst_arrow_vrange)
qed (use assms in cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros)+

lemma (in 𝒵) vfst_arrow_is_cat_Set_arr:
  assumes "A  cat_Set αObj" and "B  cat_Set αObj"
  shows "vfst_arrow A B : A × B cat_Set αA"
  using assms 
  unfolding cat_Set_components 
  by (rule vfst_arrow_is_cat_Set_arr_Vset)

lemma (in 𝒵) vfst_arrow_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
  assumes "A  cat_Set αObj" 
    and "B  cat_Set αObj"
    and "AB = A × B"
    and "A' = A"
    and "ℭ' = cat_Set α"
  shows "vfst_arrow A B : AB ℭ'A'"
  using assms(1-2) unfolding assms(3-5) by (rule vfst_arrow_is_cat_Set_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.vfst_arrow_is_cat_Set_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Set_arr_Vset:
  assumes "A  Vset α" and "B  Vset α"
  shows "vsnd_arrow A B : A × B cat_Set αB"
proof(intro cat_Set_is_arrI arr_SetI , unfold cat_cs_simps)
  show "vfsequence (vsnd_arrow A B)" unfolding vsnd_arrow_def by simp
  show "vcard (vsnd_arrow A B) = 3"
    unfolding vsnd_arrow_def by (simp add: nat_omega_simps)
  show " (vsnd_arrow A BArrVal)  B" by (rule vsnd_arrow_vrange)
qed (use assms in cs_concl cs_shallow cs_intro: V_cs_intros cat_cs_intros)+

lemma (in 𝒵) vsnd_arrow_is_cat_Set_arr:
  assumes "A  cat_Set αObj" and "B  cat_Set αObj"
  shows "vsnd_arrow A B : A × B cat_Set αB"
  using assms 
  unfolding cat_Set_components 
  by (rule vsnd_arrow_is_cat_Set_arr_Vset)

lemma (in 𝒵) vsnd_arrow_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
  assumes "A  cat_Set αObj" 
    and "B  cat_Set αObj"
    and "AB = A × B"
    and "B' = B"
    and "ℭ' = cat_Set α"
  shows "vsnd_arrow A B : AB ℭ'B'"
  using assms(1-2) unfolding assms(3-5) by (rule vsnd_arrow_is_cat_Set_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Set_arr'


subsubsection‹Projection arrows are arrows in the category Par›

lemma (in 𝒵) vfst_arrow_is_cat_Par_arr:
  assumes "A  cat_Par αObj" and "B  cat_Par αObj"
  shows "vfst_arrow A B : A × B cat_Par αA"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  from assms show ?thesis
    unfolding cat_Par_components(1)
    by (intro Set_Par.subcat_is_arrD vfst_arrow_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) vfst_arrow_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
  assumes "A  cat_Par αObj" 
    and "B  cat_Par αObj"
    and "AB = A × B"
    and "A' = A"
    and "ℭ' = cat_Par α"
  shows "vfst_arrow A B : AB ℭ'A'"
  using assms(1-2) unfolding assms(3-5) by (rule vfst_arrow_is_cat_Par_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.vfst_arrow_is_cat_Par_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Par_arr:
  assumes "A  cat_Par αObj" and "B  cat_Par αObj"
  shows "vsnd_arrow A B : A × B cat_Par αB"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  from assms show ?thesis
    unfolding cat_Par_components(1)
    by (intro Set_Par.subcat_is_arrD vsnd_arrow_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) vsnd_arrow_is_cat_Par_arr'[cat_rel_Par_set_cs_intros]:
  assumes "A  cat_Par αObj" 
    and "B  cat_Par αObj"
    and "AB = A × B"
    and "B' = B"
    and "ℭ' = cat_Par α"
  shows "vsnd_arrow A B : AB ℭ'B'"
  using assms(1-2) unfolding assms(3-5) by (rule vsnd_arrow_is_cat_Par_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Par_arr'


subsubsection‹Projection arrows are arrows in the category Rel›

lemma (in 𝒵) vfst_arrow_is_cat_Rel_arr:
  assumes "A  cat_Rel αObj" and "B  cat_Rel αObj"
  shows "vfst_arrow A B : A × B cat_Rel αA"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  interpret Par_Rel: wide_replete_subcategory α cat_Par α cat_Rel α 
    by (rule wide_replete_subcategory_cat_Par_cat_Rel)
  interpret Set_Rel: subcategory α cat_Set α cat_Rel α 
    by 
      ( 
        rule subcat_trans[
          OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
          ]
      )
  from assms show ?thesis
    unfolding cat_Rel_components(1)
    by (intro Set_Rel.subcat_is_arrD vfst_arrow_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) vfst_arrow_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
  assumes "A  cat_Rel αObj" 
    and "B  cat_Rel αObj"
    and "AB = A × B"
    and "A' = A"
    and "ℭ' = cat_Rel α"
  shows "vfst_arrow A B : AB ℭ'A'"
  using assms(1-2) unfolding assms(3-5) by (rule vfst_arrow_is_cat_Rel_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.vfst_arrow_is_cat_Rel_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Rel_arr:
  assumes "A  cat_Rel αObj" and "B  cat_Rel αObj"
  shows "vsnd_arrow A B : A × B cat_Rel αB"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  interpret Par_Rel: wide_replete_subcategory α cat_Par α cat_Rel α 
    by (rule wide_replete_subcategory_cat_Par_cat_Rel)
  interpret Set_Rel: subcategory α cat_Set α cat_Rel α 
    by 
      ( 
        rule subcat_trans[
          OF Set_Par.subcategory_axioms Par_Rel.subcategory_axioms
          ]
      )
  from assms show ?thesis
    unfolding cat_Rel_components(1)
    by (intro Set_Rel.subcat_is_arrD vsnd_arrow_is_cat_Set_arr_Vset) auto
qed

lemma (in 𝒵) vsnd_arrow_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
  assumes "A  cat_Rel αObj" 
    and "B  cat_Rel αObj"
    and "AB = A × B"
    and "B' = B"
    and "ℭ' = cat_Rel α"
  shows "vsnd_arrow A B : AB ℭ'B'"
  using assms(1-2) unfolding assms(3-5) by (rule vsnd_arrow_is_cat_Rel_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Rel_arr'


subsubsection‹Projection arrows are isomorphisms in the category Set›

lemma (in 𝒵) vfst_arrow_is_cat_Set_iso_arr_Vset:
  assumes "A  Vset α" and "b  Vset α"
  shows "vfst_arrow A (set {b}) : A × set {b} isocat_Set αA"
proof
  (
    intro 
      cat_Set_is_iso_arrI 
      arr_SetI 
      vfst_arrow_is_cat_Set_arr_Vset 
      assms,
    unfold cat_cs_simps
  )
  show "v11 (vfst_arrow A (set {b})ArrVal)"
  proof(rule vsv.vsv_valeq_v11I, unfold cat_cs_simps)
    fix ab ab' assume prems:
      "ab  A × set {b}"
      "ab'  A × set {b}"
      "vfst_arrow A (set {b})ArrValab = vfst_arrow A (set {b})ArrValab'"
    from prems obtain a where ab_def: "ab = a, b" and a: "a  A" 
      by clarsimp
    from prems obtain a' where ab'_def: "ab' = a', b" and a': "a'  A" 
      by clarsimp
    from prems(3) a a' have "a = a'"
      unfolding ab_def ab'_def
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
    then show "ab = ab'"  unfolding ab_def ab'_def by simp
  qed (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show " (vfst_arrow A (set {b})ArrVal) = A"
  proof(intro vsubset_antisym)
    show "A   (vfst_arrow A (set {b})ArrVal)"
    proof(intro vsubsetI)
      fix a assume a: "a  A"
      then have a_def: "a = vfst_arrow A (set {b})ArrVala, b"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
      from a assms show "a   (vfst_arrow A (set {b})ArrVal)"
        by (subst a_def, use nothing in intro vsv.vsv_vimageI2) 
          (auto simp: cat_cs_simps cat_cs_intros)
    qed
  qed (rule vfst_arrow_vrange)
qed (use assms in auto)

lemma (in 𝒵) vfst_arrow_is_cat_Set_iso_arr:
  assumes "A  cat_Set αObj" and "b  cat_Set αObj"
  shows "vfst_arrow A (set {b}) : A × set {b} isocat_Set αA"
  using assms 
  unfolding cat_Set_components 
  by (rule vfst_arrow_is_cat_Set_iso_arr_Vset)

lemma (in 𝒵) vfst_arrow_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
  assumes "A  cat_Set αObj" 
    and "b  cat_Set αObj"
    and "AB = A × set {b}"
    and "A' = A"
    and "ℭ' = cat_Set α"
  shows "vfst_arrow A (set {b}) : AB isoℭ'A"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vfst_arrow_is_cat_Set_iso_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.vfst_arrow_is_cat_Set_iso_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Set_iso_arr_Vset:
  assumes "a  Vset α" and "B  Vset α"
  shows "vsnd_arrow (set {a}) B : set {a} × B isocat_Set αB"
proof
  (
    intro 
      cat_Set_is_iso_arrI 
      arr_SetI 
      vsnd_arrow_is_cat_Set_arr_Vset 
      assms,
    unfold cat_cs_simps
  )
  show "v11 (vsnd_arrow (set {a}) BArrVal)"
  proof(rule vsv.vsv_valeq_v11I, unfold cat_cs_simps)
    fix ab ab' assume prems:
      "ab  set {a} × B"
      "ab'  set {a} × B"
      "vsnd_arrow (set {a}) BArrValab = vsnd_arrow (set {a}) BArrValab'"
    from prems obtain b where ab_def: "ab = a, b" and b: "b  B" 
      by clarsimp
    from prems obtain b' where ab'_def: "ab' = a, b'" and b': "b'  B" 
      by clarsimp
    from prems(3) b b' have "b = b'"
      unfolding ab_def ab'_def
      by (cs_prems cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
    then show "ab = ab'"  unfolding ab_def ab'_def by simp
  qed (cs_concl cs_shallow cs_intro: cat_cs_intros)
  show " (vsnd_arrow (set {a}) BArrVal) = B"
  proof(intro vsubset_antisym)
    show "B   (vsnd_arrow (set {a}) BArrVal)"
    proof(intro vsubsetI)
      fix b assume b: "b  B"
      then have b_def: "b = vsnd_arrow (set {a}) BArrVala, b"
        by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
      from b assms show "b   (vsnd_arrow (set {a}) BArrVal)"
        by (subst b_def, use nothing in intro vsv.vsv_vimageI2) 
          (auto simp: cat_cs_simps cat_cs_intros)
    qed
  qed (rule vsnd_arrow_vrange)
qed (use assms in auto)

lemma (in 𝒵) vsnd_arrow_is_cat_Set_iso_arr:
  assumes "a  cat_Set αObj" and "B  cat_Set αObj"
  shows "vsnd_arrow (set {a}) B : set {a} × B isocat_Set αB"
  using assms 
  unfolding cat_Set_components 
  by (rule vsnd_arrow_is_cat_Set_iso_arr_Vset)

lemma (in 𝒵) vsnd_arrow_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
  assumes "a  cat_Set αObj" 
    and "B  cat_Set αObj"
    and "AB = set {a} × B"
    and "A' = A"
    and "ℭ' = cat_Set α"
  shows "vsnd_arrow (set {a}) B : AB isoℭ'B"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vsnd_arrow_is_cat_Set_iso_arr)

lemmas [cat_rel_par_Set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Set_iso_arr'


subsubsection‹Projection arrows are isomorphisms in the category Par›

lemma (in 𝒵) vfst_arrow_is_cat_Par_iso_arr:
  assumes "A  cat_Par αObj" and "b  cat_Par αObj"
  shows "vfst_arrow A (set {b}) : A × set {b} isocat_Par αA"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  show "vfst_arrow A (set {b}) : A × set {b} isocat_Par αA"
    by 
      (
        rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
          [
            THEN iffD1, 
            OF vfst_arrow_is_cat_Set_iso_arr_Vset[
              OF assms[unfolded cat_Par_components]
              ]
          ]
      )
qed

lemma (in 𝒵) vfst_arrow_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
  assumes "A  cat_Par αObj" 
    and "b  cat_Par αObj"
    and "AB = A × set {b}"
    and "A' = A"
    and "ℭ' = cat_Par α"
  shows "vfst_arrow A (set {b}) : AB isoℭ'A"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vfst_arrow_is_cat_Par_iso_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.vfst_arrow_is_cat_Par_iso_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Par_iso_arr:
  assumes "a  cat_Par αObj" and "B  cat_Par αObj"
  shows "vsnd_arrow (set {a}) B : set {a} × B isocat_Par αB"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  show "vsnd_arrow (set {a}) B : set {a} × B isocat_Par αB"
    by 
      (
        rule Set_Par.wr_subcat_is_iso_arr_is_iso_arr
          [
            THEN iffD1, 
            OF vsnd_arrow_is_cat_Set_iso_arr_Vset[
              OF assms[unfolded cat_Par_components]
              ]
          ]
      )
qed

lemma (in 𝒵) vsnd_arrow_is_cat_Par_iso_arr'[cat_rel_Par_set_cs_intros]:
  assumes "a  cat_Par αObj" 
    and "B  cat_Par αObj"
    and "AB = set {a} × B"
    and "A' = A"
    and "ℭ' = cat_Par α"
  shows "vsnd_arrow (set {a}) B : AB isoℭ'B"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vsnd_arrow_is_cat_Par_iso_arr)

lemmas [cat_rel_Par_set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Par_iso_arr'


subsubsection‹Projection arrows are isomorphisms in the category Rel›

lemma (in 𝒵) vfst_arrow_is_cat_Rel_iso_arr:
  assumes "A  cat_Rel αObj" and "b  cat_Rel αObj"
  shows "vfst_arrow A (set {b}) : A × set {b} isocat_Rel αA"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  interpret Par_Rel: wide_replete_subcategory α cat_Par α cat_Rel α 
    by (rule wide_replete_subcategory_cat_Par_cat_Rel)
  interpret Set_Rel: wide_replete_subcategory α cat_Set α cat_Rel α 
    by 
      ( 
        rule wr_subcat_trans
          [
            OF 
              Set_Par.wide_replete_subcategory_axioms 
              Par_Rel.wide_replete_subcategory_axioms
          ]
      )
  show ?thesis
    by 
      (
        rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
          [
            THEN iffD1, 
            OF vfst_arrow_is_cat_Set_iso_arr_Vset[
              OF assms[unfolded cat_Rel_components]
              ]
          ]
      )
qed

lemma (in 𝒵) vfst_arrow_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
  assumes "A  cat_Rel αObj" 
    and "b  cat_Rel αObj"
    and "AB = A × set {b}"
    and "A' = A"
    and "ℭ' = cat_Rel α"
  shows "vfst_arrow A (set {b}) : AB isoℭ'A"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vfst_arrow_is_cat_Rel_iso_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.vfst_arrow_is_cat_Rel_iso_arr'

lemma (in 𝒵) vsnd_arrow_is_cat_Rel_iso_arr:
  assumes "a  cat_Rel αObj" and "B  cat_Rel αObj"
  shows "vsnd_arrow (set {a}) B : set {a} × B isocat_Rel αB"
proof-
  interpret Set_Par: wide_replete_subcategory α cat_Set α cat_Par α 
    by (rule wide_replete_subcategory_cat_Set_cat_Par)
  interpret Par_Rel: wide_replete_subcategory α cat_Par α cat_Rel α 
    by (rule wide_replete_subcategory_cat_Par_cat_Rel)
  interpret Set_Rel: wide_replete_subcategory α cat_Set α cat_Rel α 
    by 
      ( 
        rule wr_subcat_trans
          [
            OF 
              Set_Par.wide_replete_subcategory_axioms 
              Par_Rel.wide_replete_subcategory_axioms
          ]
      )
  show ?thesis
    by 
      (
        rule Set_Rel.wr_subcat_is_iso_arr_is_iso_arr
          [
            THEN iffD1, 
            OF vsnd_arrow_is_cat_Set_iso_arr_Vset[
              OF assms[unfolded cat_Rel_components]
              ]
          ]
      )
qed

lemma (in 𝒵) vsnd_arrow_is_cat_Rel_iso_arr'[cat_Rel_par_set_cs_intros]:
  assumes "a  cat_Rel αObj" 
    and "B  cat_Rel αObj"
    and "AB = set {a} × B"
    and "A' = A"
    and "ℭ' = cat_Rel α"
  shows "vsnd_arrow (set {a}) B : AB isoℭ'B"
  using assms(1-2) 
  unfolding assms(3-5)
  by (rule vsnd_arrow_is_cat_Rel_iso_arr)

lemmas [cat_Rel_par_set_cs_intros] = 𝒵.vsnd_arrow_is_cat_Rel_iso_arr'



subsection‹Projection arrow for vproduct›

definition vprojection_arrow :: "V  (V  V)  V  V"
  where "vprojection_arrow I A i = [vprojection I A i, (iI. A i), A i]"


text‹Components.›

lemma vprojection_arrow_components:
  shows "vprojection_arrow I A iArrVal = vprojection I A i"
    and "vprojection_arrow I A iArrDom = (iI. A i)"
    and "vprojection_arrow I A iArrCod = A i"
  unfolding vprojection_arrow_def arr_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Projection arrow value›

mk_VLambda vprojection_arrow_components(1)[unfolded vprojection_def]
  |vsv vprojection_arrow_ArrVal_vsv[cat_Set_cs_intros]|
  |vdomain vprojection_arrow_ArrVal_vdomain[cat_Set_cs_simps]|
  |app vprojection_arrow_ArrVal_app[cat_Set_cs_simps]|


subsubsection‹Projection arrow is an arrow in the category Set›

lemma (in 𝒵) arr_Set_vprojection_arrow:
  assumes "i  I" and "VLambda I A  Vset α"
  shows "arr_Set α (vprojection_arrow I A i)"
proof(intro arr_SetI)
  show "vfsequence (vprojection_arrow I A i)"
    unfolding vprojection_arrow_def by auto
  show "vcard (vprojection_arrow I A i) = 3"
    unfolding vprojection_arrow_def by (simp add: nat_omega_simps)
  show "vprojection_arrow I A iArrCod  Vset α"
    unfolding vprojection_arrow_components
  proof-
    from assms(1) have "i  I" by simp
    then have "A i   (VLambda I A)" by auto
    moreover from assms(2) have " (VLambda I A)  Vset α"
      by (meson vrange_in_VsetI)
    ultimately show "A i  Vset α" by auto   
  qed
qed 
  (
    auto 
      simp: vprojection_arrow_components 
      intro!: 
        assms 
        vprojection_vrange_vsubset 
        Limit_vproduct_in_Vset_if_VLambda_in_VsetI
  )

lemma (in 𝒵) vprojection_arrow_is_arr:
  assumes "i  I" and "VLambda I A  Vset α"
  shows "vprojection_arrow I A i : (iI. A i) cat_Set αA i"
proof(intro cat_Set_is_arrI)
  from assms show "arr_Set α (vprojection_arrow I A i)"
    by (rule arr_Set_vprojection_arrow)
qed (simp_all add: vprojection_arrow_components)



subsection‹Canonical injection arrow for vdunion›

definition vcinjection_arrow :: "V  (V  V)  V  V"
  where "vcinjection_arrow I A i = [vcinjection A i, A i, (iI. A i)]"


text‹Components.›

lemma vcinjection_arrow_components:
  shows "vcinjection_arrow I A iArrVal = vcinjection A i"
    and "vcinjection_arrow I A iArrDom = A i"
    and "vcinjection_arrow I A iArrCod = (iI. A i)"
  unfolding vcinjection_arrow_def arr_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Canonical injection arrow value›

mk_VLambda vcinjection_arrow_components(1)[unfolded vcinjection_def]
  |vsv vcinjection_arrow_ArrVal_vsv[cat_Set_cs_intros]|
  |vdomain vcinjection_arrow_ArrVal_vdomain[cat_Set_cs_simps]|
  |app vcinjection_arrow_ArrVal_app[cat_Set_cs_simps]|


subsubsection‹Canonical injection arrow is an arrow in the category Set›

lemma (in 𝒵) arr_Set_vcinjection_arrow:
  assumes "i  I" and "VLambda I A  Vset α"
  shows "arr_Set α (vcinjection_arrow I A i)"
proof(intro arr_SetI)
  show "vfsequence (vcinjection_arrow I A i)"
    unfolding vcinjection_arrow_def by auto
  show "vcard (vcinjection_arrow I A i) = 3"
    unfolding vcinjection_arrow_def by (simp add: nat_omega_simps)
  show "vcinjection_arrow I A iArrDom  Vset α"
    unfolding vcinjection_arrow_components
  proof-
    from assms(1) have Ai_def: "A i = VLambda I Ai" by simp
    with assms(1) have "A i   (VLambda I A)" by auto
    with assms(2) Limit_α show "A i  Vset α"
      unfolding Ai_def by (auto intro: vrange_in_VsetI)
  qed
  show "vcinjection_arrow I A iArrCod  Vset α"
    unfolding vcinjection_arrow_components
    by (intro Limit_vdunion_in_Vset_if_VLambda_in_VsetI Limit_α assms)
qed 
  (
    auto 
      simp: vcinjection_arrow_components 
      intro!: assms vcinjection_vrange_vsubset 
  )

lemma (in 𝒵) vcinjection_arrow_is_arr:
  assumes "i  I" and "VLambda I A  Vset α"
  shows "vcinjection_arrow I A i : A i cat_Set α(iI. A i)"
proof(intro cat_Set_is_arrI)
  from assms show "arr_Set α (vcinjection_arrow I A i)"
    by (rule arr_Set_vcinjection_arrow)
qed (simp_all add: vcinjection_arrow_components)

lemma (in 𝒵) vcinjection_arrow_is_arr'[cat_cs_intros]:
  assumes "i  I" 
    and "VLambda I A  Vset α"
    and "A' = A i"
    and "ℭ' = cat_Set α"
    and "P' = (iI. A i)"
  shows "vcinjection_arrow I A i : A' ℭ'P'"
  using assms(1,2) unfolding assms(3-5) by (rule vcinjection_arrow_is_arr)



subsection‹Product arrow value for Rel›


subsubsection‹Definition and elementary properties›

definition prod_2_Rel_ArrVal :: "V  V  V" 
  where "prod_2_Rel_ArrVal S T =
    set {a, b, c, d | a b c d. a, c  S  b, d  T}"

lemma small_prod_2_Rel_ArrVal[simp]:
  "small {a, b, c, d | a b c d. a, c  S  b, d  T}"
  (is small ?S)
proof(rule down)
  show "?S  elts ((𝒟 S × 𝒟 T) × ( S ×  T))" by auto
qed


text‹Rules.›

lemma prod_2_Rel_ArrValI:
  assumes "ab_cd = a, b, c, d"
    and "a, c  S"
    and "b, d  T"
  shows "ab_cd  prod_2_Rel_ArrVal S T"
  using assms unfolding prod_2_Rel_ArrVal_def by simp

lemma prod_2_Rel_ArrValD[dest]:
  assumes "a, b, c, d  prod_2_Rel_ArrVal S T"
  shows "a, c  S" and "b, d  T"
  using assms unfolding prod_2_Rel_ArrVal_def by auto

lemma prod_2_Rel_ArrValE[elim!]:
  assumes "ab_cd  prod_2_Rel_ArrVal S T"
  obtains a b c d where "ab_cd = a, b, c, d" 
    and "a, c  S"
    and "b, d  T"
  using assms unfolding prod_2_Rel_ArrVal_def by auto


text‹Elementary properties›

lemma prod_2_Rel_ArrVal_vsubset_vprod:
  "prod_2_Rel_ArrVal S T  ((𝒟 S × 𝒟 T) × ( S ×  T))"
  by (intro vsubsetI) auto

lemma prod_2_Rel_ArrVal_vbrelation: "vbrelation (prod_2_Rel_ArrVal S T)"
  using prod_2_Rel_ArrVal_vsubset_vprod by auto

lemma prod_2_Rel_ArrVal_vdomain: "𝒟 (prod_2_Rel_ArrVal S T) = 𝒟 S × 𝒟 T"
proof(intro vsubset_antisym)
  show "𝒟 S × 𝒟 T  𝒟 (prod_2_Rel_ArrVal S T)"
  proof(intro vsubsetI)
    fix ab assume "ab  𝒟 S × 𝒟 T"
    then obtain a b
      where ab_def: "