Theory CZH_ECAT_Set

(* Copyright 2021 (C) Mihails Milehins *)

section‹‹Set››
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



subsection‹‹Set› as a category›


subsubsection‹Definition and elementary properties›

definition cat_Set :: "V ⇒ V"
  where "cat_Set α =
    [
      Vset α,
      set {T. arr_Set α T},
      (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈),
      (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈),
      (λST∈∘composable_arrs (dg_Set α). ST⦇0⦈ ∘Rel ST⦇1ℕ⦈),
      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⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrDom⦈)"
    and "cat_Set α⦇Cod⦈ = (λT∈∘set {T. arr_Set α T}. T⦇ArrCod⦈)"
    and "cat_Set α⦇Comp⦈ =
      (λST∈∘composable_arrs (dg_Set α). ST⦇0⦈ ∘Par ST⦇1ℕ⦈)"
    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 α⦇CId⦈⦇A⦈ = 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 α⦇CId⦈⦇A⦈⦇ArrVal⦈⦇a⦈ = a"
  unfolding 
    cat_Set_CId_app[OF assms(1)[unfolded cat_Set_components(1)]] 
    id_Rel_ArrVal_app[OF assms(2)] 
  by simp


subsubsection‹‹Set› 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 α⦇CId⦈⦇A⦈ : 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 α⦇CId⦈⦇B⦈ ∘A⇘cat_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 ∘A⇘cat_Set α⇙ cat_Set α⦇CId⦈⦇B⦈ = 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'


subsubsection‹‹Set› 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 α⦇CId⦈⦇A⦈ = cat_Par α⦇CId⦈⦇A⦈"
        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 ↦iso⇘cat_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


subsubsection‹‹Set› 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 "ℛ∘ (F⦇ArrVal⦈) ⊆∘ F⦇ArrCod⦈"  
           by (auto simp: f.arr_Set_ArrVal_vrange)
        show "F⦇ArrDom⦈ ∈∘ Vset β"
          by (auto intro!: f.arr_Set_ArrDom_in_Vset Vset_in_mono assms(2))
        show "F⦇ArrCod⦈ ∈∘ 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 ∘A⇘cat_Set α⇙ F = G ∘A⇘cat_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 ∘A⇘cat_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 ∘A⇘cat_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 ∘A⇘cat_Set α⇙ F)" by (rule α_gf(1))
        then interpret arr_Set_α_gf: arr_Set β ‹(G ∘A⇘cat_Set α⇙ F)› by simp
        from α_gf_is_arr have dom_lhs: "𝒟∘ ((G ∘A⇘cat_Set α⇙ F)⦇ArrVal⦈) = A"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        show "arr_Set β (G ∘A⇘cat_Set β⇙ F)" by (rule β_gf(1))
        then interpret arr_Set_β_gf: arr_Set β ‹(G ∘A⇘cat_Set β⇙ F)› by simp
        from β_gf_is_arr have dom_rhs: "𝒟∘ ((G ∘A⇘cat_Set β⇙ F)⦇ArrVal⦈) = A"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)
        show "(G ∘A⇘cat_Set α⇙ F)⦇ArrVal⦈ = (G ∘A⇘cat_Set β⇙ F)⦇ArrVal⦈"
        proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
          fix a assume "a ∈∘ A"
          from that this show 
            "(G ∘A⇘cat_Set α⇙ F)⦇ArrVal⦈⦇a⦈ = (G ∘A⇘cat_Set β⇙ F)⦇ArrVal⦈⦇a⦈"
            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 ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈) ⊆∘ ℛ∘ (S⦇ArrVal⦈)" 
proof(intro vsubsetI)
  note SD = cat_Set_is_arrD[OF assms(1)]
  interpret S: arr_Set α S 
    rewrites "S⦇ArrDom⦈ = B" and "S⦇ArrCod⦈ = C"
    by (intro SD)+
  from assms(1,2) have "S ∘A⇘cat_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 ∘A⇘cat_Set α⇙ T›
    rewrites "(S ∘A⇘cat_Set α⇙ T)⦇ArrDom⦈ = A" 
      and "(S ∘A⇘cat_Set α⇙ T)⦇ArrCod⦈ = C"
    by (intro ST)+
  fix y assume prems: "y ∈∘ ℛ∘ ((S ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈)"
  with ST.arr_Set_ArrVal_vdomain obtain x 
    where x: "x ∈∘ A" and y_def: "y = (S ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈⦇x⦈"
    by force
  show "y ∈∘ ℛ∘ (S⦇ArrVal⦈)"
  proof(intro S.ArrVal.vsv_vimageI2', unfold cat_Set_cs_simps)
    from assms(1,2) x show "y = S⦇ArrVal⦈⦇T⦇ArrVal⦈⦇x⦈⦈"
      unfolding y_def 
      by (cs_concl cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
    from assms(2) x show "T⦇ArrVal⦈⦇x⦈ ∈∘ 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 (T⦇ArrVal⦈)"
    and "𝒟∘ (T⦇ArrVal⦈) = A"
    and "ℛ∘ (T⦇ArrVal⦈) = B"
  shows "T : A ↦iso⇘cat_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 ↦iso⇘cat_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 ↦iso⇘cat_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 ↦iso⇘cat_Set α⇙ B"
  shows "T : A ↦⇘cat_Set α⇙ B"
    and "v11 (T⦇ArrVal⦈)"
    and "𝒟∘ (T⦇ArrVal⦈) = A"
    and "ℛ∘ (T⦇ArrVal⦈) = 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 ↦iso⇘cat_Par α⇙ B"
    by (cs_concl cs_shallow cs_intro: cat_sub_cs_intros cat_sub_fw_cs_intros)
  show "v11 (T⦇ArrVal⦈)" "𝒟∘ (T⦇ArrVal⦈) = A" "ℛ∘ (T⦇ArrVal⦈) = 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 ↦iso⇘cat_Set α⇙ B ⟷ 
    T : A ↦⇘cat_Set α⇙ B ∧
    v11 (T⦇ArrVal⦈) ∧ 
    𝒟∘ (T⦇ArrVal⦈) = A ∧ 
    ℛ∘ (T⦇ArrVal⦈) = B"
  by auto

lemma (in 𝒵) cat_Set_is_iso_arr_if_monic_and_epic:
  assumes "F : A ↦mon⇘cat_Set α⇙ B" and "F : A ↦epi⇘cat_Set α⇙ B"
  shows "F : A ↦iso⇘cat_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 "F⦇ArrVal⦈⦇f⦈ : 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 "F⦇ArrVal⦈⦇f⦈ ∈∘ 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 ↦iso⇘cat_Set α⇙ B"
  shows "T¯C⇘cat_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 ↦iso⇘cat_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¯C⇘cat_Par α⇙ = T¯C⇘cat_Set α⇙"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_sub_bw_cs_simps cs_intro: cat_sub_cs_intros
      )
  from T show "T¯C⇘cat_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 ↦iso⇘cat_Set α⇙ B"
    and "a ∈∘ A"
    and [cat_cs_simps]: "T⦇ArrVal⦈⦇a⦈ = b"
  shows "(T¯C⇘cat_Set α⇙)⦇ArrVal⦈⦇b⦈ = 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 ‹T⦇ArrVal⦈› by (rule T(2))
  from T.v11_axioms assms(1,2) show "T¯C⇘cat_Set α⇙⦇ArrVal⦈⦇b⦈ = 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 ↦iso⇘cat_Set α⇙ Hom 𝔅 c d"
  shows "F¯C⇘cat_Set α⇙⦇ArrVal⦈⦇f⦈ : 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¯C⇘cat_Set α⇙⦇ArrVal⦈⦇f⦈ ∈∘ 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 ↦iso⇘cat_Set α⇙ B" and "b ∈∘ B"
  shows "F⦇ArrVal⦈⦇F¯C⇘cat_Set α⇙⦇ArrVal⦈⦇b⦈⦈ = 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 ∘A⇘cat_Set α⇙ F¯C⇘cat_Set α⇙ = cat_Set α⦇CId⦈⦇B⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms have [cat_cs_simps]: 
    "F⦇ArrVal⦈⦇F¯C⇘cat_Set α⇙⦇ArrVal⦈⦇b⦈⦈ = 
      (F ∘A⇘cat_Set α⇙ F¯C⇘cat_Set α⇙)⦇ArrVal⦈⦇b⦈"
    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 ↦iso⇘cat_Set α⇙ B" and "a ∈∘ A"
  shows "F¯C⇘cat_Set α⇙⦇ArrVal⦈⦇F⦇ArrVal⦈⦇a⦈⦈ = 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¯C⇘cat_Set α⇙ ∘A⇘cat_Set α⇙ F = cat_Set α⦇CId⦈⦇A⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  from assms have [cat_cs_simps]: 
    "F¯C⇘cat_Set α⇙⦇ArrVal⦈⦇F⦇ArrVal⦈⦇a⦈⦈ =
      (F¯C⇘cat_Set α⇙ ∘A⇘cat_Set α⇙ F)⦇ArrVal⦈⦇a⦈"
    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 B⦇ArrVal⦈ = f"
    and [cat_Set_cs_simps]: "cat_Set_arr_of_vsv f B⦇ArrDom⦈ = 𝒟∘ f"
    and [cat_cs_simps, cat_Set_cs_simps]: "cat_Set_arr_of_vsv f B⦇ArrCod⦈ = 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 = [T⦇ArrVal⦈ ↾l∘ C, C, T⦇ArrCod⦈]∘"


text‹Components.›

lemma vlrestriction_Set_components:
  shows [cat_Set_cs_simps]: "(T ↾lSet C)⦇ArrVal⦈ = T⦇ArrVal⦈ ↾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⦈ = T⦇ArrCod⦈"
  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 "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = 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)⦇ArrVal⦈⦇x⦈ = T⦇ArrVal⦈⦇x⦈"
proof-
  interpret T: arr_Set α T
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = 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 "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = 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 "𝒟∘ (T⦇ArrVal⦈ ↾l∘ C) = C"
      by (cs_concl cs_simp: V_cs_simps cat_cs_simps cs_intro: cat_cs_intros)
    show "ℛ∘ (T⦇ArrVal⦈ ↾l∘ C) ⊆∘ B"
      unfolding app_vimage_def[symmetric]
    proof(intro vsubsetI)
      fix x assume prems: "x ∈∘ T⦇ArrVal⦈ `∘ C"
      then obtain c where "c ∈∘ C" and x_def: "x = T⦇ArrVal⦈⦇c⦈" 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 ↦mon⇘cat_Set α⇙ B" and "C ⊆∘ A"
  shows "T ↾lSet C : C ↦mon⇘cat_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 ‹T⦇ArrVal⦈› 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 "𝒟∘ (T⦇ArrVal⦈ ↾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 = [T⦇ArrVal⦈ ↾r∘ C, T⦇ArrDom⦈, C]∘"


text‹Components.›

lemma vrrestriction_Set_components:
  shows [cat_Set_cs_simps]: "(T ↾rSet C)⦇ArrVal⦈ = T⦇ArrVal⦈ ↾r∘ C"
    and [cat_cs_simps, cat_Set_cs_simps]: "(T ↾rSet C)⦇ArrDom⦈ = T⦇ArrDom⦈"
    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 "ℛ∘ (T⦇ArrVal⦈) ⊆∘ C" 
  shows "(T ↾rSet C)⦇ArrVal⦈ = T⦇ArrVal⦈"
proof-
  interpret T: arr_Set α T
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = 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 "ℛ∘ (T⦇ArrVal⦈) ⊆∘ 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 "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = 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 "ℛ∘ (T⦇ArrVal⦈) ⊆∘ 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 ℛ∘ (T⦇ArrVal⦈) : A ↦⇘cat_Set α⇙ ℛ∘ (T⦇ArrVal⦈)"
    and vrrestriction_Set_vrange_ArrVal_app[cat_cs_simps, cat_Set_cs_simps]: 
      "(T ↾rSet ℛ∘ (T⦇ArrVal⦈))⦇ArrVal⦈ = T⦇ArrVal⦈"
proof(intro vrrestriction_Set_is_arr, rule assms)
  note TD = cat_Set_is_arrD[OF assms(1)]
  interpret T: arr_Set α T
    rewrites "T⦇ArrDom⦈ = A" and "T⦇ArrCod⦈ = B"
    by (intro TD)+
  show "ℛ∘ (T⦇ArrVal⦈) ∈∘ 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 ↦mon⇘cat_Set α⇙ B" 
  shows "T ↾rSet ℛ∘ (T⦇ArrVal⦈) : A ↦iso⇘cat_Set α⇙ ℛ∘ (T⦇ArrVal⦈)"
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 "ℛ∘ (S⦇ArrVal⦈) ⊆∘ D"
    and "D ∈∘ cat_Set α⦇Obj⦈"
  shows "S ↾rSet D ∘A⇘cat_Set α⇙ T = (S ∘A⇘cat_Set α⇙ T) ↾rSet D"
proof-

  note SD = cat_Set_is_arrD[OF assms(1)]
  interpret S: arr_Set α S 
    rewrites [cat_cs_simps]: "S⦇ArrDom⦈ = B" and [cat_cs_simps]: "S⦇ArrCod⦈ = C"
    by (intro SD)+
  note TD = cat_Set_is_arrD[OF assms(2)]
  interpret T: arr_Set α T 
    rewrites [cat_cs_simps]: "T⦇ArrDom⦈ = A" and [cat_cs_simps]: "T⦇ArrCod⦈ = B"
    by (intro TD)+

  from assms(3) S.arr_Par_ArrVal_vrange have RS_D: "ℛ∘ (S⦇ArrVal⦈) ⊆∘ D" by auto

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

  from assms(1,2) have "ℛ∘ ((S ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈) ⊆∘ ℛ∘ (S⦇ArrVal⦈)" 
    by (intro cat_Set_Comp_ArrVal_vrange)
  with assms(3) have RST: "ℛ∘ ((S ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈) ⊆∘ D" by auto

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

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

  show "S ↾rSet D ∘A⇘cat_Set α⇙ T = (S ∘A⇘cat_Set α⇙ T) ↾rSet D"
  proof(rule arr_Set_eqI[of α])
    show 
      "(S ↾rSet D ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈ =
        ((S ∘A⇘cat_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 ∘A⇘cat_Set α⇙ T)⦇ArrVal⦈⦇a⦈ = 
          ((S ∘A⇘cat_Set α⇙ T) ↾rSet D)⦇ArrVal⦈⦇a⦈"
        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 α⦇CId⦈⦇A⦈ ↾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 α⦇CId⦈⦇A⦈ : 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 α⦇CId⦈⦇A⦈⦇ArrVal⦈) ⊆∘ B"
    by (auto intro: arr_Set.arr_Set_ArrVal_vrange)

  with assms A assms(1,2) have lhs_is_arr:
    "cat_Set α⦇CId⦈⦇A⦈ ↾rSet B : A ↦⇘cat_Set α⇙ B"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟∘ ((cat_Set α⦇CId⦈⦇A⦈ ↾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 α⦇CId⦈⦇A⦈ ↾rSet B)⦇ArrVal⦈ = incl_Rel A B⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈∘ A"
      with A RA_B show 
        "(cat_Set α⦇CId⦈⦇A⦈ ↾rSet B)⦇ArrVal⦈⦇a⦈ = incl_Rel A B⦇ArrVal⦈⦇a⦈"
        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 "ℛ∘ (F⦇ArrVal⦈) ⊆∘ C"
  shows "incl_Rel C B ∘A⇘cat_Set α⇙ F ↾rSet C = F"
proof-
  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret F: arr_Set α F 
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = 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 ∘A⇘cat_Set α⇙ F ↾rSet C : A ↦⇘cat_Set α⇙ B"
    by (cs_concl cs_intro: cat_cs_intros)
  then have dom_lhs: "𝒟∘ ((incl_Rel C B ∘A⇘cat_Set α⇙ F ↾rSet C)⦇ArrVal⦈) = A"
    by (cs_concl cs_simp: cat_cs_simps)
  from assms(1) have dom_rhs: "𝒟∘ (F⦇ArrVal⦈) = A" 
    by (cs_concl cs_simp: cat_cs_simps)
  show ?thesis
  proof(rule arr_Set_eqI[of α])
    show "(incl_Rel C B ∘A⇘cat_Set α⇙ F ↾rSet C)⦇ArrVal⦈ = F⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume prems: "a ∈∘ A"
      with assms F.ArrVal.vsv_vimageI2 have "F⦇ArrVal⦈⦇a⦈ ∈∘ C"
        by (auto simp: F.arr_Set_ArrVal_vdomain)
      with prems assms C show 
        "(incl_Rel C B ∘A⇘cat_Set α⇙ F ↾rSet C)⦇ArrVal⦈⦇a⦈ = F⦇ArrVal⦈⦇a⦈"
        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 = [(λab∈∘A ×∘ B. vfst ab), A ×∘ B, A]∘"

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


text‹Components.›

lemma vfst_arrow_components: 
  shows "vfst_arrow A B⦇ArrVal⦈ = (λab∈∘A ×∘ B. vfst ab)"
    and [cat_cs_simps]: "vfst_arrow A B⦇ArrDom⦈ = A ×∘ B"
    and [cat_cs_simps]: "vfst_arrow A B⦇ArrCod⦈ = A"
  unfolding vfst_arrow_def arr_field_simps by (simp_all add: nat_omega_simps)

lemma vsnd_arrow_components: 
  shows "vsnd_arrow A B⦇ArrVal⦈ = (λab∈∘A ×∘ B. vsnd ab)"
    and [cat_cs_simps]: "vsnd_arrow A B⦇ArrDom⦈ = A ×∘ B"
    and [cat_cs_simps]: "vsnd_arrow A B⦇ArrCod⦈ = 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 B⦇ArrVal⦈⦇ab⦈ = a"
  using assms(2) unfolding assms(1) by (simp add: vfst_arrow_ArrVal_app')

lemma vfst_arrow_vrange: "ℛ∘ (vfst_arrow A B⦇ArrVal⦈) ⊆∘ 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 B⦇ArrVal⦈⦇ab⦈ = b"
  using assms(2) unfolding assms(1) by (simp add: vsnd_arrow_ArrVal_app')

lemma vsnd_arrow_vrange: "ℛ∘ (vsnd_arrow A B⦇ArrVal⦈) ⊆∘ 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 B⦇ArrVal⦈) ⊆∘ 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 B⦇ArrVal⦈) ⊆∘ 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} ↦iso⇘cat_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})⦇ArrVal⦈⦇ab⦈ = vfst_arrow A (set {b})⦇ArrVal⦈⦇ab'⦈"
    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})⦇ArrVal⦈⦇⟨a, 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} ↦iso⇘cat_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 ↦iso⇘cat_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}) B⦇ArrVal⦈)"
  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}) B⦇ArrVal⦈⦇ab⦈ = vsnd_arrow (set {a}) B⦇ArrVal⦈⦇ab'⦈"
    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}) B⦇ArrVal⦈) = B"
  proof(intro vsubset_antisym)
    show "B ⊆∘ ℛ∘ (vsnd_arrow (set {a}) B⦇ArrVal⦈)"
    proof(intro vsubsetI)
      fix b assume b: "b ∈∘ B"
      then have b_def: "b = vsnd_arrow (set {a}) B⦇ArrVal⦈⦇⟨a, 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}) B⦇ArrVal⦈)"
        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 ↦iso⇘cat_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} ↦iso⇘cat_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} ↦iso⇘cat_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 ↦iso⇘cat_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 ↦iso⇘cat_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} ↦iso⇘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: 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 ↦iso⇘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: 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, (∏∘i∈∘I. A i), A i]∘"


