Theory CZH_SMC_PSemicategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Product semicategory›
theory CZH_SMC_PSemicategory
  imports 
    CZH_SMC_Semifunctor
    CZH_SMC_Small_Semicategory
    CZH_DG_PDigraph
begin



subsection‹Background›


text‹
The concept of a product semicategory, as presented in this work, 
is a generalization of the concept of a product category, as presented in
Chapter II-3 in cite‹"mac_lane_categories_2010"›.
›

named_theorems smc_prod_cs_simps
named_theorems smc_prod_cs_intros



subsection‹Product semicategory: definition and elementary properties›

definition smc_prod :: "V ⇒ (V ⇒ V) ⇒ V" 
  where "smc_prod I 𝔄 = 
    [
      (∏∘i∈∘I. 𝔄 i⦇Obj⦈), 
      (∏∘i∈∘I. 𝔄 i⦇Arr⦈), 
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈)), 
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈)),
      (λgf∈∘composable_arrs (dg_prod I 𝔄). (λi∈∘I. gf⦇0⦈⦇i⦈ ∘A⇘𝔄 i⇙ gf⦇1ℕ⦈⦇i⦈))
    ]∘"

syntax "_PSEMICATEGORY" :: "pttrn ⇒ V ⇒ (V ⇒ V) ⇒ V" 
  ("(3∏SMC_∈∘_./ _)" [0, 0, 10] 10)
translations "∏SMCi∈∘I. 𝔄" ⇌ "CONST smc_prod I (λi. 𝔄)"


text‹Components.›

lemma smc_prod_components:
  shows "(∏SMCi∈∘I. 𝔄 i)⦇Obj⦈ = (∏∘i∈∘I. 𝔄 i⦇Obj⦈)"
    and "(∏SMCi∈∘I. 𝔄 i)⦇Arr⦈ = (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
    and "(∏SMCi∈∘I. 𝔄 i)⦇Dom⦈ = 
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈))"
    and "(∏SMCi∈∘I. 𝔄 i)⦇Cod⦈ = 
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈))"
    and "(∏SMCi∈∘I. 𝔄 i)⦇Comp⦈ = 
      (λgf∈∘composable_arrs (dg_prod I 𝔄). (λi∈∘I. gf⦇0⦈⦇i⦈ ∘A⇘𝔄 i⇙ gf⦇1ℕ⦈⦇i⦈))"
  unfolding smc_prod_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smc_dg_smc_prod[slicing_commute]: 
  "dg_prod I (λi. smc_dg (𝔄 i)) = smc_dg (smc_prod I 𝔄)"
  unfolding dg_prod_def smc_dg_def smc_prod_def dg_field_simps
  by (simp_all add: nat_omega_simps)

context
  fixes 𝔄 φ :: "V ⇒ V"
    and ℭ :: V
begin

lemmas_with 
  [where 𝔄=‹λi. smc_dg (𝔄 i)›, unfolded slicing_simps slicing_commute]:
  smc_prod_ObjI = dg_prod_ObjI
  and smc_prod_ObjD = dg_prod_ObjD
  and smc_prod_ObjE = dg_prod_ObjE
  and smc_prod_Obj_cong = dg_prod_Obj_cong
  and smc_prod_ArrI = dg_prod_ArrI
  and smc_prod_ArrD = dg_prod_ArrD
  and smc_prod_ArrE = dg_prod_ArrE
  and smc_prod_Arr_cong = dg_prod_Arr_cong
  and smc_prod_Dom_vsv[smc_cs_intros] = dg_prod_Dom_vsv
  and smc_prod_Dom_vdomain[smc_cs_simps] = dg_prod_Dom_vdomain
  and smc_prod_Dom_app = dg_prod_Dom_app
  and smc_prod_Dom_app_component_app[smc_cs_simps] = 
    dg_prod_Dom_app_component_app
  and smc_prod_Cod_vsv[smc_cs_intros] = dg_prod_Cod_vsv
  and smc_prod_Cod_app = dg_prod_Cod_app
  and smc_prod_Cod_vdomain[smc_cs_simps] = dg_prod_Cod_vdomain
  and smc_prod_Cod_app_component_app[smc_cs_simps] = 
    dg_prod_Cod_app_component_app
  and smc_prod_vunion_Obj_in_Obj = dg_prod_vunion_Obj_in_Obj
  and smc_prod_vdiff_vunion_Obj_in_Obj = dg_prod_vdiff_vunion_Obj_in_Obj
  and smc_prod_vunion_Arr_in_Arr = dg_prod_vunion_Arr_in_Arr
  and smc_prod_vdiff_vunion_Arr_in_Arr = dg_prod_vdiff_vunion_Arr_in_Arr

end

lemma smc_prod_dg_prod_is_arr: 
  "g : b ↦⇘∏DGi∈∘I. 𝔄 i⇙ c ⟷ g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c"
  unfolding is_arr_def smc_prod_def dg_prod_def dg_field_simps
  by (simp add: nat_omega_simps)

lemma smc_prod_composable_arrs_dg_prod:
  "composable_arrs (∏DGi∈∘I. 𝔄 i) = composable_arrs (∏SMCi∈∘I. 𝔄 i)"
  unfolding composable_arrs_def smc_prod_dg_prod_is_arr by simp



subsection‹Local assumptions for a product semicategory›

locale psemicategory_base = 𝒵 α for α I 𝔄 +
  assumes psmc_semicategories[smc_prod_cs_intros]: 
    "i ∈∘ I ⟹ semicategory α (𝔄 i)"
    and psmc_index_in_Vset[smc_cs_intros]: "I ∈∘ Vset α"


text‹Rules.›

lemma (in psemicategory_base) psemicategory_base_axioms'[smc_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "psemicategory_base α' I' 𝔄"
  unfolding assms by (rule psemicategory_base_axioms)

mk_ide rf psemicategory_base_def[unfolded psemicategory_base_axioms_def]
  |intro psemicategory_baseI|
  |dest psemicategory_baseD[dest]|
  |elim psemicategory_baseE[elim]|

lemma psemicategory_base_pdigraph_baseI:
  assumes "pdigraph_base α I (λi. smc_dg (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ semicategory α (𝔄 i)"
  shows "psemicategory_base α I 𝔄"
proof-
  interpret pdigraph_base α I ‹λi. smc_dg (𝔄 i)›
    rewrites "smc_dg ℭ'⦇Obj⦈ = ℭ'⦇Obj⦈" and "smc_dg ℭ'⦇Arr⦈ = ℭ'⦇Arr⦈" for ℭ'
    by (rule assms(1)) (simp_all add: slicing_simps)
  show ?thesis
    by (intro psemicategory_baseI)
      (auto simp: assms(2) pdg_index_in_Vset pdg_Obj_in_Vset pdg_Arr_in_Vset) 
qed


text‹Product semicategory is a product digraph.›

context psemicategory_base
begin

lemma psmc_pdigraph_base: "pdigraph_base α I (λi. smc_dg (𝔄 i))"
proof(intro pdigraph_baseI)
  show "digraph α (smc_dg (𝔄 i))" if "i ∈∘ I" for i 
    by 
      (
        use that in 
          ‹cs_concl cs_shallow cs_intro: slicing_intros smc_prod_cs_intros›
      )
  show "I ∈∘ Vset α" by (cs_concl cs_shallow cs_intro: smc_cs_intros)
qed auto

interpretation pdg: pdigraph_base α I ‹λi. smc_dg (𝔄 i)› 
  by (rule psmc_pdigraph_base)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  psmc_Obj_in_Vset = pdg.pdg_Obj_in_Vset
  and psmc_Arr_in_Vset = pdg.pdg_Arr_in_Vset
  and psmc_smc_prod_Obj_in_Vset = pdg.pdg_dg_prod_Obj_in_Vset
  and psmc_smc_prod_Arr_in_Vset = pdg.pdg_dg_prod_Arr_in_Vset
  and smc_prod_Dom_app_in_Obj[smc_cs_intros] = pdg.dg_prod_Dom_app_in_Obj
  and smc_prod_Cod_app_in_Obj[smc_cs_intros] = pdg.dg_prod_Cod_app_in_Obj
  and smc_prod_is_arrI = pdg.dg_prod_is_arrI
  and smc_prod_is_arrD[dest] = pdg.dg_prod_is_arrD
  and smc_prod_is_arrE[elim] = pdg.dg_prod_is_arrE

end

lemmas [smc_cs_intros] = psemicategory_base.smc_prod_is_arrD(7)


text‹Elementary properties.›

lemma (in psemicategory_base) psmc_vsubset_index_psemicategory_base:
  assumes "J ⊆∘ I"
  shows "psemicategory_base α J 𝔄"
proof(intro psemicategory_baseI)
  show "semicategory α (𝔄 i)" if "i ∈∘ J" for i 
    using that assms by (auto intro: smc_prod_cs_intros)
  from assms show "J ∈∘ Vset α" by (simp add: vsubset_in_VsetI smc_cs_intros)
qed auto


subsubsection‹Composition›

lemma smc_prod_Comp:
  "(∏SMCi∈∘I. 𝔄 i)⦇Comp⦈ = 
    (
      λgf∈∘composable_arrs (∏SMCi∈∘I. 𝔄 i). 
        (λi∈∘I. gf⦇0⦈⦇i⦈ ∘A⇘𝔄 i⇙ gf⦇1ℕ⦈⦇i⦈)
    )"
  unfolding smc_prod_components smc_prod_composable_arrs_dg_prod by simp

lemma smc_prod_Comp_vdomain[smc_cs_simps]: 
  "𝒟∘ ((∏SMCi∈∘I. 𝔄 i)⦇Comp⦈) = composable_arrs (∏SMCi∈∘I. 𝔄 i)" 
  unfolding smc_prod_Comp by simp

lemma smc_prod_Comp_app: 
  assumes "g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c" and "f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ b"
  shows "g ∘A⇘(∏SMCi∈∘I. 𝔄 i)⇙ f = (λi∈∘I. g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈)" 
proof-
  from assms have "[g, f]∘ ∈∘ composable_arrs (∏SMCi∈∘I. 𝔄 i)" 
    by (auto intro: smc_cs_intros)  
  then show ?thesis unfolding smc_prod_Comp by (auto simp: nat_omega_simps)
qed

lemma smc_prod_Comp_app_component[smc_cs_simps]: 
  assumes "g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c" 
    and "f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ b"
    and "i ∈∘ I"
  shows "(g ∘A⇘(∏SMCi∈∘I. 𝔄 i)⇙ f)⦇i⦈ = g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈"
  using assms(3) unfolding smc_prod_Comp_app[OF assms(1,2)] by simp

lemma (in psemicategory_base) smc_prod_Comp_vrange: 
  "ℛ∘ ((∏SMCi∈∘I. 𝔄 i)⦇Comp⦈) ⊆∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈" 
