Theory CZH_ECAT_Parallel

(* Copyright 2021 (C) Mihails Milehins *)

section‹Categories with parallel arrows between two objects›
theory CZH_ECAT_Parallel
  imports CZH_ECAT_Small_Functor
begin



subsection‹Background: category with parallel arrows between two objects›

named_theorems cat_parallel_cs_simps
named_theorems cat_parallel_cs_intros

definition 𝔞⇩P⇩L :: "V ⇒ V" where "𝔞⇩P⇩L F = set {F, 0}"
definition 𝔟⇩P⇩L :: "V ⇒ V" where "𝔟⇩P⇩L F = set {F, 1⇩ℕ}"

lemma cat_PL_𝔞_nin_F[cat_parallel_cs_intros]: "𝔞⇩P⇩L F ∉⇩∘ F" 
  unfolding 𝔞⇩P⇩L_def using mem_not_sym by auto

lemma cat_PL_𝔟_nin_F[cat_parallel_cs_intros]: "𝔟⇩P⇩L F ∉⇩∘ F"
  unfolding 𝔟⇩P⇩L_def using mem_not_sym by auto

lemma cat_PL_𝔞𝔟[cat_parallel_cs_intros]: "𝔞⇩P⇩L F ≠ 𝔟⇩P⇩L F"
  unfolding 𝔞⇩P⇩L_def 𝔟⇩P⇩L_def by (simp add: Set.doubleton_eq_iff)

lemmas cat_PL_𝔟𝔞[cat_parallel_cs_intros] = cat_PL_𝔞𝔟[symmetric]



subsection‹
Composable arrows for a category with parallel arrows between two objects
›

definition cat_parallel_composable :: "V ⇒ V ⇒ V ⇒ V"
  where "cat_parallel_composable 𝔞 𝔟 F ≡
    set {[𝔞, 𝔞]⇩∘, [𝔟, 𝔟]⇩∘} ∪⇩∘
    (F ×⇩∙ set {𝔞}) ∪⇩∘
    (set {𝔟} ×⇩∙ F)"


text‹Rules.›

lemma cat_parallel_composable_𝔞𝔞[cat_parallel_cs_intros]:
  assumes "g = 𝔞" and "f = 𝔞"
  shows "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
  unfolding assms cat_parallel_composable_def by auto

lemma cat_parallel_composable_𝔟𝔣[cat_parallel_cs_intros]:
  assumes "g = 𝔟" and "f ∈⇩∘ F"
  shows "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
  using assms(2) unfolding assms(1) cat_parallel_composable_def by auto

lemma cat_parallel_composable_𝔣𝔞[cat_parallel_cs_intros]:
  assumes "g ∈⇩∘ F" and "f = 𝔞" 
  shows "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
  using assms(1) unfolding assms(2) cat_parallel_composable_def by auto

lemma cat_parallel_composable_𝔟𝔟[cat_parallel_cs_intros]:
  assumes "g = 𝔟" and "f = 𝔟"
  shows "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
  unfolding assms cat_parallel_composable_def by auto

lemma cat_parallel_composableE:
  assumes "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
  obtains "g = 𝔟" and "f = 𝔟"
        | "g = 𝔟" and "f ∈⇩∘ F" 
        | "g ∈⇩∘ F" and "f = 𝔞"
        | "g = 𝔞" and "f = 𝔞"
  using assms that unfolding cat_parallel_composable_def by auto


text‹Elementary properties.›

lemma cat_parallel_composable_fconverse: 
  "(cat_parallel_composable 𝔞 𝔟 F)¯⇩∙ = cat_parallel_composable 𝔟 𝔞 F"
  unfolding cat_parallel_composable_def by auto



subsection‹
Local assumptions for a category with parallel arrows between two objects
›

locale cat_parallel = 𝒵 α for α +  
  fixes 𝔞 𝔟 F
  assumes cat_parallel_𝔞𝔟[cat_parallel_cs_intros]: "𝔞 ≠ 𝔟"
    and cat_parallel_𝔞F[cat_parallel_cs_intros]: "𝔞 ∉⇩∘ F"
    and cat_parallel_𝔟F[cat_parallel_cs_intros]: "𝔟 ∉⇩∘ F"
    and cat_parallel_𝔞_in_Vset[cat_parallel_cs_intros]: "𝔞 ∈⇩∘ Vset α"
    and cat_parallel_𝔟_in_Vset[cat_parallel_cs_intros]: "𝔟 ∈⇩∘ Vset α"
    and cat_parallel_F_in_Vset[cat_parallel_cs_intros]: "F ∈⇩∘ Vset α"

lemmas (in cat_parallel) cat_parallel_ineq =
  cat_parallel_𝔞𝔟
  cat_parallel_𝔞F
  cat_parallel_𝔟F


text‹Rules.›

lemmas (in cat_parallel) [cat_parallel_cs_intros] = cat_parallel_axioms

mk_ide rf cat_parallel_def[unfolded cat_parallel_axioms_def]
  |intro cat_parallelI|
  |dest cat_parallelD[dest]|
  |elim cat_parallelE[elim]|


text‹Duality.›

lemma (in cat_parallel) cat_parallel_op[cat_op_intros]: 
  "cat_parallel α 𝔟 𝔞 F"
  by (intro cat_parallelI) 
    (auto intro!: cat_parallel_cs_intros cat_parallel_𝔞𝔟[symmetric])


text‹Elementary properties.›

lemma (in 𝒵) cat_parallel_PL: 
  assumes "F ∈⇩∘ Vset α"
  shows "cat_parallel α (𝔞⇩P⇩L F) (𝔟⇩P⇩L F) F"
proof (rule cat_parallelI)
  show "𝔞⇩P⇩L F ∈⇩∘ Vset α"
    unfolding 𝔞⇩P⇩L_def by (intro Limit_vdoubleton_in_VsetI assms) auto
  show "𝔟⇩P⇩L F ∈⇩∘ Vset α"
    unfolding 𝔟⇩P⇩L_def
    by (intro Limit_vdoubleton_in_VsetI ord_of_nat_in_Vset assms) simp
qed (auto simp: assms cat_PL_𝔞𝔟 cat_PL_𝔞_nin_F cat_PL_𝔟_nin_F)



subsection‹‹⇑›: category with parallel arrows between two objects›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-2 and Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›

definition the_cat_parallel :: "V ⇒ V ⇒ V ⇒ V" (‹⇑⇩C›)
  where "⇑⇩C 𝔞 𝔟 F =
    [
      set {𝔞, 𝔟},
      set {𝔞, 𝔟} ∪⇩∘ F,
      (λx∈⇩∘set {𝔞, 𝔟} ∪⇩∘ F. (x = 𝔟 ? 𝔟 : 𝔞)),
      (λx∈⇩∘set {𝔞, 𝔟} ∪⇩∘ F. (x = 𝔞 ? 𝔞 : 𝔟)),
      (
        λgf∈⇩∘cat_parallel_composable 𝔞 𝔟 F.
         if gf = [𝔟, 𝔟]⇩∘ ⇒ 𝔟
          | ∃f. gf = [𝔟, f]⇩∘ ⇒ gf⦇1⇩ℕ⦈
          | ∃f. gf = [f, 𝔞]⇩∘ ⇒ gf⦇0⦈
          | otherwise ⇒ 𝔞
      ),
      vid_on (set {𝔞, 𝔟})
    ]⇩∘"


text‹Components.›

lemma the_cat_parallel_components: 
  shows "⇑⇩C 𝔞 𝔟 F⦇Obj⦈ = set {𝔞, 𝔟}"
    and "⇑⇩C 𝔞 𝔟 F⦇Arr⦈ = set {𝔞, 𝔟} ∪⇩∘ F"
    and "⇑⇩C 𝔞 𝔟 F⦇Dom⦈ = (λx∈⇩∘set {𝔞, 𝔟} ∪⇩∘ F. (x = 𝔟 ? 𝔟 : 𝔞))"
    and "⇑⇩C 𝔞 𝔟 F⦇Cod⦈ = (λx∈⇩∘set {𝔞, 𝔟} ∪⇩∘ F. (x = 𝔞 ? 𝔞 : 𝔟))"
    and "⇑⇩C 𝔞 𝔟 F⦇Comp⦈ =
      (
        λgf∈⇩∘cat_parallel_composable 𝔞 𝔟 F.
         if gf = [𝔟, 𝔟]⇩∘ ⇒ 𝔟
          | ∃f. gf = [𝔟, f]⇩∘ ⇒ gf⦇1⇩ℕ⦈
          | ∃f. gf = [f, 𝔞]⇩∘ ⇒ gf⦇0⦈
          | otherwise ⇒ 𝔞
      )"
    and "⇑⇩C 𝔞 𝔟 F⦇CId⦈ = vid_on (set {𝔞, 𝔟})"
  unfolding the_cat_parallel_def dg_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Objects›

lemma the_cat_parallel_Obj_𝔞I[cat_parallel_cs_intros]:
  assumes "a = 𝔞"
  shows "a ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈"
  using assms unfolding the_cat_parallel_components by simp

lemma the_cat_parallel_Obj_𝔟I[cat_parallel_cs_intros]:
  assumes "a = 𝔟"
  shows "a ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈"
  using assms unfolding the_cat_parallel_components by simp

lemma the_cat_parallel_ObjE:
  assumes "a ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈"
  obtains "a = 𝔞" | "a = 𝔟" 
  using assms unfolding the_cat_parallel_components(1) by fastforce


subsubsection‹Arrows›

lemma the_cat_parallel_Arr_𝔞I[cat_parallel_cs_intros]:
  assumes "f = 𝔞"  
  shows "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
  using assms unfolding the_cat_parallel_components by simp

lemma the_cat_parallel_Arr_𝔟I[cat_parallel_cs_intros]:
  assumes "f = 𝔟"  
  shows "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
  using assms unfolding the_cat_parallel_components by simp

lemma the_cat_parallel_Arr_FI[cat_parallel_cs_intros]:
  assumes "f ∈⇩∘ F"
  shows "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
  using assms unfolding the_cat_parallel_components by simp

lemma the_cat_parallel_ArrE:
  assumes "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
  obtains "f = 𝔞" | "f = 𝔟" | "f ∈⇩∘ F"  
  using assms that unfolding the_cat_parallel_components by auto


subsubsection‹Domain›

mk_VLambda the_cat_parallel_components(3)
  |vsv the_cat_parallel_Dom_vsv[cat_parallel_cs_intros]|
  |vdomain the_cat_parallel_Dom_vdomain[cat_parallel_cs_simps]|