text‹Components.›

lemma vprojection_arrow_components:
  shows "vprojection_arrow I A i⦇ArrVal⦈ = vprojection I A i"
    and "vprojection_arrow I A i⦇ArrDom⦈ = (∏∘i∈∘I. A i)"
    and "vprojection_arrow I A i⦇ArrCod⦈ = 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 i⦇ArrCod⦈ ∈∘ 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 : (∏∘i∈∘I. 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, (∐∘i∈∘I. A i)]∘"


text‹Components.›

lemma vcinjection_arrow_components:
  shows "vcinjection_arrow I A i⦇ArrVal⦈ = vcinjection A i"
    and "vcinjection_arrow I A i⦇ArrDom⦈ = A i"
    and "vcinjection_arrow I A i⦇ArrCod⦈ = (∐∘i∈∘I. 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 i⦇ArrDom⦈ ∈∘ Vset α"
    unfolding vcinjection_arrow_components
  proof-
    from assms(1) have Ai_def: "A i = VLambda I A⦇i⦈" 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 i⦇ArrCod⦈ ∈∘ 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 α⇙ (∐∘i∈∘I. 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' = (∐∘i∈∘I. 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: "ab = ⟨a, b⟩" 
        and "a ∈∘ 𝒟∘ S"
        and "b ∈∘ 𝒟∘ T"
      by auto
    then obtain c d where "⟨a, c⟩ ∈∘ S" and "⟨b, d⟩ ∈∘ T" by force
    then have "⟨⟨a, b⟩, ⟨c, d⟩⟩ ∈∘ prod_2_Rel_ArrVal S T"
      by (intro prod_2_Rel_ArrValI) auto
    then show "ab ∈∘ 𝒟∘ (prod_2_Rel_ArrVal S T)"
      unfolding ab_def by (simp add: app_vdomainI)
  qed
qed (use prod_2_Rel_ArrVal_vsubset_vprod in blast)

lemma prod_2_Rel_ArrVal_vrange: "ℛ∘ (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 cd assume "cd ∈∘ ℛ∘ S ×∘ ℛ∘ T"
    then obtain c d
      where cd_def: "cd = ⟨c, d⟩" 
        and "c ∈∘ ℛ∘ S"
        and "d ∈∘ ℛ∘ T"
      by auto
    then obtain a b where "⟨a, c⟩ ∈∘ S" and "⟨b, d⟩ ∈∘ T" by force
    then have "⟨⟨a, b⟩, ⟨c, d⟩⟩ ∈∘ prod_2_Rel_ArrVal S T"
      by (intro prod_2_Rel_ArrValI) auto
    then show "cd ∈∘ ℛ∘ (prod_2_Rel_ArrVal S T)"
      unfolding cd_def by (simp add: app_vrangeI)
  qed
qed (use prod_2_Rel_ArrVal_vsubset_vprod in blast)


subsubsection‹Further properties›

lemma 
  assumes "vsv g" and "vsv f"
  shows prod_2_Rel_ArrVal_vsv: "vsv (prod_2_Rel_ArrVal g f)"
    and prod_2_Rel_ArrVal_app: 
      "⋀a b. ⟦ a ∈∘ 𝒟∘ g; b ∈∘ 𝒟∘ f ⟧ ⟹ 
        prod_2_Rel_ArrVal g f⦇⟨a,b⟩⦈ = ⟨g⦇a⦈, f⦇b⦈⟩"
proof-
  interpret g: vsv g by (rule assms(1))
  interpret f: vsv f by (rule assms(2))
  show vsv_gf: "vsv (prod_2_Rel_ArrVal g f)"
    by (intro vsvI; (elim prod_2_Rel_ArrValE)?; (unfold prod_2_Rel_ArrVal_def)?)
      (auto simp: g.vsv f.vsv)
  fix a b assume "a ∈∘ 𝒟∘ g" "b ∈∘ 𝒟∘ f"
  then have a_ga: "⟨a, g⦇a⦈⟩ ∈∘ g" and b_fb: "⟨b, f⦇b⦈⟩ ∈∘ f" by auto
  from a_ga b_fb show "prod_2_Rel_ArrVal g f⦇⟨a, b⟩⦈ = ⟨g⦇a⦈, f⦇b⦈⟩"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: vsv.vsv_appI[OF vsv_gf] cs_intro: prod_2_Rel_ArrValI
      )
qed

lemma prod_2_Rel_ArrVal_v11:
  assumes "v11 g" and "v11 f"
  shows "v11 (prod_2_Rel_ArrVal g f)"
proof-
  interpret g: v11 g by (rule assms(1))
  interpret f: v11 f by (rule assms(2))
  show ?thesis
  proof
    (
      intro vsv.vsv_valeq_v11I prod_2_Rel_ArrVal_vsv g.vsv_axioms f.vsv_axioms, 
      unfold prod_2_Rel_ArrVal_vdomain
    )
    fix ab cd
    assume prems:
      "ab ∈∘ 𝒟∘ g ×∘ 𝒟∘ f"  
      "cd ∈∘ 𝒟∘ g ×∘ 𝒟∘ f"
      "prod_2_Rel_ArrVal g f⦇ab⦈ = prod_2_Rel_ArrVal g f⦇cd⦈"
    from prems(1) obtain a b
      where ab_def: "ab = ⟨a, b⟩" and a: "a ∈∘ 𝒟∘ g" and b: "b ∈∘ 𝒟∘ f"
      by auto
    from prems(2) obtain c d
      where cd_def: "cd = ⟨c, d⟩" and c: "c ∈∘ 𝒟∘ g" and d: "d ∈∘ 𝒟∘ f"
      by auto
    from prems(3) a b c d have "⟨g⦇a⦈, f⦇b⦈⟩ = ⟨g⦇c⦈, f⦇d⦈⟩"
      unfolding ab_def cd_def
      by 
        (
          cs_prems cs_shallow 
            cs_simp: prod_2_Rel_ArrVal_app cs_intro: V_cs_intros
        )
    then have "g⦇a⦈ = g⦇c⦈" and "f⦇b⦈ = f⦇d⦈" by simp_all
    then show "ab = cd"
      by (auto simp: ab_def cd_def a b c d f.v11_injective g.v11_injective)
  qed
qed

lemma prod_2_Rel_ArrVal_vcomp:
  "prod_2_Rel_ArrVal S' T' ∘∘ prod_2_Rel_ArrVal S T =
    prod_2_Rel_ArrVal (S' ∘∘ S) (T' ∘∘ T)"
proof-
  interpret ST': vbrelation ‹prod_2_Rel_ArrVal S' T'›
    by (rule prod_2_Rel_ArrVal_vbrelation)
  interpret ST: vbrelation ‹prod_2_Rel_ArrVal S T›
    by (rule prod_2_Rel_ArrVal_vbrelation)
  show ?thesis (*TODO: simplify proof*)
  proof(intro vsubset_antisym vsubsetI)
    fix aa'_cc' assume 
      "aa'_cc' ∈∘ prod_2_Rel_ArrVal S' T' ∘∘ prod_2_Rel_ArrVal S T"
    then obtain aa' bb' cc' where ac_def: "aa'_cc' = ⟨aa', cc'⟩" 
      and bc: "⟨bb', cc'⟩ ∈∘ prod_2_Rel_ArrVal S' T'"
      and ab: "⟨aa', bb'⟩ ∈∘ prod_2_Rel_ArrVal S T"
      by (elim vcompE)
    from bc obtain b b' c c' 
      where bb'_cc'_def: "⟨bb', cc'⟩ = ⟨⟨b, b'⟩, ⟨c, c'⟩⟩"
        and bc: "⟨b, c⟩ ∈∘ S'"
        and bc': "⟨b', c'⟩ ∈∘ T'"
      by auto
    with ab obtain a a' 
      where aa'_bb'_def: "⟨aa', bb'⟩ = ⟨⟨a, a'⟩, ⟨b, b'⟩⟩"
        and ab: "⟨a, b⟩ ∈∘ S"
        and ab': "⟨a', b'⟩ ∈∘ T"
      by auto
    from bb'_cc'_def have bb'_def: "bb' = ⟨b, b'⟩" and cc'_def: "cc' = ⟨c, c'⟩"
      by simp_all
    from aa'_bb'_def have aa'_def: "aa' = ⟨a, a'⟩" and bb'_def: "bb' = ⟨b, b'⟩"
      by simp_all
    from bc bc' ab ab' show "aa'_cc' ∈∘ prod_2_Rel_ArrVal (S' ∘∘ S) (T' ∘∘ T)"
      unfolding ac_def aa'_def cc'_def
      by (intro prod_2_Rel_ArrValI)
        (cs_concl cs_shallow cs_intro: prod_2_Rel_ArrValI vcompI)+
  next
    fix aa'_cc' assume "aa'_cc' ∈∘ prod_2_Rel_ArrVal (S' ∘∘ S) (T' ∘∘ T)"
    then obtain a a' c c'
      where aa'_cc'_def: "aa'_cc' = ⟨⟨a, a'⟩, ⟨c, c'⟩⟩"
        and ac: "⟨a, c⟩ ∈∘ S' ∘∘ S"
        and ac': "⟨a', c'⟩ ∈∘ T' ∘∘ T"
      by blast
    from ac obtain b where ab: "⟨a, b⟩ ∈∘ S" and bc: "⟨b, c⟩ ∈∘ S'" 
      by auto
    from ac' obtain b' where ab': "⟨a', b'⟩ ∈∘ T" and bc': "⟨b', c'⟩ ∈∘ T'" 
      by auto
    from ab bc ab' bc' show 
      "aa'_cc' ∈∘ prod_2_Rel_ArrVal S' T' ∘∘ prod_2_Rel_ArrVal S T"
      unfolding aa'_cc'_def 
      by (cs_concl cs_shallow cs_intro: vcompI prod_2_Rel_ArrValI)
  qed