proof(intro vsubsetI)
  fix h assume prems: "h ∈∘ ℛ∘ ((∏SMCi∈∘I. 𝔄 i)⦇Comp⦈)"
  then obtain gf 
    where h_def: "h = (∏SMCi∈∘I. 𝔄 i)⦇Comp⦈⦇gf⦈" 
      and "gf ∈∘ composable_arrs (∏SMCi∈∘I. 𝔄 i)"
    by (auto simp: smc_prod_Comp intro: smc_cs_intros)
  then obtain g f a b c 
    where gf_def: "gf = [g, f]∘" 
      and g: "g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c" 
      and f: "f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ b"
    by clarsimp
  from g f have gf_comp: "g ∘A⇘(∏SMCi∈∘I. 𝔄 i)⇙ f = (λi∈∘I. g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈)"
    by (rule smc_prod_Comp_app)
  show "h ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈"
    unfolding smc_prod_components
    unfolding h_def gf_def gf_comp
  proof(rule VLambda_in_vproduct)
    fix i assume prems: "i ∈∘ I"
    interpret semicategory α ‹𝔄 i› 
      using prems by (simp add: smc_prod_cs_intros)
    from prems smc_prod_is_arrD(7)[OF g] smc_prod_is_arrD(7)[OF f] have
      "g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ c⦇i⦈" 
      by (auto intro: smc_cs_intros)
    then show "g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈ ∈∘ 𝔄 i⦇Arr⦈" by (simp add: smc_cs_intros)
  qed
qed

lemma smc_prod_Comp_app_vdomain[smc_cs_simps]:
  assumes "g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c" and "f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ b"
  shows "𝒟∘ (g ∘A⇘(∏SMCi∈∘I. 𝔄 i)⇙ f) = I" 
  unfolding smc_prod_Comp_app[OF assms] by simp


subsubsection‹A product ‹α›-semicategory is a tiny ‹β›-semicategory›

lemma (in psemicategory_base) psmc_tiny_semicategory_smc_prod:
  assumes "𝒵 β" and "α ∈∘ β" 
  shows "tiny_semicategory β (∏SMCi∈∘I. 𝔄 i)"
proof(intro tiny_semicategoryI, (unfold slicing_simps)?)

  show "tiny_digraph β (smc_dg (smc_prod I 𝔄))"
    unfolding slicing_commute[symmetric]
    by 
      (
        intro pdigraph_base.pdg_tiny_digraph_dg_prod; 
        (rule assms psmc_pdigraph_base)?
      )

  show "vfsequence (∏SMCi∈∘I. 𝔄 i)" unfolding smc_prod_def by auto
  show "vcard (∏SMCi∈∘I. 𝔄 i) = 5ℕ"
    unfolding smc_prod_def by (simp add: nat_omega_simps)
  show "vsv ((∏SMCi∈∘I. 𝔄 i)⦇Comp⦈)" unfolding smc_prod_Comp by simp
  
  show
    "(gf ∈∘ 𝒟∘ ((∏SMCi∈∘I. 𝔄 i)⦇Comp⦈)) ⟷
      (
        ∃g f b c a. 
          gf = [g, f]∘ ∧ g : b ↦⇘smc_prod I 𝔄⇙ c ∧ f : a ↦⇘smc_prod I 𝔄⇙ b
      )"
    for gf
    by (auto intro: smc_cs_intros simp: smc_cs_simps)
  
  show Comp_is_arr[intro]: "g ∘A⇘(∏SMCi∈∘I. 𝔄 i)⇙ f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c"
    if "g : b ↦⇘∏SMCi∈∘I. 𝔄 i⇙ c" and "f : a ↦⇘∏SMCi∈∘I. 𝔄 i⇙ b" 
    for g b c f a
  proof(intro smc_prod_is_arrI)
    from that show "vsv (g ∘A⇘smc_prod I 𝔄⇙ f)" 
      by (auto simp: smc_prod_Comp_app)
    from that show "𝒟∘ (g ∘A⇘smc_prod I 𝔄⇙ f) = I"
      by (auto simp: smc_prod_Comp_app)
    from that(2) have f: "f ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈"
      by (elim is_arrE) (auto simp: smc_prod_components)
    from that(1) have g: "g ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈"
      by (elim is_arrE) (auto simp: smc_prod_components)
    from f have a: "a ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Obj⦈"
      by (rule smc_prod_Dom_app_in_Obj[of f, unfolded is_arrD(2)[OF that(2)]])
    then show "vsv a" by (auto simp: smc_prod_components)
    from a show "𝒟∘ a = I" by (auto simp: smc_prod_components)
    from g have c: "c ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Obj⦈"
      by (rule smc_prod_Cod_app_in_Obj[of g, unfolded is_arrD(3)[OF that(1)]])
    then show "vsv c" by (auto simp: smc_prod_components)
    from c show "𝒟∘ c = I" by (auto simp: smc_prod_components)
    fix i assume prems: "i ∈∘ I"
    interpret semicategory α ‹𝔄 i› 
      using prems by (auto intro: smc_prod_cs_intros)
    from 
      prems 
      smc_prod_is_arrD(7)[OF that(1) prems] 
      smc_prod_is_arrD(7)[OF that(2) prems] 
    show "(g ∘A⇘smc_prod I 𝔄⇙ f)⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ c⦇i⦈"
      unfolding smc_prod_Comp_app[OF that] by (auto intro: smc_cs_intros)
  qed
  
  show 
    "h ∘A⇘smc_prod I 𝔄⇙ g ∘A⇘smc_prod I 𝔄⇙ f =
      h ∘A⇘smc_prod I 𝔄⇙ (g ∘A⇘smc_prod I 𝔄⇙ f)"
    if "h : c ↦⇘smc_prod I 𝔄⇙ d"
      and "g : b ↦⇘smc_prod I 𝔄⇙ c"
      and "f : a ↦⇘smc_prod I 𝔄⇙ b"
    for h c d g b f a
  proof(rule smc_prod_Arr_cong)
    show "(h ∘A⇘smc_prod I 𝔄⇙ g) ∘A⇘smc_prod I 𝔄⇙ f ∈∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈"
      by (meson that Comp_is_arr is_arrD)
    show "h ∘A⇘smc_prod I 𝔄⇙ (g ∘A⇘smc_prod I 𝔄⇙ f) ∈∘ smc_prod I 𝔄⦇Arr⦈"
      by (meson that Comp_is_arr is_arrD)
    fix i assume prems: "i ∈∘ I"
    then interpret semicategory α ‹𝔄 i› by (simp add: smc_prod_cs_intros)
    from prems that have "h⦇i⦈ : c⦇i⦈ ↦⇘𝔄 i⇙ d⦇i⦈"
      and "g⦇i⦈ : b⦇i⦈ ↦⇘𝔄 i⇙ c⦇i⦈"
      and "f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈"
      and "h ∘A⇘smc_prod I 𝔄⇙ g : b ↦⇘smc_prod I 𝔄⇙ d"
      and "g ∘A⇘smc_prod I 𝔄⇙ f : a ↦⇘smc_prod I 𝔄⇙ c"
      by (auto simp: smc_prod_is_arrD)
    with prems that show 
      "(h ∘A⇘smc_prod I 𝔄⇙ g ∘A⇘smc_prod I 𝔄⇙ f)⦇i⦈ =
        (h ∘A⇘smc_prod I 𝔄⇙ (g ∘A⇘smc_prod I 𝔄⇙ f))⦇i⦈"
      by (simp add: smc_prod_Comp_app_component smc_Comp_assoc)
  qed

qed (intro assms)



subsection‹Further local assumptions for product semicategories›


subsubsection‹Definition and elementary properties›

locale psemicategory = psemicategory_base α I 𝔄 for α I 𝔄 +
  assumes psmc_Obj_vsubset_Vset: 
    "J ⊆∘ I ⟹ (∏SMCi∈∘J. 𝔄 i)⦇Obj⦈ ⊆∘ Vset α"
    and psmc_Hom_vifunion_in_Vset: 
      "⟦
        J ⊆∘ I;
        A ⊆∘ (∏SMCi∈∘J. 𝔄 i)⦇Obj⦈;
        B ⊆∘ (∏SMCi∈∘J. 𝔄 i)⦇Obj⦈;
        A ∈∘ Vset α;
        B ∈∘ Vset α
      ⟧ ⟹ (⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏SMCi∈∘J. 𝔄 i) a b) ∈∘ Vset α"


text‹Rules.›

lemma (in psemicategory) psemicategory_axioms'[smc_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "psemicategory α' I' 𝔄"
  unfolding assms by (rule psemicategory_axioms)

mk_ide rf psemicategory_def[unfolded psemicategory_axioms_def]
  |intro psemicategoryI|
  |dest psemicategoryD[dest]|
  |elim psemicategoryE[elim]|

lemmas [smc_prod_cs_intros] = psemicategoryD(1)

lemma psemicategory_pdigraphI:
  assumes "pdigraph α I (λi. smc_dg (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ semicategory α (𝔄 i)"
  shows "psemicategory α I 𝔄"
proof-
  interpret pdigraph α I ‹λi. smc_dg (𝔄 i)› by (rule assms(1))
  note [unfolded slicing_simps slicing_commute, smc_cs_intros] = 
    pdg_Obj_vsubset_Vset
    pdg_Hom_vifunion_in_Vset
  show ?thesis
    by (intro psemicategoryI psemicategory_base_pdigraph_baseI)
      (auto simp: assms(2) dg_prod_cs_intros intro!: smc_cs_intros) 
qed


text‹Product semicategory is a product digraph.›

context psemicategory
begin

lemma psmc_pdigraph: "pdigraph α I (λi. smc_dg (𝔄 i))"
proof(intro pdigraphI, unfold slicing_simps slicing_commute)
  show "pdigraph_base α I (λi. smc_dg (𝔄 i))" by (rule psmc_pdigraph_base)
qed (auto intro!: psmc_Obj_vsubset_Vset psmc_Hom_vifunion_in_Vset)

interpretation pdg: pdigraph α I ‹λi. smc_dg (𝔄 i)› by (rule psmc_pdigraph)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  psmc_Obj_vsubset_Vset' = pdg.pdg_Obj_vsubset_Vset'
  and psmc_Hom_vifunion_in_Vset' = pdg.pdg_Hom_vifunion_in_Vset'
  and psmc_smc_prod_vunion_is_arr = pdg.pdg_dg_prod_vunion_is_arr
  and psmc_smc_prod_vdiff_vunion_is_arr = pdg.pdg_dg_prod_vdiff_vunion_is_arr

end


text‹Elementary properties.›

lemma (in psemicategory) psmc_vsubset_index_psemicategory:
  assumes "J ⊆∘ I"
  shows "psemicategory α J 𝔄"