lemma (in cat_parallel) the_cat_parallel_Dom_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇f⦈ = 𝔟"
  unfolding the_cat_parallel_components assms by simp

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Dom_app_𝔟

lemma (in cat_parallel) the_cat_parallel_Dom_app_F[cat_parallel_cs_simps]:
  assumes "f ∈⇩∘ F"
  shows "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇f⦈ = 𝔞"
  unfolding the_cat_parallel_components using assms cat_parallel_ineq by auto

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Dom_app_F

lemma (in cat_parallel) the_cat_parallel_Dom_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇f⦈ = 𝔞"
  unfolding the_cat_parallel_components assms by auto

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Dom_app_𝔞


subsubsection‹Codomain›

mk_VLambda the_cat_parallel_components(4)
  |vsv the_cat_parallel_Cod_vsv[cat_parallel_cs_intros]|
  |vdomain the_cat_parallel_Cod_vdomain[cat_parallel_cs_simps]|

lemma (in cat_parallel) the_cat_parallel_Cod_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇f⦈ = 𝔟"
  unfolding the_cat_parallel_components assms by simp

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Cod_app_𝔟

lemma (in cat_parallel) the_cat_parallel_Cod_app_F[cat_parallel_cs_simps]:
  assumes "f ∈⇩∘ F"
  shows "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇f⦈ = 𝔟"
  unfolding the_cat_parallel_components using assms cat_parallel_ineq by auto

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Cod_app_F

lemma (in cat_parallel) the_cat_parallel_Cod_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇f⦈ = 𝔞"
  unfolding the_cat_parallel_components assms by auto

lemmas [cat_parallel_cs_simps] = cat_parallel.the_cat_parallel_Cod_app_𝔞


subsubsection‹Composition›

mk_VLambda the_cat_parallel_components(5)
  |vsv the_cat_parallel_Comp_vsv[cat_parallel_cs_intros]|
  |vdomain the_cat_parallel_Comp_vdomain[cat_parallel_cs_simps]|
  |app the_cat_parallel_Comp_app[cat_parallel_cs_simps]|

lemma the_cat_parallel_Comp_app_𝔟𝔟[cat_parallel_cs_simps]:
  assumes "g = 𝔟" and "f = 𝔟"
  shows "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g" "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
    by (cs_concl cs_shallow cs_intro: cat_parallel_cs_intros)
  then show "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g" "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f"
    unfolding the_cat_parallel_components(5) assms 
    by (auto simp: nat_omega_simps)
qed

lemma the_cat_parallel_Comp_app_𝔞𝔞[cat_parallel_cs_simps]:
  assumes "g = 𝔞" and "f = 𝔞"
  shows "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g" "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f"
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
    by (cs_concl cs_intro: cat_parallel_cs_intros)
  then show "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g" "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f"
    unfolding the_cat_parallel_components(5) assms 
    by (auto simp: nat_omega_simps)
qed

lemma the_cat_parallel_Comp_app_𝔟F[cat_parallel_cs_simps]:
  assumes "g = 𝔟" and "f ∈⇩∘ F"
  shows "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
    by (cs_concl cs_intro: cat_parallel_cs_intros)
  then show "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f"
    unfolding the_cat_parallel_components(5) assms 
    by (auto simp: nat_omega_simps)
qed

lemma (in cat_parallel) the_cat_parallel_Comp_app_F𝔞[cat_parallel_cs_simps]:
  assumes "g ∈⇩∘ F" and "f = 𝔞"
  shows "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g" 
proof-
  from assms have "[g, f]⇩∘ ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
    by (cs_concl cs_intro: cat_parallel_cs_intros)
  then show "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = g"
    unfolding the_cat_parallel_components(5)  
    using assms cat_parallel_ineq
    by (auto simp: nat_omega_simps)
qed


subsubsection‹Identity›

mk_VLambda the_cat_parallel_components(6)[unfolded VLambda_vid_on[symmetric]]
  |vsv the_cat_parallel_CId_vsv[cat_parallel_cs_intros]|
  |vdomain the_cat_parallel_CId_vdomain[cat_parallel_cs_simps]|
  |app the_cat_parallel_CId_app|

lemma the_cat_parallel_CId_app_𝔞[cat_parallel_cs_simps]: 
  assumes "a = 𝔞"
  shows "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇a⦈ = 𝔞"
  unfolding assms by (auto simp: the_cat_parallel_CId_app)

lemma the_cat_parallel_CId_app_𝔟[cat_parallel_cs_simps]: 
  assumes "a = 𝔟"
  shows "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇a⦈ = 𝔟"
  unfolding assms by (auto simp: the_cat_parallel_CId_app)


subsubsection‹Arrow with a domain and a codomain›

lemma (in cat_parallel) the_cat_parallel_is_arr_𝔞𝔞𝔞[cat_parallel_cs_intros]:
  assumes "a' = 𝔞" and "b' = 𝔞" and "f = 𝔞"
  shows "f : a' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b'"
proof(intro is_arrI, unfold assms)
  show "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇𝔞⦈ = 𝔞" "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇𝔞⦈ = 𝔞"
    by (cs_concl cs_shallow cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros)+
qed (auto simp: the_cat_parallel_components)

lemma (in cat_parallel) the_cat_parallel_is_arr_𝔟𝔟𝔟[cat_parallel_cs_intros]:
  assumes "a' = 𝔟" and "b' = 𝔟" and "f = 𝔟"
  shows "f : a' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b'"
proof(intro is_arrI, unfold assms)
  show "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇𝔟⦈ = 𝔟" "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇𝔟⦈ = 𝔟"
    by (cs_concl cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros)+
qed (auto simp: the_cat_parallel_components)

lemma (in cat_parallel) the_cat_parallel_is_arr_𝔞𝔟F[cat_parallel_cs_intros]:
  assumes "a' = 𝔞" and "b' = 𝔟" and "f ∈⇩∘ F"
  shows "f : a' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b'"
proof(intro is_arrI, unfold assms(1,2))
  from assms(3) show "⇑⇩C 𝔞 𝔟 F⦇Dom⦈⦇f⦈ = 𝔞" "⇑⇩C 𝔞 𝔟 F⦇Cod⦈⦇f⦈ = 𝔟"
    by (cs_concl cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros)+
qed (auto simp: the_cat_parallel_components assms(3))

lemma (in cat_parallel) the_cat_parallel_is_arrE:
  assumes "f' : a' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b'"
  obtains "a' = 𝔞" and "b' = 𝔞" and "f' = 𝔞"
        | "a' = 𝔟" and "b' = 𝔟" and "f' = 𝔟"
        | "a' = 𝔞" and "b' = 𝔟" and "f' ∈⇩∘ F"
proof-
  note f = is_arrD[OF assms]
  from f(1) consider (𝔞) ‹f' = 𝔞› | (𝔟) ‹f' = 𝔟› | (F) ‹f' ∈⇩∘ F› 
    unfolding the_cat_parallel_components(2) by auto
  then show ?thesis
  proof cases
    case 𝔞
    moreover from f(2)[unfolded 𝔞, symmetric] have "a' = 𝔞"
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros
        )
    moreover from f(3)[unfolded 𝔞, symmetric] have "b' = 𝔞"
      by 
        (
          cs_prems cs_shallow
            cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros
        )
    ultimately show ?thesis using that by auto
  next
    case 𝔟
    moreover from f(2)[unfolded 𝔟, symmetric] have "a' = 𝔟"
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros
        )
    moreover from f(3)[unfolded 𝔟, symmetric] have "b' = 𝔟"
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros
        )
    ultimately show ?thesis using that by auto
  next
    case F
    moreover from f(2)[symmetric] F have "a' = 𝔞"
      by 
        (
          cs_prems cs_shallow 
            cs_simp: cat_parallel_cs_simps cs_intro: V_cs_intros
        )
    moreover from f(3)[symmetric] F have "b' = 𝔟"
      by (cs_prems cs_shallow cs_simp: cat_parallel_cs_simps)
    ultimately show ?thesis using that by auto
  qed
qed


subsubsection‹‹⇑› is a category›

lemma (in cat_parallel) tiny_category_the_cat_parallel[cat_parallel_cs_intros]:
  "tiny_category α (⇑⇩C 𝔞 𝔟 F)"
proof(intro tiny_categoryI'')
  show "vfsequence (⇑⇩C 𝔞 𝔟 F)" unfolding the_cat_parallel_def by simp
  show "vcard (⇑⇩C 𝔞 𝔟 F) = 6⇩ℕ"
    unfolding the_cat_parallel_def by (simp_all add: nat_omega_simps)
  show "ℛ⇩∘ (⇑⇩C 𝔞 𝔟 F⦇Dom⦈) ⊆⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈" 
    by (auto simp: the_cat_parallel_components)
  show "ℛ⇩∘ (⇑⇩C 𝔞 𝔟 F⦇Cod⦈) ⊆⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈" 
    by (auto simp: the_cat_parallel_components)
  show "(gf ∈⇩∘ 𝒟⇩∘ (⇑⇩C 𝔞 𝔟 F⦇Comp⦈)) =
    (∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c ∧ f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b)"
    for gf
    unfolding the_cat_parallel_Comp_vdomain
  proof
    assume prems: "gf ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
    then obtain g f where gf_def: "gf = [g, f]⇩∘" 
      unfolding cat_parallel_composable_def by auto
    from prems show 
      "∃g f b c a. gf = [g, f]⇩∘ ∧ g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c ∧ f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b"
      unfolding gf_def
      by (*slow*)
        (
          cases rule: cat_parallel_composableE; 
          (intro exI conjI)?; 
          cs_concl_step?;
          (simp only:)?,
          all‹intro is_arrI, unfold the_cat_parallel_components(2)›
        )
        (
          cs_concl 
            cs_simp: cat_parallel_cs_simps V_cs_simps cs_intro: V_cs_intros
        )+
  next
    assume 
      "∃g f b' c' a'. 
        gf = [g, f]⇩∘ ∧ g : b' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c' ∧ f : a' ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b'"
    then obtain g f b c a 
      where gf_def: "gf = [g, f]⇩∘" 
        and g: "g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c"
        and f: "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b" 
      by clarsimp
    from g f show "gf ∈⇩∘ cat_parallel_composable 𝔞 𝔟 F"
      unfolding gf_def 
      by (elim the_cat_parallel_is_arrE) (auto simp: cat_parallel_cs_intros)
  qed
  show "𝒟⇩∘ (⇑⇩C 𝔞 𝔟 F⦇CId⦈) = ⇑⇩C 𝔞 𝔟 F⦇Obj⦈"
    by (simp add: cat_parallel_cs_simps the_cat_parallel_components)
  show "g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c"
    if "g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c" and "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b" for b c g a f
    using that
    by (elim the_cat_parallel_is_arrE; simp only:)
      (
        all‹
          solves‹simp add: cat_parallel_𝔞𝔟[symmetric]› |
          cs_concl cs_simp: cat_parallel_cs_simps 
        ›
      )
  show 
    "h ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = 
      h ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ (g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f)"
    if "h : c ↦⇘⇑⇩C 𝔞 𝔟 F⇙ d" 
      and "g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c" 
      and "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b"
    for c d h b g a f
    using that 
    by (elim the_cat_parallel_is_arrE; simp only:) (*slow*)
      (
        all‹
          solves‹simp only: cat_parallel_ineq cat_parallel_𝔞𝔟[symmetric]› |
          cs_concl 
            cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros
          ›
      )
  show "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇a⦈ : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ a" if "a ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈" 
    for a
  proof-
    from that consider ‹a = 𝔞› | ‹a = 𝔟›
      unfolding the_cat_parallel_components(1) by auto
    then show "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇a⦈ : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ a"
      by cases
        (
          cs_concl 
            cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros
        )+
  qed
  show "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇b⦈ ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f = f" 
    if "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b" for a b f
    using that
    by (elim the_cat_parallel_is_arrE)
      (cs_concl cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros)
  show "f ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ ⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇b⦈ = f" 
    if "f : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c" for b c f
    using that
    by (elim the_cat_parallel_is_arrE)
      (cs_concl cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros)
  show "⇑⇩C 𝔞 𝔟 F⦇Obj⦈ ∈⇩∘ Vset α"
    by 
      (
        cs_concl cs_shallow
          cs_simp: the_cat_parallel_components nat_omega_simps 
          cs_intro: V_cs_intros cat_parallel_cs_intros
      )