qed

lemma prod_2_Rel_ArrVal_vid_on[cat_cs_simps]:
  "prod_2_Rel_ArrVal (vid_on A) (vid_on B) = vid_on (A ×∘ B)"
  unfolding prod_2_Rel_ArrVal_def by auto



subsection‹Product arrow for ‹Rel››


subsubsection‹Definition and elementary properties›

definition prod_2_Rel :: "V ⇒ V ⇒ V" (infixr ‹A×Rel› 80)
  where "prod_2_Rel S T =
    [
      prod_2_Rel_ArrVal (S⦇ArrVal⦈) (T⦇ArrVal⦈),
      S⦇ArrDom⦈ ×∘ T⦇ArrDom⦈,
      S⦇ArrCod⦈ ×∘ T⦇ArrCod⦈
    ]∘"

abbreviation (input) prod_2_Par :: "V ⇒ V ⇒ V" (infixr ‹A×Par› 80)
  where "prod_2_Par ≡ prod_2_Rel"
abbreviation (input) prod_2_Set :: "V ⇒ V ⇒ V" (infixr ‹A×Set› 80)
  where "prod_2_Set ≡ prod_2_Rel"


text‹Components.›

lemma prod_2_Rel_components: 
  shows "(S A×Rel T)⦇ArrVal⦈ = prod_2_Rel_ArrVal (S⦇ArrVal⦈) (T⦇ArrVal⦈)"
    and [cat_cs_simps]: "(S A×Rel T)⦇ArrDom⦈ = S⦇ArrDom⦈ ×∘ T⦇ArrDom⦈"
    and [cat_cs_simps]: "(S A×Rel T)⦇ArrCod⦈ = S⦇ArrCod⦈ ×∘ T⦇ArrCod⦈"
  unfolding prod_2_Rel_def arr_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Product arrow for ‹Rel› is an arrow in ‹Rel››

lemma prod_2_Rel_is_cat_Rel_arr:
  assumes "S : A ↦⇘cat_Rel α⇙ B" and "T : C ↦⇘cat_Rel α⇙ D"    
  shows "S A×Rel T : A ×∘ C ↦⇘cat_Rel α⇙ B ×∘ D"
proof-
  note S = cat_Rel_is_arrD[OF assms(1)]
  note T = cat_Rel_is_arrD[OF assms(2)]
  interpret S: arr_Rel α S 
    rewrites [simp]: "S⦇ArrDom⦈ = A" and [simp]: "S⦇ArrCod⦈ = B"
    by (simp_all add: S)
  interpret T: arr_Rel α T 
    rewrites [simp]: "T⦇ArrDom⦈ = C" and [simp]: "T⦇ArrCod⦈ = D"
    by (simp_all add: T)
  show ?thesis
  proof(intro cat_Rel_is_arrI arr_RelI)
    show "vfsequence (S A×Rel T)"
      unfolding prod_2_Rel_def by simp
    show "vcard (S A×Rel T) = 3ℕ"
      unfolding prod_2_Rel_def by (simp add: nat_omega_simps)
    from S have "𝒟∘ (S⦇ArrVal⦈) ⊆∘ A" and "ℛ∘ (S⦇ArrVal⦈) ⊆∘ B" by auto
    moreover from T have "𝒟∘ (T⦇ArrVal⦈) ⊆∘ C" and "ℛ∘ (T⦇ArrVal⦈) ⊆∘ D" 
      by auto
    ultimately have 
      "𝒟∘ (S⦇ArrVal⦈) ×∘ 𝒟∘ (T⦇ArrVal⦈) ⊆∘ A ×∘ C"
      "ℛ∘ (S⦇ArrVal⦈) ×∘ ℛ∘ (T⦇ArrVal⦈) ⊆∘ B ×∘ D"
      by auto
    then show 
      "𝒟∘ ((S A×Rel T)⦇ArrVal⦈) ⊆∘ (S A×Rel T)⦇ArrDom⦈"
      "ℛ∘ ((S A×Rel T)⦇ArrVal⦈) ⊆∘ (S A×Rel T)⦇ArrCod⦈"
      unfolding 
        prod_2_Rel_components prod_2_Rel_ArrVal_vdomain prod_2_Rel_ArrVal_vrange
      by (force simp: prod_2_Rel_components)+
    from 
      S.arr_Rel_ArrDom_in_Vset T.arr_Rel_ArrDom_in_Vset
      S.arr_Rel_ArrCod_in_Vset T.arr_Rel_ArrCod_in_Vset
    show "(S A×Rel T)⦇ArrDom⦈ ∈∘ Vset α" "(S A×Rel T)⦇ArrCod⦈ ∈∘ Vset α"
      unfolding prod_2_Rel_components 
      by (all‹intro Limit_vtimes_in_VsetI›) auto
  qed (auto simp: prod_2_Rel_components intro: prod_2_Rel_ArrVal_vbrelation)
qed

lemma prod_2_Rel_is_cat_Rel_arr'[cat_Rel_par_set_cs_intros]:
  assumes "S : A ↦⇘cat_Rel α⇙ B"
    and "T : C ↦⇘cat_Rel α⇙ D"
    and "A' = A ×∘ C"
    and "B' = B ×∘ D"
    and "ℭ' = cat_Rel α"
  shows "S A×Rel T : A' ↦⇘ℭ'⇙ B'"
  using assms(1,2) unfolding assms(3-5) by (rule prod_2_Rel_is_cat_Rel_arr)


subsubsection‹Product arrow for ‹Rel› is an arrow in ‹Set››

lemma prod_2_Rel_app[cat_rel_par_Set_cs_simps]:
  assumes "S : A ↦⇘cat_Set α⇙ B" 
    and "T : C ↦⇘cat_Set α⇙ D"    
    and "a ∈∘ A"
    and "c ∈∘ C"
    and "ac = ⟨a, c⟩"
  shows "(S A×Set T)⦇ArrVal⦈⦇ac⦈ = ⟨S⦇ArrVal⦈⦇a⦈, T⦇ArrVal⦈⦇c⦈⟩"
proof-
  note S = cat_Set_is_arrD[OF assms(1)]
  note T = cat_Set_is_arrD[OF assms(2)]
  interpret S: arr_Set α S 
    rewrites [simp]: "S⦇ArrDom⦈ = A" and [simp]: "S⦇ArrCod⦈ = B"
    by (simp_all add: S)
  interpret T: arr_Set α T 
    rewrites [simp]: "T⦇ArrDom⦈ = C" and [simp]: "T⦇ArrCod⦈ = D"
    by (simp_all add: T)
  from assms(3,4) show ?thesis
    unfolding prod_2_Rel_components(1) assms(5)
    by 
      (
        cs_concl cs_shallow
          cs_simp: 
            S.arr_Set_ArrVal_vdomain 
            T.arr_Set_ArrVal_vdomain 
            prod_2_Rel_ArrVal_app 
          cs_intro: V_cs_intros
      )
qed

lemma prod_2_Rel_is_cat_Set_arr:
  assumes "S : A ↦⇘cat_Set α⇙ B" and "T : C ↦⇘cat_Set α⇙ D"    
  shows "S A×Set T : A ×∘ C ↦⇘cat_Set α⇙ B ×∘ D"
proof-

  note S = cat_Set_is_arrD[OF assms(1)]
  note T = cat_Set_is_arrD[OF assms(2)]

  interpret S: arr_Set α S 
    rewrites [simp]: "S⦇ArrDom⦈ = A" and [simp]: "S⦇ArrCod⦈ = B"
    by (simp_all add: S)
  interpret T: arr_Set α T 
    rewrites [simp]: "T⦇ArrDom⦈ = C" and [simp]: "T⦇ArrCod⦈ = D"
    by (simp_all add: T)

  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI)
    show "vfsequence (S A×Set T)"
      unfolding prod_2_Rel_def by simp
    show "vcard (S A×Set T) = 3ℕ"
      unfolding prod_2_Rel_def by (simp add: nat_omega_simps)
    from S.arr_Set_ArrVal_vrange T.arr_Set_ArrVal_vrange show 
      "ℛ∘ ((S A×Set T)⦇ArrVal⦈) ⊆∘ (S A×Set T)⦇ArrCod⦈"
      unfolding 
        prod_2_Rel_components prod_2_Rel_ArrVal_vdomain prod_2_Rel_ArrVal_vrange
      by auto
    from assms S.arr_Par_ArrDom_in_Vset T.arr_Par_ArrDom_in_Vset show 
      "(S A×Set T)⦇ArrDom⦈ ∈∘ Vset α"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
    from assms S.arr_Par_ArrCod_in_Vset T.arr_Par_ArrCod_in_Vset show 
      "(S A×Set T)⦇ArrCod⦈ ∈∘ Vset α"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: V_cs_intros)
    from assms show "(S A×Set T)⦇ArrDom⦈ = A ×∘ C"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    from assms show "(S A×Set T)⦇ArrCod⦈ = B ×∘ D"
      by (cs_concl cs_shallow cs_simp: cat_cs_simps)
    show "vsv ((S A×Set T)⦇ArrVal⦈)"
      unfolding prod_2_Rel_components
      by (intro prod_2_Rel_ArrVal_vsv S.ArrVal.vsv_axioms T.ArrVal.vsv_axioms)
  qed 
    (
      auto simp: 
        cat_cs_simps cat_Set_cs_simps 
        prod_2_Rel_ArrVal_vdomain prod_2_Rel_components(1)
    )

qed

lemma prod_2_Rel_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
  assumes "S : A ↦⇘cat_Set α⇙ B" 
    and "T : C ↦⇘cat_Set α⇙ D"
    and "AC = A ×∘ C"
    and "BD = B ×∘ D"
    and "ℭ' = cat_Set α"
  shows "S A×Set T : AC ↦⇘ℭ'⇙ BD"
  using assms(1,2) unfolding assms(3-5) by (rule prod_2_Rel_is_cat_Set_arr)


subsubsection‹Product arrow for ‹Rel› is an isomorphism in ‹Set››

lemma prod_2_Rel_is_cat_Set_iso_arr:
  assumes "S : A ↦iso⇘cat_Set α⇙ B" and "T : C ↦iso⇘cat_Set α⇙ D"    
  shows "S A×Set T : A ×∘ C ↦iso⇘cat_Set α⇙ B ×∘ D"
proof-
  note S = cat_Set_is_iso_arrD[OF assms(1)]
  note T = cat_Set_is_iso_arrD[OF assms(2)]
  show ?thesis
  proof
    (
      intro cat_Set_is_iso_arrI prod_2_Rel_is_cat_Set_arr[OF S(1) T(1)], 
      unfold prod_2_Rel_components
    )
    show "𝒟∘ (prod_2_Rel_ArrVal (S⦇ArrVal⦈) (T⦇ArrVal⦈)) = A ×∘ C"
      unfolding prod_2_Rel_ArrVal_vdomain
      by (cs_concl cs_shallow cs_simp: S(3) T(3) cs_intro: cat_cs_intros)
    show "ℛ∘ (prod_2_Rel_ArrVal (S⦇ArrVal⦈) (T⦇ArrVal⦈)) = B ×∘ D"
      unfolding prod_2_Rel_ArrVal_vrange
      by (cs_concl cs_shallow cs_simp: S(4) T(4) cs_intro: cat_cs_intros)
  qed (use S(2) T(2) in ‹cs_concl cs_shallow cs_intro: prod_2_Rel_ArrVal_v11›)
qed

lemma prod_2_Rel_is_cat_Set_iso_arr'[cat_rel_par_Set_cs_intros]:
  assumes "S : A ↦iso⇘cat_Set α⇙ B" 
    and "T : C ↦iso⇘cat_Set α⇙ D"    
    and "AC = A ×∘ C"
    and "BD = B ×∘ D"
    and "ℭ' = cat_Set α"
  shows "S A×Set T : AC ↦iso⇘ℭ'⇙ BD"
  using assms(1,2) 
  unfolding assms(3-5) 
  by (rule prod_2_Rel_is_cat_Set_iso_arr)


subsubsection‹Further elementary properties›

lemma prod_2_Rel_Comp:
  assumes "G' : B' ↦⇘cat_Rel α⇙ B''" 
    and "F' : A' ↦⇘cat_Rel α⇙ A''" 
    and "G : B ↦⇘cat_Rel α⇙ B'"
    and "F : A ↦⇘cat_Rel α⇙ A'"
  shows
    "G' A×Rel F' ∘A⇘cat_Rel α⇙ G A×Rel F =
      (G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F)"