proof(intro psemicategoryI psemicategory_pdigraphI)
  show "smc_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" if ‹J' ⊆∘ J› for J'
  proof-
    from that assms have "J' ⊆∘ I" by simp
    then show "smc_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" by (rule psmc_Obj_vsubset_Vset)
  qed
  fix A B J' assume prems:
    "J' ⊆∘ J"
    "A ⊆∘ (∏SMCi∈∘J'. 𝔄 i)⦇Obj⦈"
    "B ⊆∘ (∏SMCi∈∘J'. 𝔄 i)⦇Obj⦈"
    "A ∈∘ Vset α" 
    "B ∈∘ Vset α"
  show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏SMCi∈∘J'. 𝔄 i) a b) ∈∘ Vset α"
  proof-
    from prems(1) assms have "J' ⊆∘ I" by simp
    from psmc_Hom_vifunion_in_Vset[OF this prems(2-5)] show ?thesis.
  qed
qed (rule psmc_vsubset_index_psemicategory_base[OF assms])


subsubsection‹A product ‹α›-semicategory is an ‹α›-semicategory›

lemma (in psemicategory) psmc_semicategory_smc_prod: 
  "semicategory α (∏SMCi∈∘I. 𝔄 i)"
proof-
  interpret tiny_semicategory ‹α + ω› ‹∏SMCi∈∘I. 𝔄 i›
    by (intro psmc_tiny_semicategory_smc_prod) 
      (auto simp: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω)
  show ?thesis
    by (rule semicategory_if_semicategory)  
      (
        auto 
          intro!: psmc_Hom_vifunion_in_Vset psmc_Obj_vsubset_Vset
          intro: smc_cs_intros
      )
qed



subsection‹Local assumptions for a finite product semicategory›


subsubsection‹Definition and elementary properties›

locale finite_psemicategory = psemicategory_base α I 𝔄 for α I 𝔄 +
  assumes fin_psmc_index_vfinite: "vfinite I"


text‹Rules.›

lemma (in finite_psemicategory) finite_psemicategory_axioms[smc_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "finite_psemicategory α' I' 𝔄"
  unfolding assms by (rule finite_psemicategory_axioms)

mk_ide rf finite_psemicategory_def[unfolded finite_psemicategory_axioms_def]
  |intro finite_psemicategoryI|
  |dest finite_psemicategoryD[dest]|
  |elim finite_psemicategoryE[elim]|

lemmas [smc_prod_cs_intros] = finite_psemicategoryD(1)

lemma finite_psemicategory_finite_pdigraphI:
  assumes "finite_pdigraph α I (λi. smc_dg (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ semicategory α (𝔄 i)"
  shows "finite_psemicategory α I 𝔄"
proof-
  interpret finite_pdigraph α I ‹λi. smc_dg (𝔄 i)› by (rule assms(1))
  show ?thesis
    by 
      (
        intro 
          assms
          finite_psemicategoryI 
          psemicategory_base_pdigraph_baseI 
          finite_pdigraphD(1)[OF assms(1)]
          fin_pdg_index_vfinite
      )
qed


subsubsection‹
Local assumptions for a finite product semicategory and local
assumptions for an arbitrary product semicategory
›

sublocale finite_psemicategory ⊆ psemicategory α I 𝔄
proof-
  interpret finite_pdigraph α I ‹λi. smc_dg (𝔄 i)›
  proof(intro finite_pdigraphI pdigraph_baseI)
    fix i assume i: "i ∈∘ I"
    interpret 𝔄i: semicategory α ‹𝔄 i› by (simp add: i psmc_semicategories)
    show "digraph α (smc_dg (𝔄 i))" by (simp add: 𝔄i.smc_digraph)
  qed (auto intro!: smc_cs_intros fin_psmc_index_vfinite)
  show "psemicategory α I 𝔄"
    by (intro psemicategory_pdigraphI) 
      (simp_all add: psmc_semicategories pdigraph_axioms)
qed



subsection‹Binary union and complement›

lemma (in psemicategory) psmc_smc_prod_vunion_Comp:
  assumes "vdisjnt J K"
    and "J ⊆∘ I"
    and "K ⊆∘ I"
    and "g : b ↦⇘(∏SMCj∈∘J. 𝔄 j)⇙ c"
    and "g' : b' ↦⇘(∏SMCk∈∘K. 𝔄 k)⇙ c'"
    and "f : a ↦⇘(∏SMCj∈∘J. 𝔄 j)⇙ b"
    and "f' : a' ↦⇘(∏SMCk∈∘K. 𝔄 k)⇙ b'"
  shows "(g ∘A⇘(∏SMCj∈∘J. 𝔄 j)⇙ f) ∪∘ (g' ∘A⇘(∏SMCj∈∘K. 𝔄 j)⇙ f') = 
    g ∪∘ g' ∘A⇘(∏SMCj∈∘J ∪∘ K. 𝔄 j)⇙ f ∪∘ f'"
proof-

  interpret J𝔄: psemicategory α J 𝔄 
    using assms(2) by (simp add: psmc_vsubset_index_psemicategory)
  interpret K𝔄: psemicategory α K 𝔄 
    using assms(3) by (simp add: psmc_vsubset_index_psemicategory)
  interpret JK𝔄: psemicategory α ‹J ∪∘ K› 𝔄 
    using assms(2,3) by (simp add: psmc_vsubset_index_psemicategory)

  interpret J𝔄': semicategory α ‹smc_prod J 𝔄› 
    by (rule J𝔄.psmc_semicategory_smc_prod)
  interpret K𝔄': semicategory α ‹smc_prod K 𝔄› 
    by (rule K𝔄.psmc_semicategory_smc_prod)
  interpret JK𝔄': semicategory α ‹smc_prod (J ∪∘ K) 𝔄› 
    by (rule JK𝔄.psmc_semicategory_smc_prod)

  note gg' = psmc_smc_prod_vunion_is_arr[OF assms(1-3,4,5)]
    and ff' = psmc_smc_prod_vunion_is_arr[OF assms(1-3,6,7)]

  note gD = J𝔄.smc_prod_is_arrD[OF assms(4)]
    and g'D = K𝔄.smc_prod_is_arrD[OF assms(5)]
    and fD = J𝔄.smc_prod_is_arrD[OF assms(6)]
    and f'D = K𝔄.smc_prod_is_arrD[OF assms(7)]

  from assms(4,6) have gf: 
    "g ∘A⇘smc_prod J 𝔄⇙ f : a ↦⇘(∏SMCj∈∘J. 𝔄 j)⇙ c" 
    by (auto intro: smc_cs_intros)
  from assms(5,7) have g'f': 
    "g' ∘A⇘smc_prod K 𝔄⇙ f' : a' ↦⇘(∏SMCk∈∘K. 𝔄 k)⇙ c'"
    by (auto intro: smc_cs_intros)
  from gf have "g ∘A⇘smc_prod J 𝔄⇙ f ∈∘ smc_prod J 𝔄⦇Arr⦈" by auto
  from g'f' have "g' ∘A⇘smc_prod K 𝔄⇙ f' ∈∘ smc_prod K 𝔄⦇Arr⦈" by auto
  from gg' ff' have gg'_ff': 
    "g ∪∘ g' ∘A⇘smc_prod (J ∪∘ K) 𝔄⇙ f ∪∘ f' :
      a ∪∘ a' ↦⇘smc_prod (J ∪∘ K) 𝔄⇙ c ∪∘ c'"
    by (simp add: smc_cs_intros)

  show ?thesis
  proof(rule smc_prod_Arr_cong[of _ ‹J ∪∘ K› 𝔄])
    from gf g'f' assms(1) show 
      "(g ∘A⇘smc_prod J 𝔄⇙ f) ∪∘ (g' ∘A⇘smc_prod K 𝔄⇙ f') ∈∘ 
        smc_prod (J ∪∘ K) 𝔄⦇Arr⦈"
      by (auto intro: smc_prod_vunion_Arr_in_Arr)
    from gg'_ff' show 
      "g ∪∘ g' ∘A⇘smc_prod (J ∪∘ K) 𝔄⇙ f ∪∘ f' ∈∘ smc_prod (J ∪∘ K) 𝔄⦇Arr⦈"
      by auto
    fix i assume prems: "i ∈∘ J ∪∘ K"
    then consider (iJ) ‹i ∈∘ J› | (iK) ‹i ∈∘ K› by auto
    then show 
      "((g ∘A⇘smc_prod J 𝔄⇙ f) ∪∘ (g' ∘A⇘smc_prod K 𝔄⇙ f'))⦇i⦈ =
        (g ∪∘ g' ∘A⇘smc_prod (J ∪∘ K) 𝔄⇙ f ∪∘ f')⦇i⦈"
    proof cases
      case iJ
      have [simp]:
        "((g ∘A⇘smc_prod J 𝔄⇙ f) ∪∘ (g' ∘A⇘smc_prod K 𝔄⇙ f'))⦇i⦈ = 
          g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈"
      proof
        (
          fold smc_prod_Comp_app_component[OF assms(4,6) iJ], 
          rule vsv_vunion_app_left
        )
        from gf show "vsv (g ∘A⇘smc_prod J 𝔄⇙ f)" by auto
        from g'f' show "vsv (g' ∘A⇘smc_prod K 𝔄⇙ f')" by auto
      qed 
        (
          use assms(4-7) in 
            ‹simp_all add: iJ assms(1) smc_prod_Comp_app_vdomain›
        )
      have gg'_i: "(g ∪∘ g')⦇i⦈ = g⦇i⦈" 
        by (simp add: iJ assms(1) gD(1,2) g'D(1,2))
      have ff'_i: "(f ∪∘ f')⦇i⦈ = f⦇i⦈" 
        by (simp add: iJ assms(1) fD(1,2) f'D(1,2))
      have [simp]: 
        "(g ∪∘ g' ∘A⇘smc_prod (J ∪∘ K) 𝔄⇙ f ∪∘ f')⦇i⦈ = g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈" 
        by (fold gg'_i ff'_i) 
          (rule smc_prod_Comp_app_component[OF gg' ff' prems])
      show ?thesis by simp
    next
      case iK
      have [simp]:
        "((g ∘A⇘smc_prod J 𝔄⇙ f) ∪∘ (g' ∘A⇘smc_prod K 𝔄⇙ f'))⦇i⦈ = 
          g'⦇i⦈ ∘A⇘𝔄 i⇙ f'⦇i⦈"
      proof
        (
          fold smc_prod_Comp_app_component[OF assms(5,7) iK], 
          rule vsv_vunion_app_right
        )
        from gf show "vsv (g ∘A⇘smc_prod J 𝔄⇙ f)" by auto
        from g'f' show "vsv (g' ∘A⇘smc_prod K 𝔄⇙ f')" by auto
      qed 
        (
          use assms(4-7) in 
            ‹simp_all add: iK smc_prod_Comp_app_vdomain assms(1)›
        )
      have gg'_i: "(g ∪∘ g')⦇i⦈ = g'⦇i⦈" 
        by (simp add: iK assms(1) gD(1,2) g'D(1,2))
      have ff'_i: "(f ∪∘ f')⦇i⦈ = f'⦇i⦈" 
        by (simp add: iK assms(1) fD(1,2) f'D(1,2))
      have [simp]:
        "(g ∪∘ g' ∘A⇘smc_prod (J ∪∘ K) 𝔄⇙ f ∪∘ f')⦇i⦈ = g'⦇i⦈ ∘A⇘𝔄 i⇙ f'⦇i⦈" 
        by (fold gg'_i ff'_i)
          (rule smc_prod_Comp_app_component[OF gg' ff' prems])
      show ?thesis by simp
    qed
  qed

qed

lemma (in psemicategory) psmc_smc_prod_vdiff_vunion_Comp:
  assumes "J ⊆∘ I"   
    and "g : b ↦⇘(∏SMCj∈∘I -∘ J. 𝔄 j)⇙ c"
    and "g' : b' ↦⇘(∏SMCk∈∘J. 𝔄 k)⇙ c'"
    and "f : a ↦⇘(∏SMCj∈∘I -∘ J. 𝔄 j)⇙ b"
    and "f' : a' ↦⇘(∏SMCk∈∘J. 𝔄 k)⇙ b'"
  shows "(g ∘A⇘(∏SMCj∈∘I -∘ J. 𝔄 j)⇙ f) ∪∘ (g' ∘A⇘(∏SMCj∈∘J. 𝔄 j)⇙ f') = 
    g ∪∘ g' ∘A⇘(∏SMCj∈∘I. 𝔄 j)⇙ f ∪∘ f'"
  by 
    (
      vdiff_of_vunion' 
        rule: psmc_smc_prod_vunion_Comp assms: assms(2-5) subset: assms(1)
    )



subsection‹Projection›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-3 in cite‹"mac_lane_categories_2010"›.›

definition smcf_proj :: "V ⇒ (V ⇒ V) ⇒ V ⇒ V" (‹πSMC›)
  where "πSMC I 𝔄 i =
    [
      (λa∈∘(∏∘i∈∘I. 𝔄 i⦇Obj⦈). a⦇i⦈),
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). f⦇i⦈),
      (∏SMCi∈∘I. 𝔄 i),
      𝔄 i
    ]∘"