qed 
  (
    cs_concl  
      cs_simp: 
        nat_omega_simps cat_parallel_cs_simps the_cat_parallel_components(2) 
      cs_intro: 
        cat_cs_intros 
        cat_parallel_cs_intros 
        V_cs_intros 
        Limit_succ_in_VsetI
  )+

lemmas [cat_parallel_cs_intros] = cat_parallel.tiny_category_the_cat_parallel


subsubsection‹Opposite parallel category›

lemma (in cat_parallel) op_cat_the_cat_parallel[cat_op_simps]: 
  "op_cat (⇑⇩C 𝔞 𝔟 F) = ⇑⇩C 𝔟 𝔞 F"
proof(rule cat_eqI)
  interpret par: cat_parallel α 𝔟 𝔞 F by (rule cat_parallel_op) 
  show 𝔟𝔞: "category α (⇑⇩C 𝔟 𝔞 F)"
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_parallel_cs_intros)
  show 𝔞𝔟: "category α (op_cat (⇑⇩C 𝔞 𝔟 F))" 
    by 
      (
        cs_concl cs_shallow 
          cs_intro: cat_small_cs_intros cat_op_intros cat_parallel_cs_intros
      )
  interpret 𝔟𝔞: category α ‹⇑⇩C 𝔟 𝔞 F› by (rule 𝔟𝔞)
  interpret 𝔞𝔟: category α ‹⇑⇩C 𝔞 𝔟 F›
    by (cs_concl cs_shallow cs_intro: cat_small_cs_intros cat_parallel_cs_intros)
  show "op_cat (⇑⇩C 𝔞 𝔟 F)⦇Comp⦈ = ⇑⇩C 𝔟 𝔞 F⦇Comp⦈"
  proof(rule vsv_eqI)
    show "vsv (op_cat (⇑⇩C 𝔞 𝔟 F)⦇Comp⦈)"
      unfolding op_cat_components by (rule fflip_vsv)
    show "vsv (⇑⇩C 𝔟 𝔞 F⦇Comp⦈)"
      by (cs_concl cs_shallow cs_intro: cat_parallel_cs_intros)
    show [cat_op_simps]: "𝒟⇩∘ (op_cat (⇑⇩C 𝔞 𝔟 F)⦇Comp⦈) = 𝒟⇩∘ (⇑⇩C 𝔟 𝔞 F⦇Comp⦈)"
      by 
        (
          cs_concl cs_shallow
            cs_simp: 
              cat_parallel_composable_fconverse
              op_cat_components(5) 
              vdomain_fflip 
              cat_parallel_cs_simps 
            cs_intro: cat_cs_intros
        )
    fix gf assume "gf ∈⇩∘ 𝒟⇩∘ (op_cat (⇑⇩C 𝔞 𝔟 F)⦇Comp⦈)"
    then have "gf ∈⇩∘ 𝒟⇩∘ (⇑⇩C 𝔟 𝔞 F⦇Comp⦈)" unfolding cat_op_simps by simp
    then obtain g f a b c 
      where gf_def: "gf = [g, f]⇩∘" 
        and g: "g : b ↦⇘⇑⇩C 𝔟 𝔞 F⇙ c"
        and f: "f : a ↦⇘⇑⇩C 𝔟 𝔞 F⇙ b"
      by auto
    from g f show "op_cat (⇑⇩C 𝔞 𝔟 F)⦇Comp⦈⦇gf⦈ = ⇑⇩C 𝔟 𝔞 F⦇Comp⦈⦇gf⦈"
      unfolding gf_def
      by (elim par.the_cat_parallel_is_arrE)
        (
          simp add: cat_parallel_cs_intros | 
          cs_concl 
            cs_simp: cat_op_simps cat_parallel_cs_simps 
            cs_intro: cat_cs_intros cat_parallel_cs_intros
        )+
  qed
  show "op_cat (⇑⇩C 𝔞 𝔟 F)⦇CId⦈ = ⇑⇩C 𝔟 𝔞 F⦇CId⦈"
  proof(unfold cat_op_simps, rule vsv_eqI, unfold cat_parallel_cs_simps)  
    fix a assume "a ∈⇩∘ set {𝔞, 𝔟}"
    then consider ‹a = 𝔞› | ‹a = 𝔟› by auto
    then show "⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇a⦈ = ⇑⇩C 𝔟 𝔞 F⦇CId⦈⦇a⦈"
      by cases (cs_concl cs_simp: cat_parallel_cs_simps)+
  qed auto
qed (auto simp: the_cat_parallel_components op_cat_components)

lemmas [cat_op_simps] = cat_parallel.op_cat_the_cat_parallel



subsection‹Parallel functor›


subsubsection‹Background›


text‹
See Chapter III-3 and Chapter III-4 in \<^cite>‹"mac_lane_categories_2010"›).
›


subsubsection‹Local assumptions for the parallel functor›

locale cf_parallel = cat_parallel α 𝔞 𝔟 F + category α ℭ + F': vsv F'
  for α 𝔞 𝔟 F 𝔞' 𝔟' F' ℭ :: V +
  assumes cf_parallel_F'_vdomain[cat_parallel_cs_simps]: "𝒟⇩∘ F' = F"
    and cf_parallel_F'[cat_parallel_cs_intros]: "𝔣 ∈⇩∘ F ⟹ F'⦇𝔣⦈ : 𝔞' ↦⇘ℭ⇙ 𝔟'"
    and cf_parallel_𝔞'[cat_parallel_cs_intros]: "𝔞' ∈⇩∘ ℭ⦇Obj⦈"
    and cf_parallel_𝔟'[cat_parallel_cs_intros]: "𝔟' ∈⇩∘ ℭ⦇Obj⦈"

lemmas (in cf_parallel) [cat_parallel_cs_intros] = F'.vsv_axioms 