proof-

  from cat_Rel_is_arrD(1)[OF assms(1)] interpret 𝒵 α by auto

  interpret Rel: category α ‹cat_Rel α› by (rule category_cat_Rel)
  note (*prefer cat_Rel*)[cat_cs_simps] = cat_Rel_is_arrD(2,3)

  from assms have GF'_GF: 
    "G' A×Rel F' ∘A⇘cat_Rel α⇙ G A×Rel F :
      B ×∘ A ↦⇘cat_Rel α⇙ B'' ×∘ A''"
    by (cs_concl cs_shallow cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros)
  from assms Rel.category_axioms have GG'_FF':
    "(G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F) : 
      B ×∘ A ↦⇘cat_Rel α⇙ B'' ×∘ A''"
    by (cs_concl cs_shallow cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros)

  show ?thesis
  proof(rule arr_Rel_eqI[of α])
    from GF'_GF show arr_Rel_GF'_GF:
      "arr_Rel α (G' A×Rel F' ∘A⇘cat_Rel α⇙ G A×Rel F)"
      by (auto dest: cat_Rel_is_arrD(1))
    from GG'_FF' show arr_Rel_GG'_FF':
      "arr_Rel α ((G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F))"
      by (auto dest: cat_Rel_is_arrD(1))
    show "(G' A×Rel F' ∘A⇘cat_Rel α⇙ G A×Rel F)⦇ArrVal⦈ = 
      ((G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F))⦇ArrVal⦈"
    proof(intro vsubset_antisym vsubsetI)
      fix R assume
        "R ∈∘ (G' A×Rel F' ∘A⇘cat_Rel α⇙ G A×Rel F)⦇ArrVal⦈"
      from this assms have "R ∈∘
        prod_2_Rel_ArrVal (G'⦇ArrVal⦈) (F'⦇ArrVal⦈) ∘∘
        prod_2_Rel_ArrVal (G⦇ArrVal⦈) (F⦇ArrVal⦈)"
        by 
          (
            cs_prems cs_shallow
              cs_simp: 
                prod_2_Rel_components(1) 
                comp_Rel_components(1)
                cat_Rel_cs_simps 
              cs_intro: cat_Rel_par_set_cs_intros
          )
      from this[unfolded prod_2_Rel_ArrVal_vcomp] assms show 
        "R ∈∘ ((G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F))⦇ArrVal⦈"
        by 
          (
            cs_concl cs_shallow cs_simp: 
              prod_2_Rel_components comp_Rel_components(1) cat_Rel_cs_simps 
          )
    next
      fix R assume
        "R ∈∘ ((G' ∘A⇘cat_Rel α⇙ G) A×Rel (F' ∘A⇘cat_Rel α⇙ F))⦇ArrVal⦈"
      from this assms have 
        "R ∈∘ prod_2_Rel_ArrVal (G'⦇ArrVal⦈ ∘∘ G⦇ArrVal⦈) (F'⦇ArrVal⦈ ∘∘ F⦇ArrVal⦈)"
        by 
          (
            cs_prems cs_shallow cs_simp:
              comp_Rel_components prod_2_Rel_components cat_Rel_cs_simps
          )
      from this[folded prod_2_Rel_ArrVal_vcomp] assms show
        "R ∈∘ ((G' A×Rel F') ∘A⇘cat_Rel α⇙ (G A×Rel F))⦇ArrVal⦈"
        by
          (
            cs_concl cs_shallow
              cs_simp:
                prod_2_Rel_components comp_Rel_components(1) cat_Rel_cs_simps 
              cs_intro: cat_Rel_par_set_cs_intros
          )
    qed

  qed
    (
      use GF'_GF assms in (*slow*)
        ‹
          cs_concl 
            cs_simp: cat_cs_simps
            cs_intro: cat_cs_intros cat_Rel_cs_intros
        ›
    )+

qed

lemma (in 𝒵) prod_2_Rel_CId[cat_cs_simps]:
  assumes "A ∈∘ cat_Rel α⦇Obj⦈" and "B ∈∘ cat_Rel α⦇Obj⦈"
  shows 
    "(cat_Rel α⦇CId⦈⦇A⦈) A×Rel (cat_Rel α⦇CId⦈⦇B⦈) = cat_Rel α⦇CId⦈⦇A ×∘ B⦈"
proof-
  interpret Rel: category α ‹cat_Rel α› by (rule category_cat_Rel)
  from assms have A_B: 
    "(cat_Rel α⦇CId⦈⦇A⦈) A×Rel (cat_Rel α⦇CId⦈⦇B⦈) :
      A ×∘ B ↦⇘cat_Rel α⇙ A ×∘ B"
    by (cs_concl cs_intro: cat_Rel_par_set_cs_intros cat_cs_intros)
  from assms Rel.category_axioms have AB:
    "cat_Rel α⦇CId⦈⦇A ×∘ B⦈ : A ×∘ B ↦⇘cat_Rel α⇙ A ×∘ B"
    by 
      (
        cs_concl  
          cs_simp: cat_Rel_components(1) cs_intro: V_cs_intros cat_cs_intros
      )
  show ?thesis
  proof(rule arr_Rel_eqI)
    from A_B show arr_Rel_GF'_GF:
      "arr_Rel α ((cat_Rel α⦇CId⦈⦇A⦈) A×Rel (cat_Rel α⦇CId⦈⦇B⦈))"
      by (auto dest: cat_Rel_is_arrD(1))
    from AB show arr_Rel_GG'_FF': "arr_Rel α (cat_Rel α⦇CId⦈⦇A ×∘ B⦈)"
      by (auto dest: cat_Rel_is_arrD(1))
    from assms show 
      "((cat_Rel α⦇CId⦈⦇A⦈) A×Rel (cat_Rel α⦇CId⦈⦇B⦈))⦇ArrVal⦈ =
        cat_Rel α⦇CId⦈⦇A ×∘ B⦈⦇ArrVal⦈"
      by
        (
          cs_concl 
            cs_simp:
              id_Rel_components prod_2_Rel_components
              cat_cs_simps cat_Rel_cs_simps 
            cs_intro: V_cs_intros  cat_cs_intros 
        )
  qed 
    (
      use A_B assms in 
        ‹
          cs_concl 
            cs_simp: prod_2_Rel_components cat_Rel_cs_simps 
            cs_intro: cat_cs_intros 
        ›
    )+
qed

lemma cf_dag_Rel_ArrMap_app_prod_2_Rel:
  assumes "S : A ↦⇘cat_Rel α⇙ B" and "T : C ↦⇘cat_Rel α⇙ D"
  shows
    "†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈ =
      (†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈)"
proof-

  interpret S: arr_Rel α S by (intro cat_Rel_is_arrD[OF assms(1)])
  interpret Rel: category α ‹cat_Rel α› by (rule S.category_cat_Rel)
  interpret dag_Rel: is_iso_functor α ‹op_cat (cat_Rel α)› ‹cat_Rel α› ‹†C.Rel α›
    by (rule S.cf_dag_Rel_is_iso_functor)

  note ST = prod_2_Rel_is_cat_Rel_arr[OF assms]

  from assms have dag_S: "†C.Rel α⦇ArrMap⦈⦇S⦈ : B ↦⇘cat_Rel α⇙ A"
    and dag_T: "†C.Rel α⦇ArrMap⦈⦇T⦈ : D ↦⇘cat_Rel α⇙ C"
    by
      (
        cs_concl 
          cs_simp: cat_Rel_cs_simps cat_op_simps cs_intro: cat_cs_intros 
      )+
  from assms have dag_prod:
    "†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈ : B ×∘ D ↦⇘cat_Rel α⇙ A ×∘ C"
    by
      (
        cs_concl 
          cs_simp: cat_Rel_cs_simps cat_op_simps 
          cs_intro: V_cs_intros cat_cs_intros cat_Rel_par_set_cs_intros 
      )
  from dag_S dag_T have prod_dag:
    "(†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈) :
      B ×∘ D ↦⇘cat_Rel α⇙ A ×∘ C" 
    by (cs_concl cs_shallow cs_intro: cat_Rel_par_set_cs_intros)

  note [cat_cs_simps] = 
    prod_2_Rel_ArrVal_vdomain prod_2_Rel_ArrVal_vrange prod_2_Rel_components
  from dag_prod ST have [cat_cs_simps]:
    "𝒟∘ (†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈⦇ArrVal⦈) = ℛ∘ (S⦇ArrVal⦈) ×∘ ℛ∘ (T⦇ArrVal⦈)"
    "ℛ∘ (†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈⦇ArrVal⦈) = 𝒟∘ (S⦇ArrVal⦈) ×∘ 𝒟∘ (T⦇ArrVal⦈)"
    by (cs_concl cs_simp: cat_cs_simps)+

 show
    "†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈ =
      (†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈)"
  proof(rule arr_Rel_eqI)
    from dag_prod show arr_Rel_dag_prod: 
      "arr_Rel α (†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈)"
      by (auto dest: cat_Rel_is_arrD)
    then interpret dag_prod: arr_Rel α ‹†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈› by simp
    from prod_dag show arr_Rel_prod_dag:
      "arr_Rel α ((†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈))"
      by (auto dest: cat_Rel_is_arrD)
    then interpret prod_dag: 
      arr_Rel α ‹(†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈)› 
      by simp
    from ST have arr_Rel_ST: "arr_Rel α (S A×Rel T)" 
      by (auto dest: cat_Rel_is_arrD)
    show
      "†C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈⦇ArrVal⦈ =
        ((†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈))⦇ArrVal⦈"
    proof(intro vsubset_antisym vsubsetI)
      fix bd_ac assume prems: "bd_ac ∈∘ †C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈⦇ArrVal⦈"
      then obtain bd ac 
        where bd_ac_def: "bd_ac = ⟨bd, ac⟩" 
          and bd: "bd ∈∘ ℛ∘ (S⦇ArrVal⦈) ×∘ ℛ∘ (T⦇ArrVal⦈)" 
          and ac: "ac ∈∘ 𝒟∘ (S⦇ArrVal⦈) ×∘ 𝒟∘ (T⦇ArrVal⦈)"
        by (elim cat_Rel_is_arr_ArrValE[OF dag_prod prems, unfolded cat_cs_simps])
      have "⟨ac, bd⟩ ∈∘ prod_2_Rel_ArrVal (S⦇ArrVal⦈) (T⦇ArrVal⦈)"
        by 
          (
            rule prems[
              unfolded
                bd_ac_def
                cf_dag_Rel_ArrMap_app_iff[OF ST] 
                prod_2_Rel_components
              ]
          )
      then obtain a b c d 
        where ab: "⟨a, b⟩ ∈∘ S⦇ArrVal⦈"
          and cd: "⟨c, d⟩ ∈∘ T⦇ArrVal⦈"
          and bd_def: "bd = ⟨b, d⟩" 
          and ac_def: "ac = ⟨a, c⟩"
        by auto
      show "bd_ac ∈∘ ((†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈))⦇ArrVal⦈"
        unfolding prod_2_Rel_components
      proof(intro prod_2_Rel_ArrValI)
        show "bd_ac = ⟨⟨b, d⟩, ⟨a, c⟩⟩" unfolding bd_ac_def bd_def ac_def by simp
        from assms ab cd show 
          "⟨b, a⟩ ∈∘ †C.Rel α⦇ArrMap⦈⦇S⦈⦇ArrVal⦈"
          "⟨d, c⟩ ∈∘ †C.Rel α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈"
          by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
      qed
    next
      fix bd_ac assume prems:
        "bd_ac ∈∘ ((†C.Rel α⦇ArrMap⦈⦇S⦈) A×Rel (†C.Rel α⦇ArrMap⦈⦇T⦈))⦇ArrVal⦈"
      then obtain a b c d 
        where bd_ac_def: "bd_ac = ⟨⟨b, d⟩, a, c⟩"
          and ba: "⟨b, a⟩ ∈∘ †C.Rel α⦇ArrMap⦈⦇S⦈⦇ArrVal⦈"
          and dc: "⟨d, c⟩ ∈∘ †C.Rel α⦇ArrMap⦈⦇T⦈⦇ArrVal⦈"
        by (elim prod_2_Rel_ArrValE[OF prems[unfolded prod_2_Rel_components]])
      then have ab: "⟨a, b⟩ ∈∘ S⦇ArrVal⦈" and cd: "⟨c, d⟩ ∈∘ T⦇ArrVal⦈"
        unfolding assms[THEN cf_dag_Rel_ArrMap_app_iff] by simp_all
      from ST ab cd show "bd_ac ∈∘ †C.Rel α⦇ArrMap⦈⦇S A×Rel T⦈⦇ArrVal⦈"
        unfolding bd_ac_def 
        by
          (
            cs_concl cs_shallow
              cs_simp: prod_2_Rel_components cat_cs_simps 
              cs_intro: prod_2_Rel_ArrValI cat_cs_intros 
          )
    qed
  qed (use dag_prod prod_dag in ‹cs_concl cs_simp: cat_cs_simps›)+

qed



subsection‹Product functor for ‹Rel››

definition cf_prod_2_Rel :: "V ⇒ V"
  where "cf_prod_2_Rel 𝔄 =
    [
      (λAB∈∘(𝔄 ×C 𝔄)⦇Obj⦈. AB⦇0⦈ ×∘ AB⦇1ℕ⦈),
      (λST∈∘(𝔄 ×C 𝔄)⦇Arr⦈. (ST⦇0⦈) A×Rel (ST⦇1ℕ⦈)),
      𝔄 ×C 𝔄,
      𝔄
    ]∘"


text‹Components.›

lemma cf_prod_2_Rel_components: 
  shows "cf_prod_2_Rel 𝔄⦇ObjMap⦈ = (λAB∈∘(𝔄 ×C 𝔄)⦇Obj⦈. AB⦇0⦈ ×∘ AB⦇1ℕ⦈)"
    and "cf_prod_2_Rel 𝔄⦇ArrMap⦈ =
      (λST∈∘(𝔄 ×C 𝔄)⦇Arr⦈. (ST⦇0⦈) A×Rel (ST⦇1ℕ⦈))"
    and [cat_cs_simps]: "cf_prod_2_Rel 𝔄⦇HomDom⦈ = 𝔄 ×C 𝔄"
    and [cat_cs_simps]: "cf_prod_2_Rel 𝔄⦇HomCod⦈ = 𝔄"
  unfolding cf_prod_2_Rel_def dghm_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda cf_prod_2_Rel_components(1)
  |vsv cf_prod_2_Rel_ObjMap_vsv[cat_cs_intros]|
  |vdomain cf_prod_2_Rel_ObjMap_vdomain[cat_cs_simps]|