text‹Components.›

lemma smcf_proj_components:
  shows "(πSMC I 𝔄 i)⦇ObjMap⦈ = (λa∈∘(∏∘i∈∘I. 𝔄 i⦇Obj⦈). a⦇i⦈)"
    and "(πSMC I 𝔄 i)⦇ArrMap⦈ = (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). f⦇i⦈)"
    and "(πSMC I 𝔄 i)⦇HomDom⦈ = (∏SMCi∈∘I. 𝔄 i)"
    and "(πSMC I 𝔄 i)⦇HomCod⦈ = 𝔄 i"
  unfolding smcf_proj_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing›

lemma smcf_dghm_smcf_proj[slicing_commute]: 
  "πDG I (λi. smc_dg (𝔄 i)) i = smcf_dghm (πSMC I 𝔄 i)"
  unfolding 
    smc_dg_def 
    smcf_dghm_def 
    smcf_proj_def 
    dghm_proj_def 
    smc_prod_def 
    dg_prod_def
    dg_field_simps 
    dghm_field_simps 
  by (simp add: nat_omega_simps)

context psemicategory
begin

interpretation pdg: pdigraph α I ‹λi. smc_dg (𝔄 i)› by (rule psmc_pdigraph)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  smcf_proj_is_dghm = pdg.pdg_dghm_proj_is_dghm

end


subsubsection‹Projection semifunctor is a semifunctor›

lemma (in psemicategory) psmc_smcf_proj_is_semifunctor: 
  assumes "i ∈∘ I"
  shows "πSMC I 𝔄 i : (∏SMCi∈∘I. 𝔄 i) ↦↦SMC⇘α⇙ 𝔄 i"
proof(intro is_semifunctorI)
  show "vfsequence (πSMC I 𝔄 i)"
    unfolding smcf_proj_def by (simp add: nat_omega_simps)
  show "vcard (πSMC I 𝔄 i) = 4ℕ"
    unfolding smcf_proj_def by (simp add: nat_omega_simps)
  interpret 𝔄: semicategory α ‹smc_prod I 𝔄› 
    by (rule psmc_semicategory_smc_prod)
  interpret 𝔄i: semicategory α ‹𝔄 i› 
    using assms by (simp add: smc_prod_cs_intros)
  show "πSMC I 𝔄 i⦇ArrMap⦈⦇g ∘A⇘smc_prod I 𝔄⇙ f⦈ =
    πSMC I 𝔄 i⦇ArrMap⦈⦇g⦈ ∘A⇘𝔄 i⇙ πSMC I 𝔄 i⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘smc_prod I 𝔄⇙ c" and "f : a ↦⇘smc_prod I 𝔄⇙ b" for g b c f a
  proof-
    from that have "g ∘A⇘smc_prod I 𝔄⇙ f : a ↦⇘smc_prod I 𝔄⇙ c" 
      by (auto simp: smc_cs_intros)
    then have "g ∘A⇘smc_prod I 𝔄⇙ f ∈∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
      unfolding smc_prod_components[symmetric] by auto
    then have π_gf: "πSMC I 𝔄 i⦇ArrMap⦈⦇g ∘A⇘smc_prod I 𝔄⇙ f⦈ = g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈"
      unfolding smcf_proj_components 
      by (simp add: smc_prod_Comp_app_component[OF that assms])
    from that(1) have g: "g ∈∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)" 
      unfolding smc_prod_components[symmetric] by auto
    from that(2) have f: "f ∈∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)" 
      unfolding smc_prod_components[symmetric] by auto
    from g f have πg_πf: 
      "πSMC I 𝔄 i⦇ArrMap⦈⦇g⦈ ∘A⇘𝔄 i⇙ πSMC I 𝔄 i⦇ArrMap⦈⦇f⦈ = g⦇i⦈ ∘A⇘𝔄 i⇙ f⦇i⦈"
      unfolding smcf_proj_components by simp
    from π_gf πg_πf show ?thesis by simp
  qed
qed 
  (
    auto simp:
      smc_prod_cs_intros
      assms
      smcf_proj_components
      psmc_semicategory_smc_prod 
      smcf_proj_is_dghm
  )

lemma (in psemicategory) psmc_smcf_proj_is_semifunctor':
  assumes "i ∈∘ I" and "ℭ = (∏SMCi∈∘I. 𝔄 i)" and "𝔇 = 𝔄 i"
  shows "πSMC I 𝔄 i : ℭ ↦↦SMC⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule psmc_smcf_proj_is_semifunctor)

lemmas [smc_cs_intros] = psemicategory.psmc_smcf_proj_is_semifunctor'



subsection‹Semicategory product universal property semifunctor›


subsubsection‹Definition and elementary properties›


text‹
The following semifunctor is used in the 
proof of the universal property of the product semicategory 
later in this work.
›

definition smcf_up :: "V ⇒ (V ⇒ V) ⇒ V ⇒ (V ⇒ V) ⇒ V"
  where "smcf_up I 𝔄 ℭ φ =
    [
      (λa∈∘ℭ⦇Obj⦈. (λi∈∘I. φ i⦇ObjMap⦈⦇a⦈)),
      (λf∈∘ℭ⦇Arr⦈. (λi∈∘I. φ i⦇ArrMap⦈⦇f⦈)),
      ℭ,
      (∏SMCi∈∘I. 𝔄 i)
    ]∘"


text‹Components.›

lemma smcf_up_components: 
  shows "smcf_up I 𝔄 ℭ φ⦇ObjMap⦈ = (λa∈∘ℭ⦇Obj⦈. (λi∈∘I. φ i⦇ObjMap⦈⦇a⦈))"
    and "smcf_up I 𝔄 ℭ φ⦇ArrMap⦈ = (λf∈∘ℭ⦇Arr⦈. (λi∈∘I. φ i⦇ArrMap⦈⦇f⦈))"
    and "smcf_up I 𝔄 ℭ φ⦇HomDom⦈ = ℭ"
    and "smcf_up I 𝔄 ℭ φ⦇HomCod⦈ = (∏SMCi∈∘I. 𝔄 i)"
  unfolding smcf_up_def dghm_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smcf_dghm_smcf_up[slicing_commute]: 
  "dghm_up I (λi. smc_dg (𝔄 i)) (smc_dg ℭ) (λi. smcf_dghm (φ i)) = 
    smcf_dghm (smcf_up I 𝔄 ℭ φ)"
  unfolding 
    smc_dg_def 
    smcf_dghm_def 
    smcf_up_def 
    dghm_up_def 
    smc_prod_def 
    dg_prod_def
    dg_field_simps 
    dghm_field_simps 
  by (simp add: nat_omega_simps)

context
  fixes 𝔄 φ :: "V ⇒ V"
    and ℭ :: V
begin

lemmas_with 
  [
    where 𝔄=‹λi. smc_dg (𝔄 i)› and φ=‹λi. smcf_dghm (φ i)› and ℭ=‹smc_dg ℭ›, 
    unfolded slicing_simps slicing_commute
  ]:
  smcf_up_ObjMap_vdomain[smc_cs_simps] = dghm_up_ObjMap_vdomain
  and smcf_up_ObjMap_app = dghm_up_ObjMap_app
  and smcf_up_ObjMap_app_vdomain[smc_cs_simps] = dghm_up_ObjMap_app_vdomain
  and smcf_up_ObjMap_app_component[smc_cs_simps] = dghm_up_ObjMap_app_component
  and smcf_up_ArrMap_vdomain[smc_cs_simps] = dghm_up_ArrMap_vdomain
  and smcf_up_ArrMap_app = dghm_up_ArrMap_app
  and smcf_up_ArrMap_app_vdomain[smc_cs_simps] = dghm_up_ArrMap_app_vdomain
  and smcf_up_ArrMap_app_component[smc_cs_simps] = dghm_up_ArrMap_app_component

lemma smcf_up_ObjMap_vrange:
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i"
  shows "ℛ∘ (smcf_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆∘ (∏SMCi∈∘I. 𝔄 i)⦇Obj⦈"
proof
  (
    rule dghm_up_ObjMap_vrange
      [
        where 𝔄=‹λi. smc_dg (𝔄 i)› 
          and φ=‹λi. smcf_dghm (φ i)› 
          and ℭ=‹smc_dg ℭ›, 
        unfolded slicing_simps slicing_commute
      ]
  )
  fix i assume "i ∈∘ I"
  then interpret is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
  show "smcf_dghm (φ i) : smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (𝔄 i)" 
    by (rule smcf_is_dghm)
qed

lemma smcf_up_ObjMap_app_vrange:
  assumes "a ∈∘ ℭ⦇Obj⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i"
  shows " ℛ∘ (smcf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Obj⦈)"