lemma (in cf_parallel) cf_parallel_F''[cat_parallel_cs_intros]:
  assumes "𝔣 ∈⇩∘ F" and "a = 𝔞'" and "b = 𝔟'"
  shows "F'⦇𝔣⦈ : a ↦⇘ℭ⇙ b"
  using assms(1) unfolding assms(2-3) by (rule cf_parallel_F')

lemma (in cf_parallel) cf_parallel_F'''[cat_parallel_cs_intros]:
  assumes "𝔣 ∈⇩∘ F" and "f = F'⦇𝔣⦈" and "b = 𝔟'"
  shows "f : 𝔞' ↦⇘ℭ⇙ b"
  using assms(1) unfolding assms(2-3) by (rule cf_parallel_F')

lemma (in cf_parallel) cf_parallel_F''''[cat_parallel_cs_intros]:
  assumes "𝔣 ∈⇩∘ F" and "f = F'⦇𝔣⦈" and "a = 𝔞'"
  shows "f : a ↦⇘ℭ⇙ 𝔟'"
  using assms(1) unfolding assms(2,3) by (rule cf_parallel_F')


text‹Rules.›

lemma (in cf_parallel) cf_parallel_axioms'[cat_parallel_cs_intros]:
  assumes "α' = α" 
    and "a'' = 𝔞" 
    and "b'' = 𝔟" 
    and "F'' = F" 
    and "a''' = 𝔞'" 
    and "b''' = 𝔟'" 
    and "F''' = F'" 
  shows "cf_parallel α' a'' b'' F'' a''' b''' F''' ℭ"
  unfolding assms by (rule cf_parallel_axioms)

mk_ide rf cf_parallel_def[unfolded cf_parallel_axioms_def]
  |intro cf_parallelI|
  |dest cf_parallelD[dest]|
  |elim cf_parallelE[elim]|

lemmas [cat_parallel_cs_intros] = cf_parallelD(1,2)


text‹Duality.›

lemma (in cf_parallel) cf_parallel_op[cat_op_intros]: 
  "cf_parallel α 𝔟 𝔞 F 𝔟' 𝔞' F' (op_cat ℭ)"
  by (intro cf_parallelI, unfold cat_op_simps insert_commute) 
    (
      cs_concl 
        cs_simp: cat_parallel_cs_simps  
        cs_intro: cat_parallel_cs_intros cat_cs_intros cat_op_intros
    )+

lemmas [cat_op_intros] = cf_parallel.cf_parallel_op


subsubsection‹Definition and elementary properties›

definition the_cf_parallel :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V" 
  (‹⇑→⇑⇩C⇩F›)
  where "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F' =
    [
      (λa∈⇩∘⇑⇩C 𝔞 𝔟 F⦇Obj⦈. (a = 𝔞 ? 𝔞' : 𝔟')),
      (
        λf∈⇩∘⇑⇩C 𝔞 𝔟 F⦇Arr⦈.
          (
           if f = 𝔞 ⇒ ℭ⦇CId⦈⦇𝔞'⦈
            | f = 𝔟 ⇒ ℭ⦇CId⦈⦇𝔟'⦈
            | otherwise ⇒ F'⦇f⦈ 
          )
      ),
      ⇑⇩C 𝔞 𝔟 F,
      ℭ
    ]⇩∘"


text‹Components.›

lemma the_cf_parallel_components:
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈ =
      (λa∈⇩∘⇑⇩C 𝔞 𝔟 F⦇Obj⦈. (a = 𝔞 ? 𝔞' : 𝔟'))"
    and "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈ =
      (
        λf∈⇩∘⇑⇩C 𝔞 𝔟 F⦇Arr⦈.
          (
           if f = 𝔞 ⇒ ℭ⦇CId⦈⦇𝔞'⦈
            | f = 𝔟 ⇒ ℭ⦇CId⦈⦇𝔟'⦈
            | otherwise ⇒ F'⦇f⦈ 
          )
      )"
    and [cat_parallel_cs_simps]: "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇HomDom⦈ = ⇑⇩C 𝔞 𝔟 F"
    and [cat_parallel_cs_simps]: "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇HomCod⦈ = ℭ"
  unfolding the_cf_parallel_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda the_cf_parallel_components(1)
  |vsv the_cf_parallel_ObjMap_vsv[cat_parallel_cs_intros]|
  |vdomain the_cf_parallel_ObjMap_vdomain[cat_parallel_cs_simps]|
  |app the_cf_parallel_ObjMap_app|

lemma (in cf_parallel) the_cf_parallel_ObjMap_app_𝔞[cat_parallel_cs_simps]:
  assumes "x = 𝔞"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇x⦈ = 𝔞'"
  by 
    (
      cs_concl 
        cs_simp: 
          assms the_cf_parallel_ObjMap_app cat_parallel_cs_simps V_cs_simps 
        cs_intro: cat_parallel_cs_intros
    )

lemmas [cat_parallel_cs_simps] = cf_parallel.the_cf_parallel_ObjMap_app_𝔞

lemma (in cf_parallel) the_cf_parallel_ObjMap_app_𝔟[cat_parallel_cs_simps]:
  assumes "x = 𝔟"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇x⦈ = 𝔟'"
  using cat_parallel_ineq
  by 
    (
      cs_concl 
        cs_simp: 
          assms the_cf_parallel_ObjMap_app cat_parallel_cs_simps V_cs_simps 
        cs_intro: cat_parallel_cs_intros
    )

lemmas [cat_parallel_cs_simps] = cf_parallel.the_cf_parallel_ObjMap_app_𝔟

lemma (in cf_parallel) the_cf_parallel_ObjMap_vrange:
  "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈) = set {𝔞', 𝔟'}"
proof(intro vsubset_antisym)
  show "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈) ⊆⇩∘ set {𝔞', 𝔟'}"
    unfolding the_cf_parallel_components
    by (intro vrange_VLambda_vsubset)
      (simp_all add: cat_parallel_𝔞𝔟 cf_parallel_𝔞' cf_parallel_𝔟')
  show "set {𝔞', 𝔟'} ⊆⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈)"
  proof(rule vsubsetI)
    fix x assume prems: "x ∈⇩∘ set {𝔞', 𝔟'}"
    from prems consider ‹x = 𝔞'› | ‹x = 𝔟'› by auto
    moreover have "𝔞' ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈)"
      by (rule vsv.vsv_vimageI2'[of _ _ 𝔞])
        (
          cs_concl 
            cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros 
        )
    moreover have "𝔟' ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈)"
      by (rule vsv.vsv_vimageI2'[of _ _ 𝔟])
        (
          cs_concl 
            cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros 
        )
    ultimately show "x ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈)" by auto
  qed
qed

lemma (in cf_parallel) the_cf_parallel_ObjMap_vrange_vsubset_Obj:
  "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
  unfolding the_cf_parallel_components
  by (intro vrange_VLambda_vsubset)
    (simp_all add: cat_parallel_𝔞𝔟 cf_parallel_𝔞' cf_parallel_𝔟')


subsubsection‹Arrow map›

mk_VLambda the_cf_parallel_components(2)
  |vsv the_cf_parallel_ArrMap_vsv[cat_parallel_cs_intros]|
  |vdomain the_cf_parallel_ArrMap_vdomain[cat_parallel_cs_simps]|
  |app the_cf_parallel_ArrMap_app|

lemma (in cf_parallel) the_cf_parallel_ArrMap_app_F[cat_parallel_cs_simps]:
  assumes "f ∈⇩∘ F"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ = F'⦇f⦈"
proof-
  from assms have "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
    by (cs_concl cs_shallow cs_intro: cat_parallel_cs_intros a_in_succ_xI)
  from assms this show ?thesis
    using cat_parallel_ineq 
    by (auto simp: the_cf_parallel_ArrMap_app cat_parallel_cs_simps)
qed

lemmas [cat_parallel_cs_simps] = cf_parallel.the_cf_parallel_ArrMap_app_F

lemma (in cf_parallel) the_cf_parallel_ArrMap_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔞'⦈"
proof-
  from assms have "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
    by (cs_concl cs_intro: cat_parallel_cs_intros a_in_succ_xI)
  from this show ?thesis
    using cat_parallel_ineq
    by (elim the_cat_parallel_ArrE; simp only: assms) 
      (auto simp: the_cf_parallel_ArrMap_app)
qed

lemmas [cat_parallel_cs_simps] = cf_parallel.the_cf_parallel_ArrMap_app_𝔞

lemma (in cf_parallel) the_cf_parallel_ArrMap_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔟'⦈"
proof-
  from assms have "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
    by (cs_concl cs_intro: cat_parallel_cs_intros a_in_succ_xI)
  from this show ?thesis
    using cat_parallel_ineq
    by (elim the_cat_parallel_ArrE; simp only: assms) 
      (auto simp: the_cf_parallel_ArrMap_app)
qed

lemmas [cat_parallel_cs_simps] = cf_parallel.the_cf_parallel_ArrMap_app_𝔟

lemma (in cf_parallel) the_cf_parallel_ArrMap_vrange:
  "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈) = (F' `⇩∘ F) ∪⇩∘ set {ℭ⦇CId⦈⦇𝔞'⦈, ℭ⦇CId⦈⦇𝔟'⦈}"
  (is ‹ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈) = ?FF ∪⇩∘ ?CID›)
proof(intro vsubset_antisym)

  show "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈) ⊆⇩∘ ?FF ∪⇩∘ ?CID"
  proof
    (
      intro vsv.vsv_vrange_vsubset the_cf_parallel_ArrMap_vsv, 
      unfold the_cf_parallel_ArrMap_vdomain
    )
    fix f assume prems: "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
    from prems show "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ ∈⇩∘ ?FF ∪⇩∘ ?CID"
      by (elim the_cat_parallel_ArrE; (simp only:)?)
        (
          cs_concl  
            cs_simp: vinsert_set_insert_eq cat_parallel_cs_simps 
            cs_intro: vsv.vsv_vimageI1 V_cs_intros
        )
  qed

  show "?FF ∪⇩∘ ?CID ⊆⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
  proof(rule vsubsetI)
    fix f assume prems: "f ∈⇩∘ F' `⇩∘ F ∪⇩∘ set {ℭ⦇CId⦈⦇𝔞'⦈, ℭ⦇CId⦈⦇𝔟'⦈}"
    then consider ‹f ∈⇩∘ F' `⇩∘ F› | ‹f = ℭ⦇CId⦈⦇𝔞'⦈› | ‹f = ℭ⦇CId⦈⦇𝔟'⦈› by auto
    then show "f ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
    proof cases
      assume "f ∈⇩∘ F' `⇩∘ F"
      then obtain 𝔣 where 𝔣: "𝔣 ∈⇩∘ F" and f_def: "f = F'⦇𝔣⦈" by auto
      from 𝔣 have f_def': "f = ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇𝔣⦈"
        unfolding f_def by (cs_concl cs_simp: cat_parallel_cs_simps)
      from 𝔣 have "𝔣 ∈⇩∘ 𝒟⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros
          )
      then show "f ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        unfolding f_def' 
        by (auto simp: cat_parallel_cs_intros intro: vsv.vsv_vimageI2)
    next
      assume prems: "f = ℭ⦇CId⦈⦇𝔞'⦈"
      have f_def': "f = ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇𝔞⦈"
        by (cs_concl cs_simp: cat_parallel_cs_simps prems)
      have "𝔞 ∈⇩∘ 𝒟⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        by 
          (
            cs_concl 
              cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros
          )
      then show "f ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        unfolding f_def'
        by (auto simp: cat_parallel_cs_intros intro: vsv.vsv_vimageI2)
    next
      assume prems: "f = ℭ⦇CId⦈⦇𝔟'⦈"
      have f_def': "f = ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇𝔟⦈"
        by (cs_concl cs_shallow cs_simp: V_cs_simps cat_parallel_cs_simps prems)
      have "𝔟 ∈⇩∘ 𝒟⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        by 
          (
            cs_concl 
              cs_simp: cat_parallel_cs_simps cs_intro: cat_parallel_cs_intros
          )
      then show "f ∈⇩∘ ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)"
        unfolding f_def'
        by (auto simp: cat_parallel_cs_intros intro: vsv.vsv_vimageI2)
    qed
  qed

qed

lemma (in cf_parallel) the_cf_parallel_ArrMap_vrange_vsubset_Arr:
  "ℛ⇩∘ (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
proof(intro vsv.vsv_vrange_vsubset, unfold cat_parallel_cs_simps)
  show "vsv (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈)" 
    by (cs_intro_step cat_parallel_cs_intros)
  fix f assume "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
  then show "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ ∈⇩∘ ℭ⦇Arr⦈"
    by (elim the_cat_parallel_ArrE)
      (
        cs_concl 
          cs_simp: cat_parallel_cs_simps  
          cs_intro: cat_cs_intros cat_parallel_cs_intros 
      )+
qed


subsubsection‹Parallel functor is a functor›

lemma (in cf_parallel) cf_parallel_the_cf_parallel_is_tm_functor:
  "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F' : ⇑⇩C 𝔞 𝔟 F ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
proof(intro is_tm_functorI' is_functorI')

  interpret tcp: tiny_category α ‹⇑⇩C 𝔞 𝔟 F› 
    by (rule tiny_category_the_cat_parallel)

  show "vfsequence (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F')" 
    unfolding the_cf_parallel_def by auto
  show "vcard (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F') = 4⇩ℕ"
    unfolding the_cf_parallel_def by (simp add: nat_omega_simps)
  show "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ :
    ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇a⦈ ↦⇘ℭ⇙
    ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇b⦈"
    if "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b" for a b f
    using that
    by (cases rule: the_cat_parallel_is_arrE; simp only:)
      (
        cs_concl 
          cs_simp: cat_parallel_cs_simps
          cs_intro: cat_cs_intros cat_parallel_cs_intros
      )+

  show
    "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇g ∘⇩A⇘⇑⇩C 𝔞 𝔟 F⇙ f⦈ =
      ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇g⦈ ∘⇩A⇘ℭ⇙
      ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘⇑⇩C 𝔞 𝔟 F⇙ c" and "f : a ↦⇘⇑⇩C 𝔞 𝔟 F⇙ b" for b c g a f
    using that
    by (elim the_cat_parallel_is_arrE) (*very slow*)
      (
        all‹simp only:›, 
        all‹
          solves‹simp add: cat_parallel_ineq cat_parallel_𝔞𝔟[symmetric]› | 
          cs_concl 
            cs_simp: cat_cs_simps cat_parallel_cs_simps 
            cs_intro: cat_cs_intros cat_parallel_cs_intros
          ›
      )

  show 
    "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇⇑⇩C 𝔞 𝔟 F⦇CId⦈⦇c⦈⦈ =
      ℭ⦇CId⦈⦇⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈" for c
    using that
    by (elim the_cat_parallel_ObjE; simp only:)
      (cs_concl cs_simp: cat_parallel_cs_simps)+

  show "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈ ∈⇩∘ Vset α"
  proof
    (
      rule vbrelation.vbrelation_Limit_in_VsetI,
      unfold 
        the_cf_parallel_ObjMap_vdomain 
        the_cf_parallel_ObjMap_vrange 
        the_cat_parallel_components(1);
      (intro Limit_vdoubleton_in_VsetI)?
    )
    show "𝔞 ∈⇩∘ Vset α" "𝔟 ∈⇩∘ Vset α" "𝔞' ∈⇩∘ Vset α" "𝔟' ∈⇩∘ Vset α"
      by (cs_concl cs_intro: cat_cs_intros cat_parallel_cs_intros)+
  qed (use the_cf_parallel_ObjMap_vsv in blast)+

  show "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈ ∈⇩∘ Vset α"
  proof
    (
      rule vbrelation.vbrelation_Limit_in_VsetI,
      unfold 
        the_cf_parallel_ArrMap_vdomain 
        the_cf_parallel_ArrMap_vrange 
        the_cat_parallel_components(1);
      (intro tcp.tiny_cat_Arr_in_Vset vunion_in_VsetI Limit_vdoubleton_in_VsetI)?
    )
    show "ℭ⦇CId⦈⦇𝔞'⦈ ∈⇩∘ Vset α" "ℭ⦇CId⦈⦇𝔟'⦈ ∈⇩∘ Vset α"
      by (cs_concl cs_intro: cat_cs_intros cat_parallel_cs_intros)+
    from cf_parallel_F' have "F' `⇩∘ F ⊆⇩∘ Hom ℭ 𝔞' 𝔟'"
      by (simp add: F'.vsv_vimage_vsubsetI)
    moreover have "Hom ℭ 𝔞' 𝔟' ∈⇩∘ Vset α"
      by (auto simp: cat_Hom_in_Vset cf_parallel_𝔞' cf_parallel_𝔟')
    ultimately show "F' `⇩∘ F ∈⇩∘ Vset α" by auto
  qed (use the_cf_parallel_ArrMap_vsv in blast)+

qed
  (
    cs_concl 
      cs_simp: cat_parallel_cs_simps 
      cs_intro: 
        the_cf_parallel_ObjMap_vrange_vsubset_Obj 
        cat_parallel_cs_intros cat_cs_intros cat_small_cs_intros
  )+

lemma (in cf_parallel) cf_parallel_the_cf_parallel_is_tm_functor':
  assumes "𝔄' = ⇑⇩C 𝔞 𝔟 F" and "ℭ' = ℭ"
  shows "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F' : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
  unfolding assms by (rule cf_parallel_the_cf_parallel_is_tm_functor)

lemmas [cat_parallel_cs_intros] =
  cf_parallel.cf_parallel_the_cf_parallel_is_tm_functor'


subsubsection‹Opposite parallel functor›

lemma (in cf_parallel) cf_parallel_the_cf_parallel_op[cat_op_simps]:
  "op_cf (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F') = ⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F'"
proof-
  interpret ↑: is_tm_functor α ‹⇑⇩C 𝔞 𝔟 F› ℭ ‹⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'›
    by (rule cf_parallel_the_cf_parallel_is_tm_functor)
  show ?thesis
  proof
    (
      rule cf_eqI[of α ‹⇑⇩C 𝔟 𝔞 F› ‹op_cat ℭ› _ ‹⇑⇩C 𝔟 𝔞 F› ‹op_cat ℭ›], 
      unfold cat_op_simps
    )
    show "op_cf (⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F') : ⇑⇩C 𝔟 𝔞 F ↦↦⇩C⇘α⇙ op_cat ℭ"
      by (cs_concl cs_shallow cs_simp: cat_op_simps cs_intro: cat_op_intros)
    show "⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F' : ⇑⇩C 𝔟 𝔞 F ↦↦⇩C⇘α⇙ op_cat ℭ"
      by 
        (
          cs_concl 
            cs_intro: cat_op_intros cat_small_cs_intros cat_parallel_cs_intros
        )
    show
      "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈ =
        ⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F'⦇ObjMap⦈"
    proof
      (
        rule vsv_eqI;
        (intro cat_parallel_cs_intros)?;
        unfold cat_parallel_cs_simps
      )
      fix a assume "a ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Obj⦈"
      then consider ‹a = 𝔞› | ‹a = 𝔟› by (elim the_cat_parallel_ObjE) simp
      then show
        "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ObjMap⦈⦇a⦈ =
          ⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F'⦇ObjMap⦈⦇a⦈"
        by cases
          (
            cs_concl 
              cs_simp: cat_parallel_cs_simps
              cs_intro: cat_parallel_cs_intros cat_op_intros
          )
    qed (auto simp: the_cat_parallel_components)
    show 
      "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈ =
        ⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F'⦇ArrMap⦈"
    proof
      (
        rule vsv_eqI;
        (intro cat_parallel_cs_intros)?; 
        unfold cat_parallel_cs_simps
      )
      fix f assume "f ∈⇩∘ ⇑⇩C 𝔞 𝔟 F⦇Arr⦈"
      then consider ‹f = 𝔞› | ‹f = 𝔟› | ‹f ∈⇩∘ F›
        by (elim the_cat_parallel_ArrE) simp
      then show
        "⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 F 𝔞' 𝔟' F'⦇ArrMap⦈⦇f⦈ =
          ⇑→⇑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 F 𝔟' 𝔞' F'⦇ArrMap⦈⦇f⦈"
        by cases
          (
            cs_concl 
              cs_simp: cat_parallel_cs_simps cat_op_simps 
              cs_intro: cat_parallel_cs_intros cat_op_intros
          )+
    qed (auto simp: the_cat_parallel_components)
  qed simp_all
qed

lemmas [cat_op_simps] = cf_parallel.cf_parallel_the_cf_parallel_op



subsection‹
Background for the definition of a category with two parallel arrows 
between two objects
›


text‹
The case of two parallel arrows between two objects is treated explicitly 
because it is prevalent in applications.
›

definition 𝔤⇩P⇩L :: V where "𝔤⇩P⇩L = 0"
definition 𝔣⇩P⇩L :: V where "𝔣⇩P⇩L = 1⇩ℕ"

definition 𝔞⇩P⇩L⇩2 :: V where "𝔞⇩P⇩L⇩2 = 𝔞⇩P⇩L (set {𝔤⇩P⇩L, 𝔣⇩P⇩L})"
definition 𝔟⇩P⇩L⇩2 :: V where "𝔟⇩P⇩L⇩2 = 𝔟⇩P⇩L (set {𝔤⇩P⇩L, 𝔣⇩P⇩L})"

lemma cat_PL2_ineq:
  shows cat_PL2_𝔞𝔟[cat_parallel_cs_intros]: "𝔞⇩P⇩L⇩2 ≠ 𝔟⇩P⇩L⇩2"
    and cat_PL2_𝔞𝔤[cat_parallel_cs_intros]: "𝔞⇩P⇩L⇩2 ≠ 𝔤⇩P⇩L"
    and cat_PL2_𝔞𝔣[cat_parallel_cs_intros]: "𝔞⇩P⇩L⇩2 ≠ 𝔣⇩P⇩L"
    and cat_PL2_𝔟𝔤[cat_parallel_cs_intros]: "𝔟⇩P⇩L⇩2 ≠ 𝔤⇩P⇩L"
    and cat_PL2_𝔟𝔣[cat_parallel_cs_intros]: "𝔟⇩P⇩L⇩2 ≠ 𝔣⇩P⇩L"
    and cat_PL2_𝔤𝔣[cat_parallel_cs_intros]: "𝔤⇩P⇩L ≠ 𝔣⇩P⇩L"
  unfolding 𝔞⇩P⇩L⇩2_def 𝔟⇩P⇩L⇩2_def 𝔤⇩P⇩L_def 𝔣⇩P⇩L_def 𝔞⇩P⇩L_def 𝔟⇩P⇩L_def 
  by (simp_all add: Set.doubleton_eq_iff one)
  
lemma (in 𝒵) 
  shows cat_PL2_𝔞[cat_parallel_cs_intros]: "𝔞⇩P⇩L⇩2 ∈⇩∘ Vset α"
    and cat_PL2_𝔟[cat_parallel_cs_intros]: "𝔟⇩P⇩L⇩2 ∈⇩∘ Vset α"
    and cat_PL2_𝔤[cat_parallel_cs_intros]: "𝔤⇩P⇩L ∈⇩∘ Vset α"
    and cat_PL2_𝔣[cat_parallel_cs_intros]: "𝔣⇩P⇩L ∈⇩∘ Vset α"
  unfolding 𝔞⇩P⇩L_def 𝔟⇩P⇩L_def 𝔞⇩P⇩L⇩2_def 𝔟⇩P⇩L⇩2_def 𝔤⇩P⇩L_def 𝔣⇩P⇩L_def 
  by (simp_all add: Limit_vdoubleton_in_VsetI)



subsection‹
Local assumptions for a category with two parallel arrows between two objects
›

locale cat_parallel_2 = 𝒵 α for α +  
  fixes 𝔞 𝔟 𝔤 𝔣
  assumes cat_parallel_2_𝔞𝔟[cat_parallel_cs_intros]: "𝔞 ≠ 𝔟"
    and cat_parallel_2_𝔞𝔤[cat_parallel_cs_intros]: "𝔞 ≠ 𝔤"
    and cat_parallel_2_𝔞𝔣[cat_parallel_cs_intros]: "𝔞 ≠ 𝔣"
    and cat_parallel_2_𝔟𝔤[cat_parallel_cs_intros]: "𝔟 ≠ 𝔤"
    and cat_parallel_2_𝔟𝔣[cat_parallel_cs_intros]: "𝔟 ≠ 𝔣"
    and cat_parallel_2_𝔤𝔣[cat_parallel_cs_intros]: "𝔤 ≠ 𝔣"
    and cat_parallel_2_𝔞_in_Vset[cat_parallel_cs_intros]: "𝔞 ∈⇩∘ Vset α"
    and cat_parallel_2_𝔟_in_Vset[cat_parallel_cs_intros]: "𝔟 ∈⇩∘ Vset α"
    and cat_parallel_2_𝔤_in_Vset[cat_parallel_cs_intros]: "𝔤 ∈⇩∘ Vset α"
    and cat_parallel_2_𝔣_in_Vset[cat_parallel_cs_intros]: "𝔣 ∈⇩∘ Vset α"

lemmas (in cat_parallel_2) cat_parallel_ineq =
  cat_parallel_2_𝔞𝔟
  cat_parallel_2_𝔞𝔤
  cat_parallel_2_𝔞𝔣
  cat_parallel_2_𝔟𝔤
  cat_parallel_2_𝔟𝔣
  cat_parallel_2_𝔤𝔣


text‹Rules.›

lemmas (in cat_parallel_2) [cat_parallel_cs_intros] = cat_parallel_2_axioms

mk_ide rf cat_parallel_2_def[unfolded cat_parallel_2_axioms_def]
  |intro cat_parallel_2I|
  |dest cat_parallel_2D[dest]|
  |elim cat_parallel_2E[elim]|

sublocale cat_parallel_2 ⊆ cat_parallel α 𝔞 𝔟 ‹set {𝔤, 𝔣}›
  by unfold_locales 
    (simp_all add: cat_parallel_cs_intros Limit_vdoubleton_in_VsetI)


text‹Duality.›

lemma (in cat_parallel_2) cat_parallel_op[cat_op_intros]: 
  "cat_parallel_2 α 𝔟 𝔞 𝔣 𝔤"
  by (intro cat_parallel_2I) 
    (auto intro!: cat_parallel_cs_intros cat_parallel_ineq[symmetric])



subsection‹‹↑↑›: category with two parallel arrows between two objects›


subsubsection‹Definition and elementary properties›


text‹See Chapter I-2 and Chapter III-3 in \<^cite>‹"mac_lane_categories_2010"›.›

definition the_cat_parallel_2 :: "V ⇒ V ⇒ V ⇒ V ⇒ V" (‹↑↑⇩C›)
  where "↑↑⇩C 𝔞 𝔟 𝔤 𝔣 = ⇑⇩C 𝔞 𝔟 (set {𝔤, 𝔣})"


text‹Components.›

lemma the_cat_parallel_2_components:
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Obj⦈ = set {𝔞, 𝔟}"
    and "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈ = set {𝔞, 𝔟, 𝔤, 𝔣}"
  unfolding the_cat_parallel_2_def the_cat_parallel_components by auto


text‹Elementary properties.›

lemma the_cat_parallel_2_commute: "↑↑⇩C 𝔞 𝔟 𝔤 𝔣 = ↑↑⇩C 𝔞 𝔟 𝔣 𝔤"
  unfolding the_cat_parallel_2_def by (simp add: insert_commute)

lemma cat_parallel_is_cat_parallel_2:
  assumes "cat_parallel α 𝔞 𝔟 (set {𝔤, 𝔣})" and "𝔤 ≠ 𝔣"
  shows "cat_parallel_2 α 𝔞 𝔟 𝔤 𝔣"
proof-
  interpret cat_parallel α 𝔞 𝔟 ‹set {𝔤, 𝔣}› by (rule assms(1))
  show ?thesis
    using cat_parallel_𝔞F cat_parallel_𝔟F cat_parallel_F_in_Vset assms
    by (intro cat_parallel_2I)
      (
        auto 
          dest: vdoubleton_in_VsetD 
          simp: cat_parallel_𝔞_in_Vset cat_parallel_𝔟_in_Vset
     )
qed


subsubsection‹Objects›

lemma the_cat_parallel_2_Obj_𝔞I[cat_parallel_cs_intros]:
  assumes "a = 𝔞"
  shows "a ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Obj⦈"
  unfolding the_cat_parallel_2_def
  by (cs_concl cs_simp: assms cs_intro: cat_parallel_cs_intros)

lemma the_cat_parallel_2_Obj_𝔟I[cat_parallel_cs_intros]:
  assumes "a = 𝔟"
  shows "a ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Obj⦈"
  unfolding the_cat_parallel_2_def
  by (cs_concl cs_shallow cs_simp: assms cs_intro: cat_parallel_cs_intros)

lemma the_cat_parallel_2_ObjE:
  assumes "a ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Obj⦈"
  obtains "a = 𝔞" | "a = 𝔟" 
  using assms unfolding the_cat_parallel_2_def by (elim the_cat_parallel_ObjE)


subsubsection‹Arrows›

lemma the_cat_parallel_2_Arr_𝔞I[cat_parallel_cs_intros]:
  assumes "f = 𝔞"  
  shows "f ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈"
  using assms unfolding the_cat_parallel_2_def by (intro the_cat_parallel_Arr_𝔞I)

lemma the_cat_parallel_2_Arr_𝔟I[cat_parallel_cs_intros]:
  assumes "f = 𝔟"  
  shows "f ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈"
  using assms unfolding the_cat_parallel_2_def by (intro the_cat_parallel_Arr_𝔟I)

lemma the_cat_parallel_2_Arr_𝔤I[cat_parallel_cs_intros]:
  assumes "f = 𝔤"
  shows "f ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈"
  unfolding assms(1) the_cat_parallel_2_def
  by (cs_concl cs_simp: V_cs_simps cs_intro: V_cs_intros cat_parallel_cs_intros)

lemma the_cat_parallel_2_Arr_𝔣I[cat_parallel_cs_intros]:
  assumes "f = 𝔣"
  shows "f ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈"
  unfolding assms(1) the_cat_parallel_2_def
  by 
    (
      cs_concl cs_shallow 
        cs_simp: V_cs_simps cs_intro: V_cs_intros cat_parallel_cs_intros
    )

lemma the_cat_parallel_2_ArrE:
  assumes "f ∈⇩∘ ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Arr⦈"
  obtains "f = 𝔞" | "f = 𝔟" | "f = 𝔤" | "f = 𝔣"
  using assms that 
  unfolding the_cat_parallel_2_def
  by (auto elim!: the_cat_parallel_ArrE)


subsubsection‹Domain›

lemma the_cat_parallel_2_Dom_vsv[cat_parallel_cs_intros]: "vsv (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈)"
  unfolding the_cat_parallel_2_def by (rule the_cat_parallel_Dom_vsv)

lemma the_cat_parallel_2_Dom_vdomain[cat_parallel_cs_simps]: 
  "𝒟⇩∘ (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈) = set {𝔞, 𝔟, 𝔤, 𝔣}"
  unfolding the_cat_parallel_2_def the_cat_parallel_Dom_vdomain by auto

lemma (in cat_parallel_2) the_cat_parallel_2_Dom_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈⦇f⦈ = 𝔟"
  using assms 
  unfolding the_cat_parallel_2_def 
  by (simp add: the_cat_parallel_Dom_app_𝔟)

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Dom_app_𝔟

lemma (in cat_parallel_2) the_cat_parallel_2_Dom_app_𝔤[cat_parallel_cs_simps]:
  assumes "f = 𝔤"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈⦇f⦈ = 𝔞"
  using assms
  unfolding the_cat_parallel_2_def
  by (intro the_cat_parallel_Dom_app_F) simp

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Dom_app_𝔤

lemma (in cat_parallel_2) the_cat_parallel_2_Dom_app_𝔣[cat_parallel_cs_simps]:
  assumes "f = 𝔣"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈⦇f⦈ = 𝔞"
  using assms
  unfolding the_cat_parallel_2_def
  by (intro the_cat_parallel_Dom_app_F) simp

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Dom_app_𝔣

lemma (in cat_parallel_2) the_cat_parallel_2_Dom_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Dom⦈⦇f⦈ = 𝔞"
  using assms 
  unfolding the_cat_parallel_2_def 
  by (simp add: the_cat_parallel_Dom_app_𝔞)

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Dom_app_𝔞


subsubsection‹Codomain›

lemma the_cat_parallel_2_Cod_vsv[cat_parallel_cs_intros]: "vsv (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈)"
  unfolding the_cat_parallel_2_def by (rule the_cat_parallel_Cod_vsv)

lemma the_cat_parallel_2_Cod_vdomain[cat_parallel_cs_simps]: 
  "𝒟⇩∘ (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈) = set {𝔞, 𝔟, 𝔤, 𝔣}"
  unfolding the_cat_parallel_2_def the_cat_parallel_Cod_vdomain by auto

lemma (in cat_parallel_2) the_cat_parallel_2_Cod_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈⦇f⦈ = 𝔟"
  using assms 
  unfolding the_cat_parallel_2_def 
  by (simp add: the_cat_parallel_Cod_app_𝔟)

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Cod_app_𝔟

lemma (in cat_parallel_2) the_cat_parallel_2_Cod_app_𝔤[cat_parallel_cs_simps]:
  assumes "f = 𝔤"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈⦇f⦈ = 𝔟"
  using assms
  unfolding the_cat_parallel_2_def
  by (intro the_cat_parallel_Cod_app_F) simp

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Cod_app_𝔤

lemma (in cat_parallel_2) the_cat_parallel_2_Cod_app_𝔣[cat_parallel_cs_simps]:
  assumes "f = 𝔣"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈⦇f⦈ = 𝔟"
  using assms
  unfolding the_cat_parallel_2_def
  by (intro the_cat_parallel_Cod_app_F) simp

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Cod_app_𝔣

lemma (in cat_parallel_2) the_cat_parallel_2_Cod_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Cod⦈⦇f⦈ = 𝔞"
  using assms 
  unfolding the_cat_parallel_2_def 
  by (simp add: the_cat_parallel_Cod_app_𝔞)

lemmas [cat_parallel_cs_simps] = cat_parallel_2.the_cat_parallel_2_Cod_app_𝔞


subsubsection‹Composition›

lemma the_cat_parallel_2_Comp_vsv[cat_parallel_cs_intros]:
  "vsv (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Comp⦈)"
  unfolding the_cat_parallel_2_def by (rule the_cat_parallel_Comp_vsv)

lemma the_cat_parallel_2_Comp_app_𝔟𝔟[cat_parallel_cs_simps]:
  assumes "g = 𝔟" and "f = 𝔟"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f"
proof-
  note gf = the_cat_parallel_Comp_app_𝔟𝔟[OF assms, where F=‹set {𝔤, 𝔣}›]
  show "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f"
    unfolding the_cat_parallel_2_def 
    subgoal unfolding gf(1) by simp
    subgoal unfolding gf(2) by simp
    done
qed

lemma the_cat_parallel_2_Comp_app_𝔞𝔞[cat_parallel_cs_simps]:
  assumes "g = 𝔞" and "f = 𝔞"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f"
proof-
  note gf = the_cat_parallel_Comp_app_𝔞𝔞[OF assms, where F=‹set {𝔤, 𝔣}›]
  show "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f"
    unfolding the_cat_parallel_2_def 
    subgoal unfolding gf(1) by simp
    subgoal unfolding gf(2) by simp
    done
qed

lemma the_cat_parallel_2_Comp_app_𝔟𝔤[cat_parallel_cs_simps]:
  assumes "g = 𝔟" and "f = 𝔤"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f"
  unfolding 
    the_cat_parallel_2_def assms
    the_cat_parallel_Comp_app_𝔟F[
      where F=‹set {𝔤, 𝔣}›, OF assms(1), of 𝔤, unfolded assms, simplified
      ]
  by simp

lemma the_cat_parallel_2_Comp_app_𝔟𝔣[cat_parallel_cs_simps]:
  assumes "g = 𝔟" and "f = 𝔣"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = f" 
  unfolding 
    the_cat_parallel_2_def assms
    the_cat_parallel_Comp_app_𝔟F[
      where F=‹set {𝔤, 𝔣}›, OF assms(1), of 𝔣, unfolded assms, simplified
      ]
  by simp

lemma (in cat_parallel_2) the_cat_parallel_2_Comp_app_𝔤𝔞[cat_parallel_cs_simps]:
  assumes "g = 𝔤" and "f = 𝔞"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" 
  unfolding 
    the_cat_parallel_2_def assms
    the_cat_parallel_Comp_app_F𝔞[
      of 𝔤, OF _ assms(2), unfolded assms, simplified
      ]
  by simp

lemma (in cat_parallel_2) the_cat_parallel_2_Comp_app_𝔣𝔞[cat_parallel_cs_simps]:
  assumes "g = 𝔣" and "f = 𝔞"
  shows "g ∘⇩A⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ f = g" 
  unfolding 
    the_cat_parallel_2_def assms
    the_cat_parallel_Comp_app_F𝔞[
      of 𝔣, OF _ assms(2), unfolded assms, simplified
      ]
  by simp


subsubsection‹Identity›

lemma the_cat_parallel_2_CId_vsv[cat_parallel_cs_intros]: "vsv (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇CId⦈)"
  unfolding the_cat_parallel_2_def by (rule the_cat_parallel_CId_vsv)

lemma the_cat_parallel_2_CId_vdomain[cat_parallel_cs_simps]:
  "𝒟⇩∘ (↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇CId⦈) = set {𝔞, 𝔟}"
  unfolding the_cat_parallel_2_def by (rule the_cat_parallel_CId_vdomain)
  
lemma the_cat_parallel_2_CId_app_𝔞[cat_parallel_cs_simps]: 
  assumes "a = 𝔞"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇CId⦈⦇a⦈ = 𝔞"
  unfolding assms the_cat_parallel_2_def
  by (simp add: the_cat_parallel_CId_app_𝔞)

lemma the_cat_parallel_2_CId_app_𝔟[cat_parallel_cs_simps]: 
  assumes "a = 𝔟"
  shows "↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇CId⦈⦇a⦈ = 𝔟"
  unfolding assms the_cat_parallel_2_def
  by (simp add: the_cat_parallel_CId_app_𝔟)


subsubsection‹Arrow with a domain and a codomain›

lemma (in cat_parallel_2) the_cat_parallel_2_is_arr_𝔞𝔞𝔞[cat_parallel_cs_intros]:
  assumes "a' = 𝔞" and "b' = 𝔞" and "f = 𝔞"
  shows "f : a' ↦⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ b'"
  unfolding assms the_cat_parallel_2_def
  by (simp add: the_cat_parallel_is_arr_𝔞𝔞𝔞)

lemma (in cat_parallel_2) the_cat_parallel_2_is_arr_𝔟𝔟𝔟[cat_parallel_cs_intros]:
  assumes "a' = 𝔟" and "b' = 𝔟" and "f = 𝔟"
  shows "f : a' ↦⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ b'"
  unfolding assms the_cat_parallel_2_def
  by (simp add: the_cat_parallel_is_arr_𝔟𝔟𝔟)

lemma (in cat_parallel_2) the_cat_parallel_2_is_arr_𝔞𝔟𝔤[cat_parallel_cs_intros]:
  assumes "a' = 𝔞" and "b' = 𝔟" and "f = 𝔤"
  shows "f : a' ↦⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ b'"
  unfolding assms the_cat_parallel_2_def
  by 
    (
      rule the_cat_parallel_is_arr_𝔞𝔟F[
        OF assms(1,2), of 𝔤, unfolded assms, simplified
        ]
    )

lemma (in cat_parallel_2) the_cat_parallel_2_is_arr_𝔞𝔟𝔣[cat_parallel_cs_intros]:
  assumes "a' = 𝔞" and "b' = 𝔟" and "f = 𝔣"
  shows "f : a' ↦⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ b'"
  unfolding assms the_cat_parallel_2_def
  by 
    (
      rule the_cat_parallel_is_arr_𝔞𝔟F[
        OF assms(1,2), of 𝔣, unfolded assms, simplified
        ]
    )

lemma (in cat_parallel_2) the_cat_parallel_2_is_arrE:
  assumes "f' : a' ↦⇘↑↑⇩C 𝔞 𝔟 𝔤 𝔣⇙ b'"
  obtains "a' = 𝔞" and "b' = 𝔞" and "f' = 𝔞"
        | "a' = 𝔟" and "b' = 𝔟" and "f' = 𝔟"
        | "a' = 𝔞" and "b' = 𝔟" and "f' = 𝔤"
        | "a' = 𝔞" and "b' = 𝔟" and "f' = 𝔣"
  using assms 
  unfolding the_cat_parallel_2_def
  by (elim the_cat_parallel_is_arrE) auto


subsubsection‹‹↑↑› is a category›

lemma (in cat_parallel_2) 
  finite_category_the_cat_parallel_2[cat_parallel_cs_intros]:
  "finite_category α (↑↑⇩C 𝔞 𝔟 𝔤 𝔣)"
proof(intro finite_categoryI'' )
  show "tiny_category α (↑↑⇩C 𝔞 𝔟 𝔤 𝔣)"
    unfolding the_cat_parallel_2_def by (rule tiny_category_the_cat_parallel)
qed (auto simp: the_cat_parallel_2_components)

lemmas [cat_parallel_cs_intros] = 
  cat_parallel_2.finite_category_the_cat_parallel_2


subsubsection‹Opposite parallel category›

lemma (in cat_parallel_2) op_cat_the_cat_parallel_2[cat_op_simps]: 
  "op_cat (↑↑⇩C 𝔞 𝔟 𝔤 𝔣) = ↑↑⇩C 𝔟 𝔞 𝔣 𝔤"
  unfolding the_cat_parallel_2_def cat_op_simps by (metis doubleton_eq_iff)

lemmas [cat_op_simps] = cat_parallel_2.op_cat_the_cat_parallel_2



subsection‹
Parallel functor for a category with two parallel arrows between two objects
›

locale cf_parallel_2 = cat_parallel_2 α 𝔞 𝔟 𝔤 𝔣 + category α ℭ 
  for α 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' ℭ :: V +
  assumes cf_parallel_𝔤'[cat_parallel_cs_intros]: "𝔤' : 𝔞' ↦⇘ℭ⇙ 𝔟'"
    and cf_parallel_𝔣'[cat_parallel_cs_intros]: "𝔣' : 𝔞' ↦⇘ℭ⇙ 𝔟'"

sublocale cf_parallel_2 ⊆ 
  cf_parallel α 𝔞 𝔟 ‹set {𝔤, 𝔣}› 𝔞' 𝔟' ‹λf∈⇩∘set {𝔤, 𝔣}. (f = 𝔣 ? 𝔣' : 𝔤')› ℭ
  by unfold_locales (auto intro: cat_parallel_cs_intros cat_cs_intros)

lemma (in cf_parallel_2) cf_parallel_2_𝔤''[cat_parallel_cs_intros]:
  assumes "a = 𝔞'" and "b = 𝔟'"
  shows "𝔤' : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_parallel_𝔤')

lemma (in cf_parallel_2) cf_parallel_2_𝔤'''[cat_parallel_cs_intros]:
  assumes "g = 𝔤'" and "b = 𝔟'"
  shows "g : 𝔞' ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_parallel_𝔤')

lemma (in cf_parallel_2) cf_parallel_2_𝔤''''[cat_parallel_cs_intros]:
  assumes "g = 𝔤'" and "a = 𝔞'"
  shows "g : a ↦⇘ℭ⇙ 𝔟'"
  unfolding assms by (rule cf_parallel_𝔤')

lemma (in cf_parallel_2) cf_parallel_2_𝔣''[cat_parallel_cs_intros]:
  assumes "a = 𝔞'" and "b = 𝔟'"
  shows "𝔣' : a ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_parallel_𝔣') 

lemma (in cf_parallel_2) cf_parallel_2_𝔣'''[cat_parallel_cs_intros]:
  assumes "f = 𝔣'" and "b = 𝔟'"
  shows "f : 𝔞' ↦⇘ℭ⇙ b"
  unfolding assms by (rule cf_parallel_𝔣')

lemma (in cf_parallel_2) cf_parallel_2_𝔣''''[cat_parallel_cs_intros]:
  assumes "f = 𝔣'" and "a = 𝔞'"
  shows "f : a ↦⇘ℭ⇙ 𝔟'"
  unfolding assms by (rule cf_parallel_𝔣') 


text‹Rules.›

lemma (in cf_parallel_2) cf_parallel_axioms'[cat_parallel_cs_intros]:
  assumes "α' = α" 
    and "a = 𝔞" 
    and "b = 𝔟" 
    and "g = 𝔤" 
    and "f = 𝔣" 
    and "a' = 𝔞'" 
    and "b' = 𝔟'" 
    and "g' = 𝔤'" 
    and "f' = 𝔣'" 
  shows "cf_parallel_2 α' a b g f a' b' g' f' ℭ"
  unfolding assms by (rule cf_parallel_2_axioms)

mk_ide rf cf_parallel_2_def[unfolded cf_parallel_2_axioms_def]
  |intro cf_parallel_2I|
  |dest cf_parallel_2D[dest]|
  |elim cf_parallel_2E[elim]|

lemmas [cat_parallel_cs_intros] = cf_parallelD(1,2)


text‹Duality.›

lemma (in cf_parallel_2) cf_parallel_2_op[cat_op_intros]: 
  "cf_parallel_2 α 𝔟 𝔞 𝔣 𝔤 𝔟' 𝔞' 𝔣' 𝔤' (op_cat ℭ)"
  by (intro cf_parallel_2I, unfold cat_op_simps)
    (cs_concl cs_intro: cat_parallel_cs_intros cat_cs_intros cat_op_intros)

lemmas [cat_op_intros] = cf_parallel.cf_parallel_op


subsubsection‹Definition and elementary properties›

definition the_cf_parallel_2 :: "V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V ⇒ V" 
  (‹↑↑→↑↑⇩C⇩F›)
  where "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' =
    ⇑→⇑⇩C⇩F ℭ 𝔞 𝔟 (set {𝔤, 𝔣}) 𝔞' 𝔟' (λf∈⇩∘set {𝔤, 𝔣}. (f = 𝔣 ? 𝔣' : 𝔤'))"


text‹Components.›

lemma the_cf_parallel_2_components:
  shows [cat_parallel_cs_simps]: 
      "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇HomDom⦈ = ↑↑⇩C 𝔞 𝔟 𝔤 𝔣"
    and [cat_parallel_cs_simps]: 
      "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇HomCod⦈ = ℭ"
  unfolding 
    the_cf_parallel_2_def the_cat_parallel_2_def the_cf_parallel_components
  by simp_all


text‹Elementary properties.›

lemma (in cf_parallel_2) cf_parallel_2_the_cf_parallel_2_commute:
  "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' = ↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔣 𝔤 𝔞' 𝔟' 𝔣' 𝔤'"
  using cat_parallel_2_𝔤𝔣 
  unfolding the_cf_parallel_2_def insert_commute
  by (force simp: VLambda_vdoubleton)

lemma cf_parallel_is_cf_parallel_2:
  assumes 
    "cf_parallel α 𝔞 𝔟 (set {𝔤, 𝔣}) 𝔞' 𝔟' (λf∈⇩∘set {𝔤, 𝔣}. (f = 𝔣 ? 𝔣' : 𝔤')) ℭ" 
    and "𝔤 ≠ 𝔣"
  shows "cf_parallel_2 α 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' ℭ"
proof-
  interpret
    cf_parallel α 𝔞 𝔟 ‹set {𝔤, 𝔣}› 𝔞' 𝔟' ‹λf∈⇩∘set {𝔤, 𝔣}. (f = 𝔣 ? 𝔣' : 𝔤')› ℭ  
    by (rule assms(1))
  have 𝔤𝔣: "𝔤 ∈⇩∘ set {𝔤, 𝔣}" "𝔣 ∈⇩∘ set {𝔤, 𝔣}" by auto
  show ?thesis
    using cat_parallel_axioms assms(2) category_axioms 𝔤𝔣[THEN cf_parallel_F']
    by (intro cf_parallel_2I cat_parallel_is_cat_parallel_2) 
      (auto simp: assms(2))
qed


subsubsection‹Object map›

lemma the_cf_parallel_2_ObjMap_vsv[cat_parallel_cs_intros]: 
  "vsv (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈)"
  unfolding the_cf_parallel_2_def by (intro cat_parallel_cs_intros)

lemma the_cf_parallel_2_ObjMap_vdomain[cat_parallel_cs_simps]: 
  "𝒟⇩∘ (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈) = ↑↑⇩C 𝔞 𝔟 𝔤 𝔣⦇Obj⦈"
  unfolding the_cf_parallel_2_def
  by (cs_concl cs_shallow cs_simp: cat_parallel_cs_simps the_cat_parallel_2_def) 

lemma (in cf_parallel_2) the_cf_parallel_2_ObjMap_app_𝔞[cat_parallel_cs_simps]:
  assumes "x = 𝔞"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈⦇x⦈ = 𝔞'"
  unfolding the_cf_parallel_2_def 
  by (cs_concl cs_simp: assms cat_parallel_cs_simps)

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ObjMap_app_𝔞

lemma (in cf_parallel_2) the_cf_parallel_2_ObjMap_app_𝔟[cat_parallel_cs_simps]:
  assumes "x = 𝔟"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈⦇x⦈ = 𝔟'"
  unfolding the_cf_parallel_2_def 
  by (cs_concl cs_shallow cs_simp: assms cat_parallel_cs_simps)

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ObjMap_app_𝔟

lemma (in cf_parallel_2) the_cf_parallel_2_ObjMap_vrange:
  "ℛ⇩∘ (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈) = set {𝔞', 𝔟'}"
  unfolding the_cf_parallel_2_def by (rule the_cf_parallel_ObjMap_vrange)

lemma (in cf_parallel_2) the_cf_parallel_2_ObjMap_vrange_vsubset_Obj:
  "ℛ⇩∘ (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ObjMap⦈) ⊆⇩∘ ℭ⦇Obj⦈"
  unfolding the_cf_parallel_2_def 
  by (rule the_cf_parallel_ObjMap_vrange_vsubset_Obj)


subsubsection‹Arrow map›

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_app_𝔤[cat_parallel_cs_simps]:
  assumes "f = 𝔤"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈⦇f⦈ = 𝔤'"
  unfolding the_cf_parallel_2_def assms
  by
    (
      cs_concl 
        cs_simp: V_cs_simps cat_parallel_cs_simps 
        cs_intro: V_cs_intros cat_parallel_cs_intros
    )

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ArrMap_app_𝔤

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_app_𝔣[cat_parallel_cs_simps]:
  assumes "f = 𝔣"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈⦇f⦈ = 𝔣'"
  unfolding the_cf_parallel_2_def assms
  by
    (
      cs_concl 
        cs_simp: V_cs_simps cat_parallel_cs_simps 
        cs_intro: V_cs_intros cat_parallel_cs_intros
    )

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ArrMap_app_𝔣

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_app_𝔞[cat_parallel_cs_simps]:
  assumes "f = 𝔞"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔞'⦈"
  unfolding the_cf_parallel_2_def assms
  by (cs_concl cs_simp: cat_parallel_cs_simps)

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ArrMap_app_𝔞

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_app_𝔟[cat_parallel_cs_simps]:
  assumes "f = 𝔟"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈⦇f⦈ = ℭ⦇CId⦈⦇𝔟'⦈"
  unfolding the_cf_parallel_2_def assms
  by (cs_concl cs_shallow cs_simp: cat_parallel_cs_simps)

lemmas [cat_parallel_cs_simps] = cf_parallel_2.the_cf_parallel_2_ArrMap_app_𝔟

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_vrange:
  "ℛ⇩∘ (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈) = set {ℭ⦇CId⦈⦇𝔞'⦈, ℭ⦇CId⦈⦇𝔟'⦈, 𝔣', 𝔤'}"
  unfolding the_cf_parallel_2_def the_cf_parallel_ArrMap_vrange
  using cat_parallel_2_𝔤𝔣 
  by (auto simp: app_vimage_iff VLambda_vdoubleton)

lemma (in cf_parallel_2) the_cf_parallel_2_ArrMap_vrange_vsubset_Arr:
  "ℛ⇩∘ (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣'⦇ArrMap⦈) ⊆⇩∘ ℭ⦇Arr⦈"
  unfolding the_cf_parallel_2_def 
  by (rule the_cf_parallel_ArrMap_vrange_vsubset_Arr)


subsubsection‹
Parallel functor for a category with two parallel arrows between 
two objects is a functor
›

lemma (in cf_parallel_2) cf_parallel_2_the_cf_parallel_2_is_tm_functor:
  "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' : ↑↑⇩C 𝔞 𝔟 𝔤 𝔣 ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ"
  unfolding the_cf_parallel_2_def the_cat_parallel_2_def
  by (rule cf_parallel_the_cf_parallel_is_tm_functor)

lemma (in cf_parallel_2) cf_parallel_2_the_cf_parallel_2_is_tm_functor':
  assumes "𝔄' = ↑↑⇩C 𝔞 𝔟 𝔤 𝔣" and "ℭ' = ℭ"
  shows "↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣' : 𝔄' ↦↦⇩C⇩.⇩t⇩m⇘α⇙ ℭ'"
  unfolding assms by (rule cf_parallel_2_the_cf_parallel_2_is_tm_functor)

lemmas [cat_parallel_cs_intros] = 
  cf_parallel_2.cf_parallel_2_the_cf_parallel_2_is_tm_functor'


subsubsection‹
Opposite parallel functor for a category with two parallel arrows between 
two objects
›

lemma (in cf_parallel_2) cf_parallel_2_the_cf_parallel_2_op[cat_op_simps]:
  "op_cf (↑↑→↑↑⇩C⇩F ℭ 𝔞 𝔟 𝔤 𝔣 𝔞' 𝔟' 𝔤' 𝔣') = 
    ↑↑→↑↑⇩C⇩F (op_cat ℭ) 𝔟 𝔞 𝔣 𝔤 𝔟' 𝔞' 𝔣' 𝔤'"
  using cat_parallel_2_𝔤𝔣
  unfolding the_cf_parallel_2_def cf_parallel_the_cf_parallel_op
  by (auto simp: VLambda_vdoubleton insert_commute)

lemmas [cat_op_simps] = cf_parallel_2.cf_parallel_2_the_cf_parallel_2_op

text‹\newpage›

end