lemma cf_prod_2_Rel_ObjMap_app[cat_cs_simps]: 
  assumes "AB = [A, B]∘" and "AB ∈∘ (𝔄 ×C 𝔄)⦇Obj⦈"
  shows "A ⊗HM.O⇘cf_prod_2_Rel 𝔄⇙ B = A ×∘ B"
  using assms(2) 
  unfolding assms(1) cf_prod_2_Rel_components 
  by (simp add: nat_omega_simps)

lemma (in 𝒵) cf_prod_2_Rel_ObjMap_vrange: 
  "ℛ∘ (cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈) ⊆∘ cat_Rel α⦇Obj⦈"
proof-
  interpret Rel: category α ‹cat_Rel α›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)
  show ?thesis
  proof(rule vsv.vsv_vrange_vsubset, unfold cat_cs_simps)
    fix AB assume prems: "AB ∈∘ (cat_Rel α ×C cat_Rel α)⦇Obj⦈"
    with Rel.category_axioms obtain A B where AB_def: "AB = [A, B]∘"
      and A: "A ∈∘ cat_Rel α⦇Obj⦈"
      and B: "B ∈∘ cat_Rel α⦇Obj⦈"
      by (elim cat_prod_2_ObjE[rotated 2])
    from prems A B show "cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈⦇AB⦈ ∈∘ cat_Rel α⦇Obj⦈"
      unfolding AB_def cat_Rel_components(1)
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_cs_simps cat_Rel_cs_simps cs_intro: V_cs_intros
        )
  qed (cs_concl cs_shallow cs_intro: cat_cs_intros)
qed


subsubsection‹Arrow map›

mk_VLambda cf_prod_2_Rel_components(2)
  |vsv cf_prod_2_Rel_ArrMap_vsv[cat_cs_intros]|
  |vdomain cf_prod_2_Rel_ArrMap_vdomain[cat_cs_simps]|

lemma cf_prod_2_Rel_ArrMap_app[cat_cs_simps]: 
  assumes "GF = [G, F]∘" and "GF ∈∘ (𝔄 ×C 𝔄)⦇Arr⦈"
  shows "G ⊗HM.A⇘cf_prod_2_Rel 𝔄⇙ F = G A×Rel F"
  using assms(2) 
  unfolding assms(1) cf_prod_2_Rel_components 
  by (simp add: nat_omega_simps)


subsubsection‹Product functor for ‹Rel› is a functor›

lemma (in 𝒵) cf_prod_2_Rel_is_functor:
  "cf_prod_2_Rel (cat_Rel α) : cat_Rel α ×C cat_Rel α ↦↦C⇘α⇙ cat_Rel α"
proof-

  interpret Rel: category α ‹cat_Rel α›
    by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_Rel_cs_intros)

  show ?thesis
  proof(rule is_functorI')
   show "vfsequence (cf_prod_2_Rel (cat_Rel α))"
      unfolding cf_prod_2_Rel_def by auto
    show "vcard (cf_prod_2_Rel (cat_Rel α)) = 4ℕ"
      unfolding cf_prod_2_Rel_def by (simp add: nat_omega_simps)
    show "ℛ∘ (cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈) ⊆∘ cat_Rel α⦇Obj⦈"
      by (rule cf_prod_2_Rel_ObjMap_vrange)
    show "cf_prod_2_Rel (cat_Rel α)⦇ArrMap⦈⦇GF⦈ :
      cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈⦇AB⦈ ↦⇘cat_Rel α⇙
      cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈⦇CD⦈"
      if "GF : AB ↦⇘cat_Rel α ×C cat_Rel α⇙ CD" for AB CD GF
    proof-
      from that obtain G F A B C D
        where GF_def: "GF = [G, F]∘"
          and AB_def: "AB = [A, B]∘"
          and CD_def: "CD = [C, D]∘"
          and G: "G : A ↦⇘cat_Rel α⇙ C"
          and F: "F : B ↦⇘cat_Rel α⇙ D"
        by (elim cat_prod_2_is_arrE[OF Rel.category_axioms Rel.category_axioms])
      from that G F show ?thesis
        unfolding GF_def AB_def CD_def
        by
          (
            cs_concl 
              cs_simp: cat_cs_simps 
              cs_intro: 
                cat_Rel_par_set_cs_intros cat_cs_intros cat_prod_cs_intros
          )
    qed

    show 
      "cf_prod_2_Rel (cat_Rel α)⦇ArrMap⦈⦇GF' ∘A⇘cat_Rel α ×C cat_Rel α⇙ GF⦈ =
        cf_prod_2_Rel (cat_Rel α)⦇ArrMap⦈⦇GF'⦈ ∘A⇘cat_Rel α⇙
          cf_prod_2_Rel (cat_Rel α)⦇ArrMap⦈⦇GF⦈"
      if "GF' : AB' ↦⇘cat_Rel α ×C cat_Rel α⇙ AB''"
        and "GF : AB ↦⇘cat_Rel α ×C cat_Rel α⇙ AB'"
      for AB' AB'' GF' AB GF
    proof-
      from that(2) obtain G F A A' B B' 
        where GF_def: "GF = [G, F]∘"
          and AB_def: "AB = [A, B]∘"
          and AB'_def: "AB' = [A', B']∘"
          and G: "G : A ↦⇘cat_Rel α⇙ A'"
          and F: "F : B ↦⇘cat_Rel α⇙ B'"
        by (elim cat_prod_2_is_arrE[OF Rel.category_axioms Rel.category_axioms])
      with that(1) obtain G' F' A'' B''
        where GF'_def: "GF' = [G', F']∘"
          and AB''_def: "AB'' = [A'', B'']∘"
          and G': "G' : A' ↦⇘cat_Rel α⇙ A''"
          and F': "F' : B' ↦⇘cat_Rel α⇙ B''"
        by 
          (
            auto elim: 
              cat_prod_2_is_arrE[OF Rel.category_axioms Rel.category_axioms]
          )
      from that G F G' F' show ?thesis
        unfolding GF_def AB_def AB'_def GF'_def AB''_def
        by
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps cat_prod_cs_simps prod_2_Rel_Comp
              cs_intro: cat_cs_intros cat_prod_cs_intros
          )
    qed

    show 
      "cf_prod_2_Rel (cat_Rel α)⦇ArrMap⦈⦇(cat_Rel α ×C cat_Rel α)⦇CId⦈⦇AB⦈⦈ =
        cat_Rel α⦇CId⦈⦇cf_prod_2_Rel (cat_Rel α)⦇ObjMap⦈⦇AB⦈⦈"
      if "AB ∈∘ (cat_Rel α ×C cat_Rel α)⦇Obj⦈" for AB 
    proof-
      from that obtain A B 
        where AB_def: "AB = [A, B]∘"
          and A: "A ∈∘ cat_Rel α⦇Obj⦈"
          and B: "B ∈∘ cat_Rel α⦇Obj⦈"
        by (elim cat_prod_2_ObjE[OF Rel.category_axioms Rel.category_axioms])
      from A B show ?thesis
        unfolding AB_def     
        by
          (
            cs_concl 
              cs_simp:
                cf_prod_2_Rel_ObjMap_app cf_prod_2_Rel_ArrMap_app
                cat_cs_simps cat_prod_cs_simps
              cs_intro:
                V_cs_intros cat_cs_intros cat_Rel_cs_intros cat_prod_cs_intros
          )
    qed

  qed
    (
      cs_concl cs_shallow
        cs_simp: cat_cs_simps 
        cs_intro: cat_cs_intros cat_cs_intros cat_Rel_cs_intros
    )+

qed

lemma (in 𝒵) cf_prod_2_Rel_is_functor'[cat_cs_intros]:
  assumes "𝔄' = cat_Rel α ×C cat_Rel α"
    and "𝔅' = cat_Rel α"
    and "α' = α"
  shows "cf_prod_2_Rel (cat_Rel α) : 𝔄' ↦↦C⇘α'⇙ 𝔅'"
  unfolding assms by (rule cf_prod_2_Rel_is_functor)

lemmas [cat_cs_intros] = 𝒵.cf_prod_2_Rel_is_functor'



subsection‹Product universal property arrow for ‹Set››


subsubsection‹Definition and elementary properties›

definition cat_Set_obj_prod_up :: "V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "cat_Set_obj_prod_up I F A φ =
    [(λa∈∘A. (λi∈∘I. φ i⦇ArrVal⦈⦇a⦈)), A, (∏∘i∈∘I. F i)]∘"


text‹Components.›

lemma cat_Set_obj_prod_up_components: 
  shows "cat_Set_obj_prod_up I F A φ⦇ArrVal⦈ = 
    (λa∈∘A. (λi∈∘I. φ i⦇ArrVal⦈⦇a⦈))"
    and [cat_Set_cs_simps]: 
      "cat_Set_obj_prod_up I F A φ⦇ArrDom⦈ = A"
    and [cat_Set_cs_simps]: 
      "cat_Set_obj_prod_up I F A φ⦇ArrCod⦈ = (∏∘i∈∘I. F i)"
  unfolding cat_Set_obj_prod_up_def arr_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda cat_Set_obj_prod_up_components(1)
  |vsv cat_Set_obj_prod_up_ArrVal_vsv[cat_Set_cs_intros]|
  |vdomain cat_Set_obj_prod_up_ArrVal_vdomain[cat_Set_cs_simps]|
  |app cat_Set_obj_prod_up_ArrVal_app|

lemma cat_Set_obj_prod_up_ArrVal_vrange: 
  assumes "⋀i. i ∈∘ I ⟹ φ i : A ↦⇘cat_Set α⇙ F i"
  shows "ℛ∘ (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈) ⊆∘ (∏∘i∈∘I. F i)"
  unfolding cat_Set_obj_prod_up_components 
proof(intro vrange_VLambda_vsubset vproductI)
  fix a assume prems: "a ∈∘ A"
  show "∀i∈∘I. (λi∈∘I. φ i⦇ArrVal⦈⦇a⦈)⦇i⦈ ∈∘ F i"
  proof(intro ballI)
    fix i assume "i ∈∘ I"
    with assms prems show "(λi∈∘I. φ i⦇ArrVal⦈⦇a⦈)⦇i⦈ ∈∘ F i"
      by (cs_concl cs_shallow cs_simp: V_cs_simps cs_intro: cat_Set_cs_intros)
  qed
qed auto

lemma cat_Set_obj_prod_up_ArrVal_app_vdomain[cat_Set_cs_simps]:
  assumes "a ∈∘ A"
  shows "𝒟∘ (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈) = I"
  unfolding cat_Set_obj_prod_up_ArrVal_app[OF assms] by simp

lemma cat_Set_obj_prod_up_ArrVal_app_component[cat_Set_cs_simps]: 
  assumes "a ∈∘ A" and "i ∈∘ I"
  shows "cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈⦇i⦈ = φ i⦇ArrVal⦈⦇a⦈"
  using assms 
  by (cs_concl cs_shallow cs_simp: cat_Set_obj_prod_up_ArrVal_app V_cs_simps)

lemma cat_Set_obj_prod_up_ArrVal_app_vrange: 
  assumes "a ∈∘ A" and "⋀i. i ∈∘ I ⟹ φ i : A ↦⇘cat_Set α⇙ F i"
  shows "ℛ∘ (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. F i)"
proof(intro vsubsetI)
  fix b assume prems: "b ∈∘ ℛ∘ (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈)"
  from assms(1) have "vsv (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈)"
    by (auto simp: cat_Set_obj_prod_up_components)
  with prems obtain i 
    where b_def: "b = cat_Set_obj_prod_up I F A φ⦇ArrVal⦈⦇a⦈⦇i⦈" 
      and i: "i ∈∘ I"
    by 
      ( 
        auto 
          elim: vsv.vrange_atE 
          simp: cat_Set_obj_prod_up_ArrVal_app[OF assms(1)]
      )
  from cat_Set_obj_prod_up_ArrVal_app_component[OF assms(1) i] b_def have b_def':
    "b = φ i⦇ArrVal⦈⦇a⦈"
    by simp
  from assms(1) assms(2)[OF i] have "b ∈∘ F i" 
    unfolding b_def' by (cs_concl cs_shallow cs_intro: cat_Set_cs_intros)
  with i show "b ∈∘ (⋃∘i∈∘I. F i)" by force
qed


subsubsection‹Product universal property arrow for ‹Set› is an arrow in ‹Set››

lemma (in 𝒵) cat_Set_obj_prod_up_cat_Set_is_arr:
  assumes "A ∈∘ cat_Set α⦇Obj⦈" 
    and "VLambda I F ∈∘ Vset α" 
    and "⋀i. i ∈∘ I ⟹ φ i : A ↦⇘cat_Set α⇙ F i"
  shows "cat_Set_obj_prod_up I F A φ : A ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i)"
proof(intro cat_Set_is_arrI arr_SetI)
  show "vfsequence (cat_Set_obj_prod_up I F A φ)"
    unfolding cat_Set_obj_prod_up_def by auto
  show "vcard (cat_Set_obj_prod_up I F A φ) = 3ℕ"
    unfolding cat_Set_obj_prod_up_def by (auto simp: nat_omega_simps)
  show 
    "ℛ∘ (cat_Set_obj_prod_up I F A φ⦇ArrVal⦈) ⊆∘
      cat_Set_obj_prod_up I F A φ⦇ArrCod⦈"
    unfolding cat_Set_obj_prod_up_components(3)
    by (rule cat_Set_obj_prod_up_ArrVal_vrange[OF assms(3)])
  show "cat_Set_obj_prod_up I F A φ⦇ArrCod⦈ ∈∘ Vset α"
    unfolding cat_Set_cs_simps
    by (rule Limit_vproduct_in_Vset_if_VLambda_in_VsetI)
      (simp_all add: cat_Set_cs_simps assms)
qed 
  (
    auto 
      simp: assms[unfolded cat_Set_components(1)] cat_Set_cs_simps 
      intro: cat_Set_cs_intros
  )


subsubsection‹Further properties›