proof
  (
    rule dghm_up_ObjMap_app_vrange
      [
        where 𝔄=‹λi. smc_dg (𝔄 i)› 
          and φ=‹λi. smcf_dghm (φ i)› 
          and ℭ=‹smc_dg ℭ›, 
        unfolded slicing_simps slicing_commute
      ]
  )
  show "a ∈∘ ℭ⦇Obj⦈" by (rule assms)
  fix i assume "i ∈∘ I"
  then interpret is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
  show "smcf_dghm (φ i) : smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (𝔄 i)"
    by (rule smcf_is_dghm)
qed

lemma smcf_up_ArrMap_vrange:
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i"
  shows "ℛ∘ (smcf_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆∘ (∏SMCi∈∘I. 𝔄 i)⦇Arr⦈"
proof
  (
    rule dghm_up_ArrMap_vrange
      [
        where 𝔄=‹λi. smc_dg (𝔄 i)› 
          and φ=‹λi. smcf_dghm (φ i)› 
          and ℭ=‹smc_dg ℭ›, 
        unfolded slicing_simps slicing_commute
      ]
  )
  fix i assume "i ∈∘ I"
  then interpret is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
  show "smcf_dghm (φ i) : smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (𝔄 i)"
    by (rule smcf_is_dghm)
qed

lemma smcf_up_ArrMap_app_vrange:
  assumes "a ∈∘ ℭ⦇Arr⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i"
  shows "ℛ∘ (smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Arr⦈)"
proof
  (
    rule dghm_up_ArrMap_app_vrange[
      where 𝔄=‹λi. smc_dg (𝔄 i)› 
        and φ=‹λi. smcf_dghm (φ i)› 
        and ℭ=‹smc_dg ℭ›, 
      unfolded slicing_simps slicing_commute
      ]
  )
  show "a ∈∘ ℭ⦇Arr⦈" by (rule assms)
  fix i assume "i ∈∘ I"
  then interpret is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
  show "smcf_dghm (φ i) : smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (𝔄 i)"
    by (rule smcf_is_dghm)
qed

end

context psemicategory
begin

interpretation pdg: pdigraph α I ‹λi. smc_dg (𝔄 i)› by (rule psmc_pdigraph)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  psmc_dghm_comp_dghm_proj_dghm_up = pdg.pdg_dghm_comp_dghm_proj_dghm_up
  and psmc_dghm_up_eq_dghm_proj = pdg.pdg_dghm_up_eq_dghm_proj

end


subsubsection‹
Semicategory product universal property semifunctor is a semifunctor
›

lemma (in psemicategory) psmc_smcf_up_is_semifunctor:
  assumes "semicategory α ℭ" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i"
  shows "smcf_up I 𝔄 ℭ φ : ℭ ↦↦SMC⇘α⇙ (∏SMCi∈∘I. 𝔄 i)"
proof(intro is_semifunctorI)
  interpret ℭ: semicategory α ℭ by (simp add: assms(1))
  interpret 𝔄: semicategory α ‹smc_prod I 𝔄› 
    by (rule psmc_semicategory_smc_prod)
  show "vfsequence (smcf_up I 𝔄 ℭ φ)"
    unfolding smcf_up_def by simp
  show "vcard (smcf_up I 𝔄 ℭ φ) = 4ℕ"
    unfolding smcf_up_def by (simp add: nat_omega_simps)
  show dghm_smcf_up: 
    "smcf_dghm (smcf_up I 𝔄 ℭ φ) : smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (smc_prod I 𝔄)"
    by 
      (
        simp add: 
          assms 
          slicing_commute[symmetric]
          psmc_pdigraph 
          is_semifunctor.smcf_is_dghm 
          pdigraph.pdg_dghm_up_is_dghm 
          semicategory.smc_digraph
      )
  interpret smcf_up:
    is_dghm α ‹smc_dg ℭ› ‹smc_dg (smc_prod I 𝔄)› ‹smcf_dghm (smcf_up I 𝔄 ℭ φ)›
    by (rule dghm_smcf_up)
  show "smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ = 
    smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g⦈ ∘A⇘smc_prod I 𝔄⇙ smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for g b c f a
  proof(rule smc_prod_Arr_cong[of _ I 𝔄])
    note smcf_up_f = 
        smcf_up.dghm_ArrMap_is_arr[unfolded slicing_simps, OF that(2)]
      and smcf_up_g = 
        smcf_up.dghm_ArrMap_is_arr[unfolded slicing_simps, OF that(1)]
    from that have gf: "g ∘A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c" 
      by (simp add: smc_cs_intros)
    from smcf_up.dghm_ArrMap_is_arr[unfolded slicing_simps, OF this] show
      "smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ ∈∘ smc_prod I 𝔄⦇Arr⦈" 
      by (simp add: smc_cs_intros)
    from smcf_up_g smcf_up_f show 
      "smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g⦈ ∘A⇘smc_prod I 𝔄⇙ smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇f⦈ ∈∘ 
        smc_prod I 𝔄⦇Arr⦈"
      by (meson 𝔄.smc_is_arrE 𝔄.smc_Comp_is_arr)
    fix i assume prems: "i ∈∘ I"
    from gf have gf': "g ∘A⇘ℭ⇙ f ∈∘ ℭ⦇Arr⦈" by (simp add: smc_cs_intros)
    from that have g: "g ∈∘ ℭ⦇Arr⦈" and f: "f ∈∘ ℭ⦇Arr⦈" by auto
    interpret φ: is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF prems])
    from that show "smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈⦇i⦈ = 
      (
        smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇g⦈ ∘A⇘smc_prod I 𝔄⇙ smcf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇f⦈
      )⦇i⦈"
      unfolding 
        smcf_up_ArrMap_app_component[OF gf' prems]
        smc_prod_Comp_app_component[OF smcf_up_g smcf_up_f prems]
        smcf_up_ArrMap_app_component[OF g prems]
        smcf_up_ArrMap_app_component[OF f prems]
      by (rule φ.smcf_ArrMap_Comp)
  qed
qed (auto simp: assms(1) psmc_semicategory_smc_prod smcf_up_components)


subsubsection‹Further properties›

lemma (in psemicategory) psmc_Comp_smcf_proj_smcf_up: 
  assumes "semicategory α ℭ" 
    and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i" 
    and "i ∈∘ I" 
  shows "φ i = πSMC I 𝔄 i ∘SMCF smcf_up I 𝔄 ℭ φ"
proof(rule smcf_dghm_eqI)
  interpret φ: is_semifunctor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF assms(3)])
  interpret π: is_semifunctor α ‹smc_prod I 𝔄› ‹𝔄 i› ‹πSMC I 𝔄 i›
    by (simp add: assms(3) psmc_smcf_proj_is_semifunctor)
  interpret up: is_semifunctor α ℭ ‹smc_prod I 𝔄› ‹smcf_up I 𝔄 ℭ φ›
    by 
      (
        simp add: 
          assms(2) φ.HomDom.semicategory_axioms psmc_smcf_up_is_semifunctor
      )
  show "φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i" by (simp add: smc_cs_intros)
  show "πSMC I 𝔄 i ∘SMCF smcf_up I 𝔄 ℭ φ : ℭ ↦↦SMC⇘α⇙ 𝔄 i" 
      by (auto intro: smc_cs_intros)
  from assms show 
    "smcf_dghm (φ i) = smcf_dghm (πSMC I 𝔄 i ∘SMCF smcf_up I 𝔄 ℭ φ)"
    unfolding slicing_simps[symmetric] slicing_commute[symmetric]
    by 
      (
        intro 
          psmc_dghm_comp_dghm_proj_dghm_up
            [
              where φ=‹λi. smcf_dghm (φ i)›, 
              unfolded slicing_simps[symmetric] slicing_commute[symmetric]
            ]
      )
      (auto simp: is_semifunctor.smcf_is_dghm)
qed simp_all

lemma (in psemicategory) psmc_smcf_up_eq_smcf_proj:
  assumes "𝔉 : ℭ ↦↦SMC⇘α⇙ (∏SMCi∈∘I. 𝔄 i)"
    and "⋀i. i ∈∘ I ⟹ φ i = πSMC I 𝔄 i ∘SMCF 𝔉"
  shows "smcf_up I 𝔄 ℭ φ = 𝔉"
proof(rule smcf_dghm_eqI)
  interpret 𝔉: is_semifunctor α ℭ ‹(∏SMCi∈∘I. 𝔄 i)› 𝔉 by (rule assms(1))
  show "smcf_up I 𝔄 ℭ φ : ℭ ↦↦SMC⇘α⇙ (∏SMCi∈∘I. 𝔄 i)"
  proof(rule psmc_smcf_up_is_semifunctor)
    fix i assume prems: "i ∈∘ I"
    interpret π: is_semifunctor α ‹(∏SMCi∈∘I. 𝔄 i)› ‹𝔄 i› ‹πSMC I 𝔄 i›
      using prems by (rule psmc_smcf_proj_is_semifunctor)
    show "φ i : ℭ ↦↦SMC⇘α⇙ 𝔄 i" 
      unfolding assms(2)[OF prems] by (auto intro: smc_cs_intros)
  qed (auto intro: smc_cs_intros)
  show "𝔉 : ℭ ↦↦SMC⇘α⇙ (∏SMCi∈∘I. 𝔄 i)" by (rule assms(1))
  from assms show "smcf_dghm (smcf_up I 𝔄 ℭ φ) = smcf_dghm 𝔉"
    unfolding slicing_simps[symmetric] slicing_commute[symmetric]
    by (intro psmc_dghm_up_eq_dghm_proj) 
      (auto simp: slicing_simps slicing_commute)
qed simp_all



subsection‹Singleton semicategory›


subsubsection‹Slicing›

context
  fixes ℭ :: V
begin

lemmas_with [where ℭ=‹smc_dg ℭ›, unfolded slicing_simps slicing_commute]:
  smc_singleton_ObjI = dg_singleton_ObjI
  and smc_singleton_ObjE = dg_singleton_ObjE
  and smc_singleton_ArrI = dg_singleton_ArrI
  and smc_singleton_ArrE = dg_singleton_ArrE

end

context semicategory
begin

interpretation dg: digraph α ‹smc_dg ℭ› by (rule smc_digraph)

lemmas_with [unfolded slicing_simps slicing_commute]:
  smc_finite_pdigraph_smc_singleton = dg.dg_finite_pdigraph_dg_singleton
  and smc_singleton_is_arrI = dg.dg_singleton_is_arrI
  and smc_singleton_is_arrD = dg.dg_singleton_is_arrD
  and smc_singleton_is_arrE = dg.dg_singleton_is_arrE

end


subsubsection‹Singleton semicategory is a semicategory›

lemma (in semicategory) smc_finite_psemicategory_smc_singleton: 
  assumes "j ∈∘ Vset α"
  shows "finite_psemicategory α (set {j}) (λi. ℭ)"
  by 
    (
      auto intro: 
        assms
        semicategory_axioms 
        finite_psemicategory_finite_pdigraphI 
        smc_finite_pdigraph_smc_singleton 
    )

lemma (in semicategory) smc_semicategory_smc_singleton:
  assumes "j ∈∘ Vset α"
  shows "semicategory α (∏SMCi∈∘set {j}. ℭ)"
proof-
  interpret finite_psemicategory α ‹set {j}› ‹λi. ℭ›
    using assms by (rule smc_finite_psemicategory_smc_singleton)
  show ?thesis by (rule psmc_semicategory_smc_prod)
qed



subsection‹Singleton semifunctor›


subsubsection‹Definition and elementary properties›

definition smcf_singleton :: "V ⇒ V ⇒ V"
  where "smcf_singleton j ℭ =
    [
      (λa∈∘ℭ⦇Obj⦈. set {⟨j, a⟩}),
      (λf∈∘ℭ⦇Arr⦈. set {⟨j, f⟩}),
      ℭ,
      (∏SMCi∈∘set {j}. ℭ)
    ]∘"


text‹Components.›

lemma smcf_singleton_components:
  shows "smcf_singleton j ℭ⦇ObjMap⦈ = (λa∈∘ℭ⦇Obj⦈. set {⟨j, a⟩})"
    and "smcf_singleton j ℭ⦇ArrMap⦈ = (λf∈∘ℭ⦇Arr⦈. set {⟨j, f⟩})"
    and "smcf_singleton j ℭ⦇HomDom⦈ = ℭ"
    and "smcf_singleton j ℭ⦇HomCod⦈ = (∏SMCi∈∘set {j}. ℭ)"
  unfolding smcf_singleton_def dghm_field_simps 
  by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma smcf_dghm_smcf_singleton[slicing_commute]: 
  "dghm_singleton j (smc_dg ℭ)= smcf_dghm (smcf_singleton j ℭ)"
  unfolding dghm_singleton_def smcf_singleton_def slicing_simps slicing_commute
  by 
    (
      simp add: 
        nat_omega_simps dghm_field_simps dg_field_simps smc_dg_def smcf_dghm_def
     )

context
  fixes ℭ :: V
begin

lemmas_with [where ℭ=‹smc_dg ℭ›, unfolded slicing_simps slicing_commute]:
  smcf_singleton_ObjMap_vsv[smc_cs_intros] = dghm_singleton_ObjMap_vsv
  and smcf_singleton_ObjMap_vdomain[smc_cs_simps] = 
    dghm_singleton_ObjMap_vdomain
  and smcf_singleton_ObjMap_vrange = dghm_singleton_ObjMap_vrange
  and smcf_singleton_ObjMap_app[smc_prod_cs_simps] = dghm_singleton_ObjMap_app
  and smcf_singleton_ArrMap_vsv[smc_cs_intros] = dghm_singleton_ArrMap_vsv
  and smcf_singleton_ArrMap_vdomain[smc_cs_simps] = 
    dghm_singleton_ArrMap_vdomain
  and smcf_singleton_ArrMap_vrange = dghm_singleton_ArrMap_vrange
  and smcf_singleton_ArrMap_app[smc_prod_cs_simps] = dghm_singleton_ArrMap_app

end

context semicategory
begin

interpretation dg: digraph α ‹smc_dg ℭ› by (rule smc_digraph)

lemmas_with [unfolded slicing_simps slicing_commute]:
  smc_smcf_singleton_is_dghm = dg.dg_dghm_singleton_is_dghm

end


subsubsection‹Singleton semifunctor is an isomorphism of semicategories›

lemma (in semicategory) smc_smcf_singleton_is_iso_semifunctor:
  assumes "j ∈∘ Vset α"
  shows "smcf_singleton j ℭ : ℭ ↦↦SMC.iso⇘α⇙ (∏SMCi∈∘set {j}. ℭ)"
proof(intro is_iso_semifunctorI is_semifunctorI)
  show dghm_singleton: 
    "smcf_dghm (smcf_singleton j ℭ) :
      smc_dg ℭ ↦↦DG.iso⇘α⇙ smc_dg (∏SMCi∈∘set {j}. ℭ)"
    by (rule smc_smcf_singleton_is_dghm[OF assms, unfolded slicing_simps])
  show "vfsequence (smcf_singleton j ℭ)" unfolding smcf_singleton_def by simp
  show "vcard (smcf_singleton j ℭ) = 4ℕ"
    unfolding smcf_singleton_def by (simp add: nat_omega_simps)
  from dghm_singleton show 
    "smcf_dghm (smcf_singleton j ℭ) :
      smc_dg ℭ ↦↦DG⇘α⇙ smc_dg (∏SMCi∈∘set {j}. ℭ)"
    by (simp add: is_iso_dghm.axioms(1))
  show "smcf_singleton j ℭ⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ =
    smcf_singleton j ℭ⦇ArrMap⦈⦇g⦈ ∘A⇘∏SMCi∈∘set {j}. ℭ⇙
    smcf_singleton j ℭ⦇ArrMap⦈⦇f⦈"
    if "g : b ↦⇘ℭ⇙ c" and "f : a ↦⇘ℭ⇙ b" for g b c f a
  proof-
    let ?jg = ‹smcf_singleton j ℭ⦇ArrMap⦈⦇g⦈›
      and ?jf = ‹smcf_singleton j ℭ⦇ArrMap⦈⦇f⦈›
    from that have [simp]: "?jg = set {⟨j, g⟩}" "?jf = set {⟨j, f⟩}"
       by (simp_all add: smcf_singleton_ArrMap_app smc_cs_intros)
     from that have "g ∘A⇘ℭ⇙ f : a ↦⇘ℭ⇙ c" by (auto intro: smc_cs_intros)
    then have "smcf_singleton j ℭ⦇ArrMap⦈⦇g ∘A⇘ℭ⇙ f⦈ = set {⟨j, g ∘A⇘ℭ⇙ f⟩}"
      by (simp_all add: smcf_singleton_ArrMap_app smc_cs_intros)
    moreover from 
      smc_singleton_is_arrI[OF assms that(1)]
      smc_singleton_is_arrI[OF assms that(2)] 
    have "?jg ∘A⇘∏SMCi∈∘set {j}. ℭ⇙ ?jf = set {⟨j, g ∘A⇘ℭ⇙ f⟩}"
      by (simp add: smc_prod_Comp_app VLambda_vsingleton)
    ultimately show ?thesis by auto
  qed
qed 
  (
    auto intro:
      smc_cs_intros
      assms 
      smc_semicategory_smc_singleton 
      smcf_singleton_components 
  )

lemmas [smc_cs_intros] = semicategory.smc_smcf_singleton_is_iso_semifunctor



subsection‹Product of two semicategories›


subsubsection‹Definition and elementary properties.›


text‹See Chapter II-3 in cite‹"mac_lane_categories_2010"›.›

definition smc_prod_2 :: "V ⇒ V ⇒ V" (infixr ‹×SMC› 80)
  where "𝔄 ×SMC 𝔅 ≡ smc_prod (2ℕ) (λi. (i = 0 ? 𝔄 : 𝔅))"


text‹Slicing.›
  
lemma smc_dg_smc_prod_2[slicing_commute]: 
  "smc_dg 𝔄 ×DG smc_dg 𝔅 = smc_dg (𝔄 ×SMC 𝔅)"
  unfolding smc_prod_2_def dg_prod_2_def slicing_commute[symmetric] if_distrib
  by simp

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)

lemmas_with 
  [
    where 𝔄=‹smc_dg 𝔄› and 𝔅=‹smc_dg 𝔅›, 
    unfolded slicing_simps slicing_commute, 
    OF 𝔄.smc_digraph 𝔅.smc_digraph
  ]:
  smc_prod_2_ObjI = dg_prod_2_ObjI 
  and smc_prod_2_ObjI'[smc_prod_cs_intros] = dg_prod_2_ObjI'
  and smc_prod_2_ObjE = dg_prod_2_ObjE
  and smc_prod_2_ArrI = dg_prod_2_ArrI
  and smc_prod_2_ArrI'[smc_prod_cs_intros] = dg_prod_2_ArrI'
  and smc_prod_2_ArrE = dg_prod_2_ArrE
  and smc_prod_2_is_arrI = dg_prod_2_is_arrI
  and smc_prod_2_is_arrI'[smc_prod_cs_intros] = dg_prod_2_is_arrI'
  and smc_prod_2_is_arrE = dg_prod_2_is_arrE
  and smc_prod_2_Dom_vsv = dg_prod_2_Dom_vsv
  and smc_prod_2_Dom_vdomain[smc_cs_simps] = dg_prod_2_Dom_vdomain
  and smc_prod_2_Dom_app[smc_prod_cs_simps] = dg_prod_2_Dom_app
  and smc_prod_2_Dom_vrange = dg_prod_2_Dom_vrange
  and smc_prod_2_Cod_vsv = dg_prod_2_Cod_vsv
  and smc_prod_2_Cod_vdomain[smc_cs_simps] = dg_prod_2_Cod_vdomain
  and smc_prod_2_Cod_app[smc_prod_cs_simps] = dg_prod_2_Cod_app
  and smc_prod_2_Cod_vrange = dg_prod_2_Cod_vrange
  and smc_prod_2_op_smc_smc_Obj[smc_op_simps] = dg_prod_2_op_dg_dg_Obj
  and smc_prod_2_smc_op_smc_Obj[smc_op_simps] = dg_prod_2_dg_op_dg_Obj
  and smc_prod_2_op_smc_smc_Arr[smc_op_simps] = dg_prod_2_op_dg_dg_Arr
  and smc_prod_2_smc_op_smc_Arr[smc_op_simps] = dg_prod_2_dg_op_dg_Arr

end


subsubsection‹Product of two semicategories is a semicategory›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])
interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)

lemma finite_psemicategory_smc_prod_2: 
  "finite_psemicategory α (2ℕ) (if2 𝔄 𝔅)"
proof(intro finite_psemicategoryI psemicategory_baseI)
  from Axiom_of_Infinity show z1_in_Vset: "2ℕ ∈∘ Vset α" by blast
  show "semicategory α (i = 0 ? 𝔄 : 𝔅)" if "i ∈∘ 2ℕ" for i
    by (auto simp: smc_cs_intros)
qed auto

interpretation finite_psemicategory α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_psemicategory_smc_prod_2 𝔄 𝔅)

lemma semicategory_smc_prod_2[smc_cs_intros]: "semicategory α (𝔄 ×SMC 𝔅)"
  unfolding smc_prod_2_def by (rule psmc_semicategory_smc_prod)

end


subsubsection‹Composition›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])

interpretation finite_psemicategory α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_psemicategory_smc_prod_2 𝔄 𝔅)

lemma smc_prod_2_Comp_app[smc_prod_cs_simps]:
  assumes "[g, g']∘ : [b, b']∘ ↦⇘𝔄 ×SMC 𝔅⇙ [c, c']∘" 
    and "[f, f']∘ : [a, a']∘ ↦⇘𝔄 ×SMC 𝔅⇙ [b, b']∘"
  shows "[g, g']∘ ∘A⇘𝔄 ×SMC 𝔅⇙ [f, f']∘ = [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f']∘"