lemma (in 𝒵) cat_Set_cf_comp_proj_obj_prod_up: 
  assumes "A ∈∘ cat_Set α⦇Obj⦈" 
    and "VLambda I F ∈∘ Vset α"
    and "⋀i. i ∈∘ I ⟹ φ i : A ↦⇘cat_Set α⇙ F i" 
    and "i ∈∘ I"
  shows 
    "φ i = vprojection_arrow I F i ∘A⇘cat_Set α⇙ cat_Set_obj_prod_up I F A φ"
    (is ‹φ i = ?Fi ∘A⇘cat_Set α⇙ ?φ›)
proof(rule arr_Set_eqI[of α])
  note φi = assms(3)[OF assms(4)]
  note φi = cat_Set_is_arrD[OF φi] φi
  have Fi: "?Fi : (∏∘i∈∘I. F i) ↦⇘cat_Set α⇙ F i"
    by (rule vprojection_arrow_is_arr[OF assms(4,2)])
  from cat_Set_obj_prod_up_cat_Set_is_arr[OF assms(1,2,3)] have φ:
    "cat_Set_obj_prod_up I F A φ : A ↦⇘cat_Set α⇙ (∏∘i∈∘I. F i)"
    by simp
  show "arr_Set α (φ i)" by (rule φi(1))
  interpret φi: arr_Set α ‹φ i› by (rule φi(1))
  from Fi φ have Fi_φ: "?Fi ∘A⇘cat_Set α⇙ ?φ : A ↦⇘cat_Set α⇙ F i"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  then show arr_Set_Fi_φ: "arr_Set α (?Fi ∘A⇘cat_Set α⇙ ?φ)"
    by (auto simp: cat_Set_is_arrD(1))
  interpret arr_Set α ‹?Fi ∘A⇘cat_Set α⇙ ?φ› by (rule arr_Set_Fi_φ)
  from φi have dom_lhs: "𝒟∘ (φ i⦇ArrVal⦈) = A"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from Fi_φ have dom_rhs: "𝒟∘ ((?Fi ∘A⇘cat_Set α⇙ ?φ)⦇ArrVal⦈) = A"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "φ i⦇ArrVal⦈ = (?Fi ∘A⇘cat_Set α⇙ ?φ)⦇ArrVal⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume prems: "a ∈∘ A"
    from assms(4) prems φi(4) φ Fi show 
      "φ i⦇ArrVal⦈⦇a⦈ = (?Fi ∘A⇘cat_Set α⇙ ?φ)⦇ArrVal⦈⦇a⦈"
      by 
        ( 
          cs_concl cs_shallow
            cs_simp: cat_Set_cs_simps cat_cs_simps 
            cs_intro: cat_Set_cs_intros cat_cs_intros
        )
  qed auto
  from Fi φ show
    "φ i⦇ArrDom⦈ = (?Fi ∘A⇘cat_Set α⇙ ?φ)⦇ArrDom⦈"
    "φ i⦇ArrCod⦈ = (?Fi ∘A⇘cat_Set α⇙ ?φ)⦇ArrCod⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_Set_cs_simps φi(2,3))+
qed



subsection‹Coproduct universal property arrow for ‹Set››


subsubsection‹Definition and elementary properties›

definition cat_Set_obj_coprod_up :: "V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "cat_Set_obj_coprod_up I F A φ =
    [(λix∈∘(∐∘i∈∘I. F i). φ (vfst ix)⦇ArrVal⦈⦇vsnd ix⦈), (∐∘i∈∘I. F i), A]∘"


text‹Components.›

lemma cat_Set_obj_coprod_up_components: 
  shows "cat_Set_obj_coprod_up I F A φ⦇ArrVal⦈ = 
    (λix∈∘(∐∘i∈∘I. F i). φ (vfst ix)⦇ArrVal⦈⦇vsnd ix⦈)"
    and [cat_Set_cs_simps]: 
      "cat_Set_obj_coprod_up I F A φ⦇ArrDom⦈ = (∐∘i∈∘I. F i)"
    and [cat_Set_cs_simps]: 
      "cat_Set_obj_coprod_up I F A φ⦇ArrCod⦈ = A"
  unfolding cat_Set_obj_coprod_up_def arr_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda cat_Set_obj_coprod_up_components(1)
  |vsv cat_Set_obj_coprod_up_ArrVal_vsv[cat_Set_cs_intros]|
  |vdomain cat_Set_obj_coprod_up_ArrVal_vdomain[cat_Set_cs_simps]|
  |app cat_Set_obj_coprod_up_ArrVal_app'|

lemma cat_Set_obj_coprod_up_ArrVal_app[cat_cs_simps]:
  assumes "ix = ⟨i, x⟩" and "⟨i, x⟩ ∈∘ (∐∘i∈∘I. F i)"
  shows "cat_Set_obj_coprod_up I F A φ⦇ArrVal⦈⦇ix⦈ = φ i⦇ArrVal⦈⦇x⦈"
  using assms by (auto simp: cat_Set_obj_coprod_up_ArrVal_app')

lemma cat_Set_obj_coprod_up_ArrVal_vrange:
  assumes "⋀i. i ∈∘ I ⟹ φ i : F i ↦⇘cat_Set α⇙ A"
  shows "ℛ∘ (cat_Set_obj_coprod_up I F A φ⦇ArrVal⦈) ⊆∘ A"
proof
  (
    intro vsv.vsv_vrange_vsubset cat_Set_obj_coprod_up_ArrVal_vsv, 
    unfold cat_Set_cs_simps
  )
  fix ix assume "ix ∈∘ (∐∘i∈∘I. F i)"
  then obtain i x where ix_def: "ix = ⟨i, x⟩" and i: "i ∈∘ I" and x: "x ∈∘ F i" 
    by auto
  show "cat_Set_obj_coprod_up I F A φ⦇ArrVal⦈⦇ix⦈ ∈∘ A"
  proof(cs_concl_step cat_Set_obj_coprod_up_ArrVal_app)
    show "ix = ⟨i, x⟩" by (rule ix_def)
    from i x show "⟨i, x⟩ ∈∘ (∐∘i∈∘I. F i)" by auto
    from i x assms[OF i] show "φ i⦇ArrVal⦈⦇x⦈ ∈∘ A"
      by (auto intro: cat_Set_ArrVal_app_vrange)
  qed
qed


subsubsection‹Coproduct universal property arrow for ‹Set› is an arrow in ‹Set››

lemma (in 𝒵) cat_Set_obj_coprod_up_cat_Set_is_arr:
  assumes "A ∈∘ cat_Set α⦇Obj⦈" 
    and "VLambda I F ∈∘ Vset α" 
    and "⋀i. i ∈∘ I ⟹ φ i : F i ↦⇘cat_Set α⇙ A"
  shows "cat_Set_obj_coprod_up I F A φ : (∐∘i∈∘I. F i) ↦⇘cat_Set α⇙ A"
proof(intro cat_Set_is_arrI arr_SetI)
  show "vfsequence (cat_Set_obj_coprod_up I F A φ)"
    unfolding cat_Set_obj_coprod_up_def by auto
  show "vcard (cat_Set_obj_coprod_up I F A φ) = 3ℕ"
    unfolding cat_Set_obj_coprod_up_def by (auto simp: nat_omega_simps)
  show 
    "ℛ∘ (cat_Set_obj_coprod_up I F A φ⦇ArrVal⦈) ⊆∘
      cat_Set_obj_coprod_up I F A φ⦇ArrCod⦈"
    unfolding cat_Set_obj_coprod_up_components(3)
    by (rule cat_Set_obj_coprod_up_ArrVal_vrange[OF assms(3)])
  show "cat_Set_obj_coprod_up I F A φ⦇ArrCod⦈ ∈∘ Vset α"
    by (simp_all add: cat_Set_cs_simps assms[unfolded cat_Set_components(1)])
qed 
  (
    auto simp: 
      assms 
      cat_Set_obj_coprod_up_components 
      Limit_vdunion_in_Vset_if_VLambda_in_VsetI
  ) 


subsubsection‹Further properties›

lemma (in 𝒵) cat_Set_cf_comp_coprod_up_vcia:
  assumes "A ∈∘ cat_Set α⦇Obj⦈"
    and "VLambda I F ∈∘ Vset α"
    and "⋀i. i ∈∘ I ⟹ φ i : F i ↦⇘cat_Set α⇙ A" 
    and "i ∈∘ I"
  shows 
    "φ i = cat_Set_obj_coprod_up I F A φ ∘A⇘cat_Set α⇙ vcinjection_arrow I F i"
    (is ‹φ i = ?φ ∘A⇘cat_Set α⇙ ?Fi›)
proof(rule arr_Set_eqI[of α])
  note φi = assms(3)[OF assms(4)]
  note φi = cat_Set_is_arrD[OF φi] φi
  have Fi: "?Fi : F i ↦⇘cat_Set α⇙ (∐∘i∈∘I. F i)"
    by (rule vcinjection_arrow_is_arr[OF assms(4,2)])
  from cat_Set_obj_coprod_up_cat_Set_is_arr[OF assms(1,2,3)] have φ:
    "cat_Set_obj_coprod_up I F A φ : (∐∘i∈∘I. F i) ↦⇘cat_Set α⇙ A"
    by simp
  show "arr_Set α (φ i)" by (rule φi(1))
  then interpret φi: arr_Set α ‹φ i› .
  from Fi φ have Fi_φ: "?φ ∘A⇘cat_Set α⇙ ?Fi : F i ↦⇘cat_Set α⇙ A"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros)
  then show arr_Set_Fi_φ: "arr_Set α (?φ ∘A⇘cat_Set α⇙ ?Fi)"
    by (auto simp: cat_Set_is_arrD(1))
  interpret arr_Set α ‹?φ ∘A⇘cat_Set α⇙ ?Fi› by (rule arr_Set_Fi_φ)
  from φi have dom_lhs: "𝒟∘ (φ i⦇ArrVal⦈) = F i"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)
  from Fi_φ have dom_rhs: "𝒟∘ ((?φ ∘A⇘cat_Set α⇙ ?Fi)⦇ArrVal⦈) = F i"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
  show "φ i⦇ArrVal⦈ = (?φ ∘A⇘cat_Set α⇙ ?Fi)⦇ArrVal⦈"
  proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
    fix a assume "a ∈∘ F i"
    from assms(4) this φi(4) φ Fi show 
      "φ i⦇ArrVal⦈⦇a⦈ = (?φ ∘A⇘cat_Set α⇙ ?Fi)⦇ArrVal⦈⦇a⦈"
      by
        (
          cs_concl cs_shallow
            cs_simp: cat_Set_cs_simps cat_cs_simps 
            cs_intro: vdunionI cat_Set_cs_intros cat_cs_intros
        )
  qed auto
  from Fi φ show 
    "φ i⦇ArrDom⦈ = (?φ ∘A⇘cat_Set α⇙ ?Fi)⦇ArrDom⦈"
    "φ i⦇ArrCod⦈ = (?φ ∘A⇘cat_Set α⇙ ?Fi)⦇ArrCod⦈"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_Set_cs_simps φi(2,3))+
qed



subsection‹Equalizer object for the category ‹Set››


text‹
The definition of the (non-categorical concept of an) equalizer can be 
found in cite‹"noauthor_wikipedia_2001"›\footnote{
\url{https://en.wikipedia.org/wiki/Equaliser_(mathematics)}
}›

definition vequalizer :: "V ⇒ V ⇒ V ⇒ V"
  where "vequalizer X f g = set {x. x ∈∘ X ∧ f⦇ArrVal⦈⦇x⦈ = g⦇ArrVal⦈⦇x⦈}"

lemma small_vequalizer[simp]: 
  "small {x. x ∈∘ X ∧ f⦇ArrVal⦈⦇x⦈ = g⦇ArrVal⦈⦇x⦈}"
  by auto


text‹Rules.›

lemma vequalizerI:
  assumes "x ∈∘ X" and "f⦇ArrVal⦈⦇x⦈ = g⦇ArrVal⦈⦇x⦈"
  shows "x ∈∘ vequalizer X f g"
  using assms unfolding vequalizer_def by auto

lemma vequalizerD[dest]:
  assumes "x ∈∘ vequalizer X f g"
  shows "x ∈∘ X" and "f⦇ArrVal⦈⦇x⦈ = g⦇ArrVal⦈⦇x⦈"
  using assms unfolding vequalizer_def by auto

lemma vequalizerE[elim]:
  assumes "x ∈∘ vequalizer X f g"
  obtains "x ∈∘ X" and "f⦇ArrVal⦈⦇x⦈ = g⦇ArrVal⦈⦇x⦈"
  using assms unfolding vequalizer_def by auto


text‹Elementary results.›

lemma vequalizer_vsubset_vdomain[cat_Set_cs_intros]: "vequalizer a g f ⊆∘ a" 
  by auto
  
lemma Limit_vequalizer_in_Vset[cat_Set_cs_intros]:
  assumes "Limit α" and "a ∈∘ cat_Set α⦇Obj⦈"
  shows "vequalizer a g f ∈∘ cat_Set α⦇Obj⦈"
  using assms unfolding cat_Set_components(1) by auto

lemma vequalizer_flip: "vequalizer a f g = vequalizer a g f"
  unfolding vequalizer_def by auto

lemma cat_Set_incl_Set_commute:
  assumes "𝔤 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" and "𝔣 : 𝔞 ↦⇘cat_Set α⇙ 𝔟" 
  shows 
    "𝔤 ∘A⇘cat_Set α⇙ incl_Set (vequalizer 𝔞 𝔣 𝔤) 𝔞 =
      𝔣 ∘A⇘cat_Set α⇙ incl_Set (vequalizer 𝔞 𝔣 𝔤) 𝔞"
  (is ‹𝔤 ∘A⇘cat_Set α⇙ ?incl = 𝔣 ∘A⇘cat_Set α⇙ ?incl›)
proof-

  interpret 𝔤: arr_Set α 𝔤 
    rewrites "𝔤⦇ArrDom⦈ = 𝔞" and "𝔤⦇ArrCod⦈ = 𝔟"
    by (intro cat_Set_is_arrD[OF assms(1)])+
  interpret 𝔣: arr_Set α 𝔣 
    rewrites "𝔣⦇ArrDom⦈ = 𝔞" and "𝔣⦇ArrCod⦈ = 𝔟"
    by (intro cat_Set_is_arrD[OF assms(2)])+

  note [cat_Set_cs_intros] = 𝔤.arr_Set_ArrDom_in_Vset 𝔣.arr_Set_ArrCod_in_Vset

  from assms have 𝔤_incl: 
    "𝔤 ∘A⇘cat_Set α⇙ ?incl : vequalizer 𝔞 𝔣 𝔤 ↦⇘cat_Set α⇙ 𝔟"
    by (cs_concl cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros)
  then have dom_lhs: "𝒟∘ ((𝔤 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈) = vequalizer 𝔞 𝔣 𝔤"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)+
  from assms have 𝔣_incl: 
    "𝔣 ∘A⇘cat_Set α⇙ ?incl : vequalizer 𝔞 𝔣 𝔤 ↦⇘cat_Set α⇙ 𝔟"
    by (cs_concl cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros)
  then have dom_rhs: "𝒟∘ ((𝔣 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈) = vequalizer 𝔞 𝔣 𝔤"
    by (cs_concl cs_shallow cs_simp: cat_cs_simps)+

  show ?thesis
  proof(rule arr_Set_eqI)
    from 𝔤_incl show arr_Set_𝔤_incl: "arr_Set α (𝔤 ∘A⇘cat_Set α⇙ ?incl)"
      by (auto dest: cat_Set_is_arrD(1))
    interpret arr_Set_𝔤_incl: arr_Set α ‹𝔤 ∘A⇘cat_Set α⇙ ?incl›
      by (rule arr_Set_𝔤_incl)
    from 𝔣_incl show arr_Set_𝔣_incl: "arr_Set α (𝔣 ∘A⇘cat_Set α⇙ ?incl)"
      by (auto dest: cat_Set_is_arrD(1))
    interpret arr_Set_𝔣_incl: arr_Set α ‹𝔣 ∘A⇘cat_Set α⇙ ?incl›
      by (rule arr_Set_𝔣_incl)
    show "(𝔤 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈ = (𝔣 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈"
    proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
      fix a assume "a ∈∘ vequalizer 𝔞 𝔣 𝔤"
      with assms show 
        "(𝔤 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈⦇a⦈ = (𝔣 ∘A⇘cat_Set α⇙ ?incl)⦇ArrVal⦈⦇a⦈"
        by (*very slow*)
          (
            cs_concl 
              cs_simp: vequalizerD(2) cat_Set_cs_simps cat_cs_simps
              cs_intro: V_cs_intros cat_Set_cs_intros cat_cs_intros
          )
    qed auto
  qed (use 𝔤_incl 𝔣_incl in ‹cs_concl cs_shallow cs_simp: cat_cs_simps›)+