proof-
  have "[g, g']∘ ∘A⇘𝔄 ×SMC 𝔅⇙ [f, f']∘ = 
    (λi∈∘2ℕ. [g, g']∘⦇i⦈ ∘A⇘i = 0 ? 𝔄 : 𝔅⇙ [f, f']∘⦇i⦈)"
    by 
      (
        rule smc_prod_Comp_app[
          OF assms[unfolded smc_prod_2_def], folded smc_prod_2_def
          ]
      )
  also have 
    "(λi∈∘2ℕ. [g, g']∘⦇i⦈ ∘A⇘i = 0 ? 𝔄 : 𝔅⇙ [f, f']∘⦇i⦈) = 
      [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f']∘"
  proof(rule vsv_eqI, unfold vdomain_VLambda)
    fix i assume "i ∈∘ 2ℕ"
    then consider ‹i = 0› | ‹i = 1ℕ› unfolding two by auto 
    then show 
      "(λi∈∘2ℕ. [g, g']∘⦇i⦈ ∘A⇘i = 0 ? 𝔄 : 𝔅⇙ [f, f']∘⦇i⦈)⦇i⦈ = 
        [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f']∘⦇i⦈"
      by cases (simp_all add: two nat_omega_simps)
  qed (auto simp: two nat_omega_simps)
  finally show ?thesis by simp
qed

end


subsubsection‹Opposite product semicategory›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)

lemma op_smc_smc_prod_2[smc_op_simps]: 
  "op_smc (𝔄 ×SMC 𝔅) = op_smc 𝔄 ×SMC op_smc 𝔅"
proof(rule smc_dg_eqI[of α])

  from 𝔄 𝔅 show smc_lhs: "semicategory α (op_smc (𝔄 ×SMC 𝔅))"
    by 
      (
        cs_concl cs_shallow
          cs_simp: smc_cs_simps smc_op_simps 
          cs_intro: smc_cs_intros smc_op_intros
      )
  interpret smc_lhs: semicategory α ‹op_smc (𝔄 ×SMC 𝔅)› by (rule smc_lhs)
  
  from 𝔄 𝔅 show smc_rhs: "semicategory α (op_smc 𝔄 ×SMC op_smc 𝔅)"
    by 
      (
        cs_concl cs_shallow 
          cs_simp: smc_cs_simps smc_op_simps 
          cs_intro: smc_cs_intros smc_op_intros
      )
  interpret smc_rhs: semicategory α ‹op_smc 𝔄 ×SMC op_smc 𝔅› by (rule smc_rhs)

  show "op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈ = (op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈"
  proof(rule vsv_eqI)
    show "vsv (op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈)"
      unfolding op_smc_components by (rule fflip_vsv)
    show "vsv ((op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈)"
      unfolding smc_prod_2_def smc_prod_components by simp      
    show "𝒟∘ (op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈) = 𝒟∘ ((op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈)"
    proof(intro vsubset_antisym vsubsetI)
      fix gg'ff' assume gf: "gg'ff' ∈∘ 𝒟∘ (op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈)"
      then obtain gg' ff' aa' bb' cc' 
        where gg'ff'_def: "gg'ff' = [gg', ff']∘" 
          and "gg' : bb' ↦⇘op_smc (𝔄 ×SMC 𝔅)⇙ cc'" 
          and "ff' : aa' ↦⇘op_smc (𝔄 ×SMC 𝔅)⇙ bb'"
        by clarsimp
      then have gg': "gg' : cc' ↦⇘𝔄 ×SMC 𝔅⇙ bb'" 
        and ff': "ff' : bb' ↦⇘𝔄 ×SMC 𝔅⇙ aa'"
        unfolding smc_op_simps by simp_all
      from gg' obtain g g' b b' c c' 
        where gg'_def: "gg' = [g, g']∘" 
          and "cc' = [c, c']∘" 
          and "bb' = [b, b']∘"
          and g: "g : c ↦⇘𝔄⇙ b" 
          and g': "g' : c' ↦⇘𝔅⇙ b'"
        by (elim smc_prod_2_is_arrE[OF 𝔄 𝔅])
      with ff' obtain f f' a a' 
        where ff'_def: "ff' = [f, f']∘" 
          and "bb' = [b, b']∘" 
          and "aa' = [a, a']∘"
          and f: "f : b ↦⇘𝔄⇙ a" 
          and f': "f' : b' ↦⇘𝔅⇙ a'"
        by (auto elim: smc_prod_2_is_arrE[OF 𝔄 𝔅])
      from 𝔄 𝔅 g g' f f' show "gg'ff' ∈∘ 𝒟∘ ((op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈)"
        by
          (
            intro smc_rhs.smc_Comp_vdomainI[OF _ _ gg'ff'_def], 
            unfold gg'_def ff'_def
          )
          (
            cs_concl cs_shallow 
              cs_simp: smc_cs_simps smc_op_simps 
              cs_intro: smc_op_intros smc_prod_cs_intros
          )
    next
      fix gg'ff' assume gf: "gg'ff' ∈∘ 𝒟∘ ((op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈)"
      then obtain gg' ff' aa' bb' cc' 
        where gg'ff'_def: "gg'ff' = [gg', ff']∘" 
          and gg': "gg' : bb' ↦⇘op_smc 𝔄 ×SMC op_smc 𝔅⇙ cc'" 
          and ff': "ff' : aa' ↦⇘op_smc 𝔄 ×SMC op_smc 𝔅⇙ bb'"
        by clarsimp
      from gg' obtain g g' b b' c c' 
        where gg'_def: "gg' = [g, g']∘" 
          and "bb' = [b, b']∘"
          and "cc' = [c, c']∘" 
          and g: "g : b ↦⇘op_smc 𝔄⇙ c" 
          and g': "g' : b' ↦⇘op_smc 𝔅⇙ c'"
        by (elim smc_prod_2_is_arrE[OF 𝔄.semicategory_op 𝔅.semicategory_op])
      with ff' obtain f f' a a' 
        where ff'_def: "ff' = [f, f']∘" 
          and "aa' = [a, a']∘"
          and "bb' = [b, b']∘" 
          and f: "f : a ↦⇘op_smc 𝔄⇙ b" 
          and f': "f' : a' ↦⇘op_smc 𝔅⇙ b'"
        by 
          (
            auto elim: 
              smc_prod_2_is_arrE[OF 𝔄.semicategory_op 𝔅.semicategory_op]
          )
      from 𝔄 𝔅 g g' f f' show "gg'ff' ∈∘ 𝒟∘ (op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈)"
        by 
          (
            intro smc_lhs.smc_Comp_vdomainI[OF _ _ gg'ff'_def], 
            unfold gg'_def ff'_def smc_op_simps
          )
          (
            cs_concl cs_shallow 
              cs_simp: smc_cs_simps smc_op_simps 
              cs_intro: smc_op_intros smc_prod_cs_intros
          )
    qed
    fix gg'ff' assume "gg'ff' ∈∘ 𝒟∘ (op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈)"
    then obtain gg' ff' aa' bb' cc' 
      where gg'ff'_def: "gg'ff' = [gg', ff']∘" 
        and "gg' : bb' ↦⇘op_smc (𝔄 ×SMC 𝔅)⇙ cc'" 
        and "ff' : aa' ↦⇘op_smc (𝔄 ×SMC 𝔅)⇙ bb'"
      by clarsimp
    then have gg': "gg' : cc' ↦⇘𝔄 ×SMC 𝔅⇙ bb'" 
      and ff': "ff' : bb' ↦⇘𝔄 ×SMC 𝔅⇙ aa'"
      unfolding smc_op_simps by simp_all
    from gg' obtain g g' b b' c c' 
      where gg'_def[smc_cs_simps]: "gg' = [g, g']∘" 
        and "cc' = [c, c']∘" 
        and "bb' = [b, b']∘"
        and g: "g : c ↦⇘𝔄⇙ b" 
        and g': "g' : c' ↦⇘𝔅⇙ b'"
      by (elim smc_prod_2_is_arrE[OF 𝔄 𝔅])
    with ff' obtain f f' a a' 
      where ff'_def[smc_cs_simps]: "ff' = [f, f']∘" 
        and "bb' = [b, b']∘" 
        and "aa' = [a, a']∘"
        and f: "f : b ↦⇘𝔄⇙ a" 
        and f': "f' : b' ↦⇘𝔅⇙ a'"
      by (auto elim: smc_prod_2_is_arrE[OF 𝔄 𝔅])
    from 𝔄 𝔅 g g' f f' show "op_smc (𝔄 ×SMC 𝔅)⦇Comp⦈⦇gg'ff'⦈ = 
      (op_smc 𝔄 ×SMC op_smc 𝔅)⦇Comp⦈⦇gg'ff'⦈"
      unfolding gg'ff'_def 
      by 
        (
          cs_concl cs_shallow 
            cs_simp: smc_cs_simps smc_op_simps smc_prod_cs_simps
            cs_intro: smc_cs_intros smc_op_intros smc_prod_cs_intros
        )
  qed

  from 𝔄 𝔅 show 
    "smc_dg (op_smc (𝔄 ×SMC 𝔅)) = smc_dg (op_smc 𝔄 ×SMC op_smc 𝔅)"
    unfolding slicing_commute[symmetric]
    by (cs_concl cs_shallow cs_simp: dg_op_simps cs_intro: slicing_intros)

qed
  
end



subsection‹Projections for the product of two semicategories›


subsubsection‹Definition and elementary properties›


text‹See Chapter II-3 in cite‹"mac_lane_categories_2010"›.›

definition smcf_proj_fst :: "V ⇒ V ⇒ V" (‹πSMC.1›)
  where "πSMC.1 𝔄 𝔅 = smcf_proj (2ℕ) (λi. (i = 0 ? 𝔄 : 𝔅)) 0"
definition smcf_proj_snd :: "V ⇒ V ⇒ V" (‹πSMC.2›)
  where "πSMC.2 𝔄 𝔅 = smcf_proj (2ℕ) (λi. (i = 0 ? 𝔄 : 𝔅)) (1ℕ)"


text‹Slicing›

lemma smcf_dghm_smcf_proj_fst[slicing_commute]: 
  "πDG.1 (smc_dg 𝔄) (smc_dg 𝔅) = smcf_dghm (πSMC.1 𝔄 𝔅)"
  unfolding 
    smcf_proj_fst_def dghm_proj_fst_def slicing_commute[symmetric] if_distrib 
    ..

lemma smcf_dghm_smcf_proj_snd[slicing_commute]: 
  "πDG.2 (smc_dg 𝔄) (smc_dg 𝔅) = smcf_dghm (πSMC.2 𝔄 𝔅)"
  unfolding 
    smcf_proj_snd_def dghm_proj_snd_def slicing_commute[symmetric] if_distrib 
    ..

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])
interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)

lemmas_with 
  [
    where 𝔄=‹smc_dg 𝔄› and 𝔅=‹smc_dg 𝔅›, 
    unfolded slicing_simps slicing_commute, 
    OF 𝔄.smc_digraph 𝔅.smc_digraph
  ]:
  smcf_proj_fst_ObjMap_app[smc_cs_simps] = dghm_proj_fst_ObjMap_app 
  and smcf_proj_snd_ObjMap_app[smc_cs_simps] = dghm_proj_snd_ObjMap_app
  and smcf_proj_fst_ArrMap_app[smc_cs_simps] = dghm_proj_fst_ArrMap_app
  and smcf_proj_snd_ArrMap_app[smc_cs_simps] = dghm_proj_snd_ArrMap_app

end


subsubsection‹
Domain and codomain of a projection of a product of two semicategories
›

lemma smcf_proj_fst_HomDom: "πSMC.1 𝔄 𝔅⦇HomDom⦈ = 𝔄 ×SMC 𝔅"
  unfolding smcf_proj_fst_def smcf_proj_components smc_prod_2_def ..

lemma smcf_proj_fst_HomCod: "πSMC.1 𝔄 𝔅⦇HomCod⦈ = 𝔄"
  unfolding smcf_proj_fst_def smcf_proj_components smc_prod_2_def by simp
  
lemma smcf_proj_snd_HomDom: "πSMC.2 𝔄 𝔅⦇HomDom⦈ = 𝔄 ×SMC 𝔅"
  unfolding smcf_proj_snd_def smcf_proj_components smc_prod_2_def ..

lemma smcf_proj_snd_HomCod: "πSMC.2 𝔄 𝔅⦇HomCod⦈ = 𝔅"
  unfolding smcf_proj_snd_def smcf_proj_components smc_prod_2_def by simp


subsubsection‹Projection of a product of two semicategories is a semifunctor›

context 
  fixes α 𝔄 𝔅
  assumes 𝔄: "semicategory α 𝔄" and 𝔅: "semicategory α 𝔅"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])
interpretation finite_psemicategory α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_psemicategory_smc_prod_2 𝔄 𝔅)

lemma smcf_proj_fst_is_semifunctor: 
  assumes "i ∈∘ I" 
  shows "πSMC.1 𝔄 𝔅 : 𝔄 ×SMC 𝔅 ↦↦SMC⇘α⇙ 𝔄"
  by 
    (
      rule 
        psmc_smcf_proj_is_semifunctor[
          where i=0, simplified, folded smcf_proj_fst_def smc_prod_2_def
          ]
    )

lemma smcf_proj_fst_is_semifunctor'[smc_cs_intros]: 
  assumes "i ∈∘ I" and "ℭ = 𝔄 ×SMC 𝔅" and "𝔇 = 𝔄"
  shows "πSMC.1 𝔄 𝔅 : ℭ ↦↦SMC⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule smcf_proj_fst_is_semifunctor)

lemma smcf_proj_snd_is_semifunctor: 
  assumes "i ∈∘ I" 
  shows "πSMC.2 𝔄 𝔅 : 𝔄 ×SMC 𝔅 ↦↦SMC⇘α⇙ 𝔅"
  by 
    (
      rule 
        psmc_smcf_proj_is_semifunctor[
          where i=‹1ℕ›, simplified, folded smcf_proj_snd_def smc_prod_2_def
          ]
    )

lemma smcf_proj_snd_is_semifunctor'[smc_cs_intros]: 
  assumes "i ∈∘ I" and "ℭ = 𝔄 ×SMC 𝔅" and "𝔇 = 𝔅"
  shows "πSMC.2 𝔄 𝔅 : ℭ ↦↦SMC⇘α⇙ 𝔇"
  using assms(1) unfolding assms(2,3) by (rule smcf_proj_snd_is_semifunctor)

end



subsection‹Product of three semicategories›
(*TODO: find a way to generalize to the product of n semicategories*)


subsubsection‹Definition and elementary properties.›

definition smc_prod_3 :: "V ⇒ V ⇒ V ⇒ V"
  ("(_ ×SMC3 _ ×SMC3 _)" [81, 81, 81] 80)
  where "𝔄 ×SMC3 𝔅 ×SMC3 ℭ = (∏SMCi∈∘3ℕ. if3 𝔄 𝔅 ℭ i)"


text‹Slicing.›

lemma smc_dg_smc_prod_3[slicing_commute]: 
  "smc_dg 𝔄 ×DG3 smc_dg 𝔅 ×DG3 smc_dg ℭ = smc_dg (𝔄 ×SMC3 𝔅 ×SMC3 ℭ)"
  unfolding smc_prod_3_def dg_prod_3_def slicing_commute[symmetric] if_distrib
  by (simp add: if_distrib[symmetric])

context
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "semicategory α 𝔄" 
    and 𝔅: "semicategory α 𝔅"
    and ℭ: "semicategory α ℭ"
begin

interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)
interpretation ℭ: semicategory α ℭ by (rule ℭ)

lemmas_with 
  [
    where 𝔄=‹smc_dg 𝔄› and 𝔅=‹smc_dg 𝔅› and ℭ=‹smc_dg ℭ›, 
    unfolded slicing_simps slicing_commute, 
    OF 𝔄.smc_digraph 𝔅.smc_digraph ℭ.smc_digraph
  ]:
  smc_prod_3_ObjI = dg_prod_3_ObjI 
  and smc_prod_3_ObjI'[smc_prod_cs_intros] = dg_prod_3_ObjI'
  and smc_prod_3_ObjE = dg_prod_3_ObjE
  and smc_prod_3_ArrI = dg_prod_3_ArrI
  and smc_prod_3_ArrI'[smc_prod_cs_intros] = dg_prod_3_ArrI'
  and smc_prod_3_ArrE = dg_prod_3_ArrE
  and smc_prod_3_is_arrI = dg_prod_3_is_arrI
  and smc_prod_3_is_arrI'[smc_prod_cs_intros] = dg_prod_3_is_arrI'
  and smc_prod_3_is_arrE = dg_prod_3_is_arrE
  and smc_prod_3_Dom_vsv = dg_prod_3_Dom_vsv
  and smc_prod_3_Dom_vdomain[smc_cs_simps] = dg_prod_3_Dom_vdomain
  and smc_prod_3_Dom_app[smc_prod_cs_simps] = dg_prod_3_Dom_app
  and smc_prod_3_Dom_vrange = dg_prod_3_Dom_vrange
  and smc_prod_3_Cod_vsv = dg_prod_3_Cod_vsv
  and smc_prod_3_Cod_vdomain[smc_cs_simps] = dg_prod_3_Cod_vdomain
  and smc_prod_3_Cod_app[smc_prod_cs_simps] = dg_prod_3_Cod_app
  and smc_prod_3_Cod_vrange = dg_prod_3_Cod_vrange

end


subsubsection‹Product of three semicategories is a semicategory›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "semicategory α 𝔄" 
    and 𝔅: "semicategory α 𝔅"
    and ℭ: "semicategory α ℭ"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])
interpretation 𝔄: semicategory α 𝔄 by (rule 𝔄)
interpretation 𝔅: semicategory α 𝔅 by (rule 𝔅)
interpretation ℭ: semicategory α ℭ by (rule ℭ)

lemma finite_psemicategory_smc_prod_3: 
  "finite_psemicategory α (3ℕ) (if3 𝔄 𝔅 ℭ)"
proof(intro finite_psemicategoryI psemicategory_baseI)
  from Axiom_of_Infinity show z1_in_Vset: "3ℕ ∈∘ Vset α" by blast
  show "semicategory α (if3 𝔄 𝔅 ℭ i)" if "i ∈∘ 3ℕ" for i
    by (auto simp: smc_cs_intros)
qed auto

interpretation finite_psemicategory α ‹3ℕ› ‹if3 𝔄 𝔅 ℭ›
  by (intro finite_psemicategory_smc_prod_3 𝔄 𝔅)

lemma semicategory_smc_prod_3[smc_cs_intros]: 
  "semicategory α (𝔄 ×SMC3 𝔅 ×SMC3 ℭ)"
  unfolding smc_prod_3_def by (rule psmc_semicategory_smc_prod)

end


subsubsection‹Composition›

context 
  fixes α 𝔄 𝔅 ℭ
  assumes 𝔄: "semicategory α 𝔄" 
    and 𝔅: "semicategory α 𝔅"
    and ℭ: "semicategory α ℭ"
begin

interpretation 𝒵 α by (rule semicategoryD[OF 𝔄])

interpretation finite_psemicategory α ‹3ℕ› ‹if3 𝔄 𝔅 ℭ›
  by (intro finite_psemicategory_smc_prod_3 𝔄 𝔅 ℭ)

lemma smc_prod_3_Comp_app[smc_prod_cs_simps]:
  assumes "[g, g', g'']∘ : [b, b', b'']∘ ↦⇘𝔄 ×SMC3 𝔅 ×SMC3 ℭ⇙ [c, c', c'']∘" 
    and "[f, f', f'']∘ : [a, a', a'']∘ ↦⇘𝔄 ×SMC3 𝔅 ×SMC3 ℭ⇙ [b, b', b'']∘"
  shows 
    "[g, g', g'']∘ ∘A⇘𝔄 ×SMC3 𝔅 ×SMC3 ℭ⇙ [f, f', f'']∘ =
      [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f', g'' ∘A⇘ℭ⇙ f'']∘"
proof-
  have 
    "[g, g', g'']∘ ∘A⇘𝔄 ×SMC3 𝔅 ×SMC3 ℭ⇙ [f, f', f'']∘ =
      (λi∈∘3ℕ. [g, g', g'']∘⦇i⦈ ∘A⇘if3 𝔄 𝔅 ℭ i⇙ [f, f', f'']∘⦇i⦈)"
    by 
      (
        rule smc_prod_Comp_app[
          OF assms[unfolded smc_prod_3_def], folded smc_prod_3_def
          ]
      )
  also have 
    "(λi∈∘3ℕ. [g, g', g'']∘⦇i⦈ ∘A⇘if3 𝔄 𝔅 ℭ i⇙ [f, f', f'']∘⦇i⦈) = 
      [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f', g'' ∘A⇘ℭ⇙ f'']∘"
  proof(rule vsv_eqI, unfold vdomain_VLambda)
    fix i assume "i ∈∘ 3ℕ"
    then consider ‹i = 0› | ‹i = 1ℕ› | ‹i = 2ℕ› unfolding three by auto 
    then show 
      "(λi∈∘3ℕ. [g, g', g'']∘⦇i⦈ ∘A⇘if3 𝔄 𝔅 ℭ i⇙ [f, f', f'']∘⦇i⦈)⦇i⦈ = 
        [g ∘A⇘𝔄⇙ f, g' ∘A⇘𝔅⇙ f', g'' ∘A⇘ℭ⇙ f'']∘⦇i⦈"
      by cases (simp_all add: three nat_omega_simps)
  qed (auto simp: three nat_omega_simps)
  finally show ?thesis by simp
qed

end

text‹\newpage›

end