qed



subsection‹Application of a function to a finite sequence as an arrow in ‹Set››

definition vfsequence_map :: "V ⇒ V"
  where "vfsequence_map F =
    [
      (λxs∈∘vfsequences_on (F⦇ArrDom⦈). F⦇ArrVal⦈ ∘∘ xs),
      vfsequences_on (F⦇ArrDom⦈),
      vfsequences_on (F⦇ArrCod⦈)
    ]∘"


text‹Components.›

lemma vfsequence_map_components:
  shows "vfsequence_map F⦇ArrVal⦈ =
    (λxs∈∘vfsequences_on (F⦇ArrDom⦈). F⦇ArrVal⦈ ∘∘ xs)"
    and [cat_cs_simps]: "vfsequence_map F⦇ArrDom⦈ = vfsequences_on (F⦇ArrDom⦈)"
    and [cat_cs_simps]: "vfsequence_map F⦇ArrCod⦈ = vfsequences_on (F⦇ArrCod⦈)"
  unfolding vfsequence_map_def arr_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda vfsequence_map_components(1)
  |vsv vfsequence_map_ArrVal_vsv[cat_cs_intros, cat_Set_cs_intros]|
  |vdomain vfsequence_map_ArrVal_vdomain[cat_cs_simps, cat_Set_cs_simps]|
  |app vfsequence_map_ArrVal_app|

lemma vfsequence_map_ArrVal_app_app:
  assumes "F : A ↦⇘cat_Set α⇙ B" 
    and "xs ∈∘ vfsequences_on A"
    and "i ∈∘ 𝒟∘ xs"
  shows "vfsequence_map F⦇ArrVal⦈⦇xs⦈⦇i⦈ = F⦇ArrVal⦈⦇xs⦇i⦈⦈"
proof-
  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret arr_Set α F 
    rewrites "F⦇ArrDom⦈ = A" and "F⦇ArrCod⦈ = B"
    by (intro FD)+
  note xsD = vfsequences_onD[OF assms(2)]
  interpret xs: vfsequence xs by (rule xsD(1))
  from assms xsD(2)[OF assms(3)] show ?thesis
    by
      (
        cs_concl
          cs_simp: V_cs_simps cat_cs_simps vfsequence_map_ArrVal_app
          cs_intro: V_cs_intros
      )
qed


subsubsection‹
Application of a function to a finite sequence is an arrow in ‹Set›
›

lemma vfsequence_map_is_arr:
  assumes "F : A ↦⇘cat_Set α⇙ B"
  shows "vfsequence_map F : vfsequences_on A ↦⇘cat_Set α⇙ vfsequences_on B"
proof-

  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret arr_Set α F 
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+

  show ?thesis
  proof(intro cat_Set_is_arrI arr_SetI , unfold cat_cs_simps)
    show "vfsequence (vfsequence_map F)"
      unfolding vfsequence_map_def by auto
    show "vcard (vfsequence_map F) = 3ℕ"
      unfolding vfsequence_map_def by (simp_all add: nat_omega_simps)
    show "ℛ∘ (vfsequence_map F⦇ArrVal⦈) ⊆∘ vfsequences_on B"
      unfolding vfsequence_map_components
    proof
      (
        intro vrange_VLambda_vsubset vfsequences_onI; 
        elim vfsequences_onE; 
        unfold cat_cs_simps
      )
      fix xs assume prems: "vfsequence xs" "i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ A" for i
      interpret xs: vfsequence xs by (rule prems(1))
      have [intro]: "x ∈∘ 𝒟∘ (F⦇ArrVal⦈)" if "x ∈∘ ℛ∘ xs" for x
      proof-
        from that obtain i where i: "i ∈∘ 𝒟∘ xs" and x_def: "x = xs⦇i⦈"
          by (auto dest: xs.vrange_atD)
        from prems(2)[OF i] show "x ∈∘ 𝒟∘ (F⦇ArrVal⦈)"
          unfolding x_def arr_Set_ArrVal_vdomain .
      qed
      show "vfsequence (F⦇ArrVal⦈ ∘∘ xs)"
        by (intro vfsequence_vcomp_vsv_vfsequence vsubsetI)
          (auto intro: prems(1))
      fix i assume prems': "i ∈∘ 𝒟∘ (F⦇ArrVal⦈ ∘∘ xs)"
      moreover have "𝒟∘ (F⦇ArrVal⦈ ∘∘ xs) = 𝒟∘ xs"
        by (intro vdomain_vcomp_vsubset vsubsetI) (auto intro: prems(1))
      ultimately have i: "i ∈∘ 𝒟∘ xs" by simp
      with assms(1) prems(2)[OF i] show "(F⦇ArrVal⦈ ∘∘ xs)⦇i⦈ ∈∘ B"
        by 
          (
            cs_concl
              cs_simp: V_cs_simps cat_cs_simps 
              cs_intro: V_cs_intros cat_Set_cs_intros
          )
    qed

  qed 
    (
      auto intro: 
        vfsequences_on_in_VsetI 
        arr_Set_ArrDom_in_Vset 
        arr_Set_ArrCod_in_Vset
        cat_cs_intros
    )

qed

lemma (in 𝒵) vfsequence_map_is_monic_arr:
  assumes "F : A ↦mon⇘cat_Set α⇙ B"
  shows "vfsequence_map F : vfsequences_on A ↦mon⇘cat_Set α⇙ vfsequences_on B"
proof-
  
  note cat_Set_is_monic_arrD[OF assms]
  note FD = this cat_Set_is_arrD[OF this(1)]
  interpret F: arr_Set α F 
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+

  show ?thesis
  proof
    (
      intro cat_Set_is_monic_arrI vfsequence_map_is_arr FD(1) vsv.vsv_valeq_v11I,
      unfold cat_cs_simps;
      (elim vfsequences_onE)?
    )
  
    fix xs ys assume prems:
      "vfsequence_map F⦇ArrVal⦈⦇xs⦈ = vfsequence_map F⦇ArrVal⦈⦇ys⦈"
      "vfsequence xs"
      "⋀i. i ∈∘ 𝒟∘ xs ⟹ xs⦇i⦈ ∈∘ A"
      "vfsequence ys"
      "⋀i. i ∈∘ 𝒟∘ ys ⟹ ys⦇i⦈ ∈∘ A"

    interpret xs: vfsequence xs by (rule prems(2))
    interpret ys: vfsequence ys by (rule prems(4))

    have "xs ∈∘ vfsequences_on (F⦇ArrDom⦈)"
      unfolding cat_cs_simps by (intro vfsequences_onI prems(2,3))
    from vfsequence_map_ArrVal_app[OF this] have F_xs:
      "vfsequence_map F⦇ArrVal⦈⦇xs⦈ = F⦇ArrVal⦈ ∘∘ xs" 
      by simp
    from prems(3) have rxs: "ℛ∘ xs ⊆∘ A"
      by (intro vsubsetI) (auto dest: xs.vrange_atD)
    from xs.vfsequence_vdomain_in_omega have dxs: "𝒟∘ xs ∈∘ Vset α"
      by (auto intro!: Axiom_of_Infinity)
    note xs_is_arr = cat_Set_arr_of_vsv_is_arr
      [
        OF xs.vsv_axioms rxs,
        unfolded cat_Set_components(1), 
        OF dxs F.arr_Par_ArrDom_in_Vset
      ]

    have ys: "ys ∈∘ vfsequences_on (F⦇ArrDom⦈)"
      unfolding cat_cs_simps by (intro vfsequences_onI prems(4,5))
    from vfsequence_map_ArrVal_app[OF this] have F_ys:
      "vfsequence_map F⦇ArrVal⦈⦇ys⦈ = F⦇ArrVal⦈ ∘∘ ys" 
      by simp
    from prems(5) have rys: "ℛ∘ ys ⊆∘ A"
      by (intro vsubsetI) (auto dest: ys.vrange_atD)
    from ys.vfsequence_vdomain_in_omega have dys: "𝒟∘ ys ∈∘ Vset α"
      by (auto intro!: Axiom_of_Infinity)
    note ys_is_arr = cat_Set_arr_of_vsv_is_arr
      [
        OF ys.vsv_axioms rys,
        unfolded cat_Set_components(1), 
        OF dys F.arr_Par_ArrDom_in_Vset
      ]

    note Fxs_Fys = prems(1)[unfolded F_xs F_ys]

    from rxs have dom_rxs: "𝒟∘ (F⦇ArrVal⦈ ∘∘ xs) = 𝒟∘ xs"
      by (intro vdomain_vcomp_vsubset vsubsetI, unfold F.arr_Set_ArrVal_vdomain)
        auto
    moreover from rys have dom_rys: "𝒟∘ (F⦇ArrVal⦈ ∘∘ ys) = 𝒟∘ ys"
      by (intro vdomain_vcomp_vsubset vsubsetI, unfold F.arr_Set_ArrVal_vdomain)
        auto
    ultimately have dxs_dys: "𝒟∘ xs = 𝒟∘ ys"
      by (simp add: prems(1)[unfolded F_xs F_ys])

    from FD(1) xs_is_arr have lhs_is_arr:
      "F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv xs A : 𝒟∘ xs ↦⇘cat_Set α⇙ B"
      by (cs_concl cs_intro: cat_cs_intros)
    then have dom_lhs: 
      "𝒟∘ ((F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv xs A)⦇ArrVal⦈) = 𝒟∘ xs"
      by (simp add: cat_cs_simps)

    from FD(1) ys_is_arr have rhs_is_arr:
      "F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv ys A : 𝒟∘ xs ↦⇘cat_Set α⇙ B"
      by (cs_concl cs_simp: dxs_dys cs_intro: cat_cs_intros)
    then have dom_rhs: 
      "𝒟∘ ((F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv ys A)⦇ArrVal⦈) = 𝒟∘ xs"
      by (simp add: cat_cs_simps)

    have F_xs_F_ys:
      "F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv xs A = 
        F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv ys A"
    proof(rule arr_Set_eqI[of α])
      show
        "(F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv xs A)⦇ArrVal⦈ = 
          (F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv ys A)⦇ArrVal⦈"
      proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
        fix i assume prems: "i ∈∘ 𝒟∘ xs"
        from prems rxs have xsi: "xs⦇i⦈ ∈∘ A" 
          by (auto dest: xs.vdomain_atD)
        from prems rys have ysi: "ys⦇i⦈ ∈∘ A" 
          by (auto simp: dxs_dys dest: ys.vdomain_atD)
        from arg_cong[OF Fxs_Fys, where f=‹λx. x⦇i⦈›] prems FD(1) xsi ysi
        have "F⦇ArrVal⦈⦇xs⦇i⦈⦈ = F⦇ArrVal⦈⦇ys⦇i⦈⦈"
          by
            (
              cs_prems 
                cs_simp: V_cs_simps cat_cs_simps dxs_dys[symmetric] 
                cs_intro: V_cs_intros cat_cs_intros
            )
        with prems FD(1) xs_is_arr ys_is_arr show 
          "(F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv xs A)⦇ArrVal⦈⦇i⦈ = 
            (F ∘A⇘cat_Set α⇙ cat_Set_arr_of_vsv ys A)⦇ArrVal⦈⦇i⦈"
          by
            (
              cs_concl 
                cs_simp: cat_Set_cs_simps cat_cs_simps dxs_dys[symmetric] 
                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_cs_simps dest: cat_Set_is_arrD(1)›
      )+
    have "cat_Set_arr_of_vsv xs A = cat_Set_arr_of_vsv ys A"
      by 
        (
          rule is_monic_arrD(2)[
            OF assms(1) xs_is_arr, unfolded dxs_dys, OF ys_is_arr, OF F_xs_F_ys
            ]
        )
    from arg_cong [OF this, where f=‹λx. x⦇ArrVal⦈›, unfolded cat_Set_cs_simps]
    show "xs = ys" .

  qed (auto intro: cat_cs_intros)

qed

lemma (in 𝒵) vfsequence_map_is_epic_arr:
  assumes "F : A ↦epi⇘cat_Set α⇙ B"
  shows "vfsequence_map F : vfsequences_on A ↦epi⇘cat_Set α⇙ vfsequences_on B"
proof-

  note cat_Set_is_epic_arrD[OF assms]
  note FD = this cat_Set_is_arrD[OF this(1)]

  interpret F: arr_Set α F 
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+
  interpret SF: arr_Set α ‹vfsequence_map F›
    rewrites "vfsequence_map F⦇ArrDom⦈ = vfsequences_on A"
      and "vfsequence_map F⦇ArrCod⦈ = vfsequences_on B"
    by (intro cat_Set_is_arrD[OF vfsequence_map_is_arr[OF FD(1)]])+
  
  show ?thesis
  proof
    (
      intro cat_Set_is_epic_arrI, 
      rule vfsequence_map_is_arr[OF FD(1)], 
      rule vsubset_antisym, 
      rule SF.arr_Par_ArrVal_vrange,
      rule vsubsetI
    )
    fix xs assume prems: "xs ∈∘ vfsequences_on B"
    note xsD = vfsequences_onD[OF prems]
    interpret vfsequence xs by (rule xsD(1))
    define ys where "ys = (λi∈∘𝒟∘ xs. SOME x. x ∈∘ A ∧ xs⦇i⦈ = F⦇ArrVal⦈⦇x⦈)"
    have ys_vdomain: "𝒟∘ ys = 𝒟∘ xs" unfolding ys_def by simp
    interpret ys: vfsequence ys
      by (rule vfsequenceI)
        (auto intro: vfsequence_vdomain_in_omega simp: ys_def)
    have ysi: "ys⦇i⦈ = (SOME x. x ∈∘ A ∧ xs⦇i⦈ = F⦇ArrVal⦈⦇x⦈)"
      if "i ∈∘ 𝒟∘ xs" for i
      using that unfolding ys_def by simp
    have ysi: "ys⦇i⦈ ∈∘ A" 
      and xsi_def: "xs⦇i⦈ = F⦇ArrVal⦈⦇ys⦇i⦈⦈"
      if "i ∈∘ 𝒟∘ xs" for i
    proof-
      have "xs⦇i⦈ ∈∘ ℛ∘ (F⦇ArrVal⦈)" by (rule xsD(2)[OF that, folded FD(2)])
      then obtain x where x: "x ∈∘ A" and xsi_def: "xs⦇i⦈ = F⦇ArrVal⦈⦇x⦈"
        by (auto elim: F.ArrVal.vrange_atE simp: F.arr_Set_ArrVal_vdomain)
      show "ys⦇i⦈ ∈∘ A" and "xs⦇i⦈ = F⦇ArrVal⦈⦇ys⦇i⦈⦈"
        unfolding ysi[OF that]
        by 
          (
            all‹rule someI2_ex, intro exI conjI; (elim conjE)?›, 
            tactic‹distinct_subgoals_tac›
          )
          (auto simp: x xsi_def)
    qed
    show "xs ∈∘ ℛ∘ (vfsequence_map F⦇ArrVal⦈)"
    proof
      (
        intro vsv.vsv_vimageI2' cat_cs_intros, 
        cs_concl_step vfsequence_map_ArrVal_app, 
        unfold cat_cs_simps,
        tactic‹distinct_subgoals_tac›
      )
      show "ys ∈∘ vfsequences_on A"
        by (intro vfsequences_onI ys.vfsequence_axioms)
          (auto intro: ysi simp: ys_vdomain)
      show "xs = F⦇ArrVal⦈ ∘∘ ys"  
      proof(rule vsv_eqI)
        show "𝒟∘ xs = 𝒟∘ (F⦇ArrVal⦈ ∘∘ ys)"
          unfolding ys_vdomain[symmetric]
        proof(intro vdomain_vcomp_vsubset[symmetric] vsubsetI)
          fix y assume "y ∈∘ ℛ∘ ys"
          then obtain i where i: "i ∈∘ 𝒟∘ ys" and y_def: "y = ys⦇i⦈"
            by (auto dest: ys.vrange_atD)
          from i show "y ∈∘ 𝒟∘ (F⦇ArrVal⦈)"
            unfolding y_def F.arr_Set_ArrVal_vdomain ys_vdomain by (rule ysi)
        qed
        show "xs⦇i⦈ = (F⦇ArrVal⦈ ∘∘ ys)⦇i⦈"
          if "i ∈∘ 𝒟∘ xs" for i 
          using FD(1) that 
          by
            (
              cs_concl
                cs_simp: V_cs_simps cat_cs_simps xsi_def ys_vdomain
                cs_intro: V_cs_intros ysi
            )
      qed (auto intro: vsv_vcomp)
    qed
  qed

qed

lemma vfsequence_map_is_iso_arr:
  assumes "F : A ↦iso⇘cat_Set α⇙ B"
  shows "vfsequence_map F : vfsequences_on A ↦iso⇘cat_Set α⇙ vfsequences_on B"
proof-
  note cat_Set_is_iso_arrD[OF assms]
  note FD = this cat_Set_is_arrD[OF this(1)]
  interpret F: arr_Set α F 
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+
  interpret Set: category α ‹cat_Set α› by (cs_concl cs_intro: cat_cs_intros)
  show ?thesis
    by 
      ( 
        intro 
        F.cat_Set_is_iso_arr_if_monic_and_epic
        F.vfsequence_map_is_monic_arr[
          OF Set.cat_is_iso_arr_is_monic_arr[OF assms]
          ]
        F.vfsequence_map_is_epic_arr[
          OF Set.cat_is_iso_arr_is_epic_arr[OF assms]
          ]
      )
qed



subsection‹An injection from the range of an arrow in ‹Set› into its domain›


subsubsection‹Definition and elementary properties›

definition vrange_iso :: "V ⇒ V"
  where "vrange_iso F =
    [
      (λy∈∘ℛ∘ (F⦇ArrVal⦈). (SOME x. x ∈∘ F⦇ArrDom⦈ ∧ y = F⦇ArrVal⦈⦇x⦈)),
      ℛ∘ (F⦇ArrVal⦈),
      F⦇ArrDom⦈
    ]∘"


text‹Components.›

lemma vrange_iso_components:
  shows "vrange_iso F⦇ArrVal⦈ =
    (λy∈∘ℛ∘ (F⦇ArrVal⦈). (SOME x. x ∈∘ F⦇ArrDom⦈ ∧ y = F⦇ArrVal⦈⦇x⦈))"
    and [cat_cs_simps]: "vrange_iso F⦇ArrDom⦈ = ℛ∘ (F⦇ArrVal⦈)"
    and [cat_cs_simps]: "vrange_iso F⦇ArrCod⦈ = F⦇ArrDom⦈"
  unfolding vrange_iso_def arr_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Arrow value›

mk_VLambda vrange_iso_components(1)
  |vsv vrange_iso_ArrVal_vsv[cat_cs_intros]|
  |vdomain vrange_iso_ArrVal_vdomain[cat_cs_simps]|
  |app vrange_iso_ArrVal_app|

lemma vrange_iso_ArrVal_rules:
  assumes "F : A ↦⇘cat_Set α⇙ B" and "y ∈∘ ℛ∘ (F⦇ArrVal⦈)"
  shows "vrange_iso F⦇ArrVal⦈⦇y⦈ ∈∘ A"
    and "y = F⦇ArrVal⦈⦇vrange_iso F⦇ArrVal⦈⦇y⦈⦈"
proof-
  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret F: arr_Set α F
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+
  from assms(2) have vri_Fy_def:
    "vrange_iso F⦇ArrVal⦈⦇y⦈ = (SOME x. x ∈∘ F⦇ArrDom⦈ ∧ y = F⦇ArrVal⦈⦇x⦈)"
    by (cs_concl cs_simp: vrange_iso_ArrVal_app)
  from assms(2) F.arr_Set_ArrVal_vdomain obtain x 
    where x: "x ∈∘ A" and y_def: "y = F⦇ArrVal⦈⦇x⦈"
    by (auto elim: F.ArrVal.vrange_atE)
  show "vrange_iso F⦇ArrVal⦈⦇y⦈ ∈∘ A"
    and "y = F⦇ArrVal⦈⦇vrange_iso F⦇ArrVal⦈⦇y⦈⦈"
    unfolding vri_Fy_def cat_cs_simps 
    by (all‹rule someI2_ex; (intro exI conjI)?; (elim conjE)?›)
      (simp_all add: x y_def)
qed


subsubsection‹
An injection from the range of a function into its domain is a monic in ‹Set›
›

lemma vrange_iso_is_arr:
  assumes "F : A ↦⇘cat_Set α⇙ B"
  shows "vrange_iso F : ℛ∘ (F⦇ArrVal⦈) ↦⇘cat_Set α⇙ A"
proof-

  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret F: arr_Set α F
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+

  show "vrange_iso F : ℛ∘ (F⦇ArrVal⦈) ↦⇘cat_Set α⇙ A"
  proof(intro cat_Set_is_arrI arr_SetI, unfold cat_cs_simps)
    show "vfsequence (vrange_iso F)" 
      unfolding vrange_iso_def by (simp_all add: nat_omega_simps)
    show "vsv (vrange_iso F⦇ArrVal⦈)"
      by (cs_concl cs_intro: cat_cs_intros)
    then interpret vsv ‹vrange_iso F⦇ArrVal⦈› 
      rewrites "𝒟∘ (vrange_iso F⦇ArrVal⦈) = ℛ∘ (F⦇ArrVal⦈)"
      unfolding cat_cs_simps by simp_all
    show "vcard (vrange_iso F) = 3ℕ"
      unfolding vrange_iso_def by (simp_all add: nat_omega_simps)
    show "ℛ∘ (vrange_iso F⦇ArrVal⦈) ⊆∘ A"
    proof(intro vsubsetI)
      fix x assume "x ∈∘ ℛ∘ (vrange_iso F⦇ArrVal⦈)"
      then obtain y where y: "y ∈∘ ℛ∘ (F⦇ArrVal⦈)"
        and x_def: "x = vrange_iso F⦇ArrVal⦈⦇y⦈" 
        by (auto dest: vrange_atD)
      show "x ∈∘ A"
        unfolding x_def
        by (rule vrange_iso_ArrVal_rules(1)[OF assms y, unfolded cat_cs_simps])
    qed
  qed 
    (
      auto 
        simp: F.arr_Set_ArrDom_in_Vset 
        intro: vrange_in_VsetI F.arr_Rel_ArrVal_in_Vset
    )

qed

lemma vrange_iso_is_arr':
  assumes "F : A ↦⇘cat_Set α⇙ B" 
    and "B' = ℛ∘ (F⦇ArrVal⦈)"
    and "ℭ' = cat_Set α"
  shows "vrange_iso F : B' ↦⇘ℭ'⇙ A"
  using assms(1) unfolding assms(2,3) by (rule vrange_iso_is_arr)

lemma vrange_iso_is_monic_arr:
  assumes "F : A ↦⇘cat_Set α⇙ B"
  shows "vrange_iso F : ℛ∘ (F⦇ArrVal⦈) ↦mon⇘cat_Set α⇙ A"
proof-
  note FD = cat_Set_is_arrD[OF assms(1)]
  interpret F: arr_Set α F
    rewrites [cat_cs_simps]: "F⦇ArrDom⦈ = A" and [cat_cs_simps]: "F⦇ArrCod⦈ = B"
    by (intro FD)+
  show ?thesis
  proof
    (
      intro cat_Set_is_monic_arrI vrange_iso_is_arr, 
      rule assms, 
      rule vsv.vsv_valeq_v11I[OF vrange_iso_ArrVal_vsv], 
      unfold cat_cs_simps
    )
    fix x y assume prems:
      "x ∈∘ ℛ∘ (F⦇ArrVal⦈)"
      "y ∈∘ ℛ∘ (F⦇ArrVal⦈)"
      "vrange_iso F⦇ArrVal⦈⦇x⦈ = vrange_iso F⦇ArrVal⦈⦇y⦈"    
    show "x = y"
      by 
        (
          rule vrange_iso_ArrVal_rules(2)
            [
              OF assms prems(1), 
              unfolded prems(3), 
              folded vrange_iso_ArrVal_rules(2)[OF assms prems(2)]
            ]
        )
  qed simp
qed

lemma vrange_iso_is_monic_arr':
  assumes "F : A ↦⇘cat_Set α⇙ B"
    and "B' = ℛ∘ (F⦇ArrVal⦈)"
    and "ℭ' = cat_Set α"
  shows "vrange_iso F : B' ↦mon⇘ℭ'⇙ A"
  using assms(1) unfolding assms(2,3) by (rule vrange_iso_is_monic_arr)



subsection‹Auxiliary›


text‹
This subsection is reserved for insignificant helper lemmas 
and rules that are used in applied formalization elsewhere.
›

lemma (in 𝒵) cat_Rel_CId_is_cat_Set_arr:
  assumes "A ∈∘ cat_Rel α⦇Obj⦈"
  shows "cat_Rel α⦇CId⦈⦇A⦈ : A ↦⇘cat_Set α⇙ A"
proof-
  from assms show ?thesis
    unfolding cat_Rel_components cat_Set_components(6)[symmetric]
    by 
      (
        cs_concl cs_shallow 
          cs_simp: cat_Set_components(1) cs_intro: cat_cs_intros
      )
qed

lemma (in 𝒵) cat_Rel_CId_is_cat_Set_arr'[cat_rel_par_Set_cs_intros]:
  assumes "A ∈∘ cat_Rel α⦇Obj⦈" 
    and "B' = A"
    and "C' = A"
    and "ℭ' = cat_Set α"
  shows "cat_Rel α⦇CId⦈⦇A⦈ : B' ↦⇘ℭ'⇙ C'"
  using assms(1) unfolding assms(2-4) by (rule cat_Rel_CId_is_cat_Set_arr)

text‹\newpage›

end