Theory CZH_ECAT_PCategory

(* Copyright 2021 (C) Mihails Milehins *)

section‹Product category›
theory CZH_ECAT_PCategory
  imports 
    CZH_ECAT_NTCF
    CZH_ECAT_Small_Category
    CZH_Foundations.CZH_SMC_PSemicategory
begin



subsection‹Background›


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

named_theorems cat_prod_cs_simps
named_theorems cat_prod_cs_intros



subsection‹Product category: definition and elementary properties› 

definition cat_prod :: "V ⇒ (V ⇒ V) ⇒ V" 
  where "cat_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. vpfst gf⦇i⦈ ∘A⇘𝔄 i⇙ vpsnd gf⦇i⦈)
      ),
      (λa∈∘(∏∘i∈∘I. 𝔄 i⦇Obj⦈). (λi∈∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈))
    ]∘"

syntax "_PCATEGORY" :: "pttrn ⇒ V ⇒ (V ⇒ V) ⇒ V" 
  ("(3∏C_∈∘_./ _)" [0, 0, 10] 10)
translations "∏Ci∈∘I. 𝔄" ⇌ "CONST cat_prod I (λi. 𝔄)"


text‹Components.›

lemma cat_prod_components:
  shows "(∏Ci∈∘I. 𝔄 i)⦇Obj⦈ = (∏∘i∈∘I. 𝔄 i⦇Obj⦈)"
    and "(∏Ci∈∘I. 𝔄 i)⦇Arr⦈ = (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
    and "(∏Ci∈∘I. 𝔄 i)⦇Dom⦈ =
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Dom⦈⦇f⦇i⦈⦈))"
    and "(∏Ci∈∘I. 𝔄 i)⦇Cod⦈ =
      (λf∈∘(∏∘i∈∘I. 𝔄 i⦇Arr⦈). (λi∈∘I. 𝔄 i⦇Cod⦈⦇f⦇i⦈⦈))"
    and "(∏Ci∈∘I. 𝔄 i)⦇Comp⦈ =
      (
        λgf∈∘composable_arrs (dg_prod I 𝔄).
          (λi∈∘I. vpfst gf⦇i⦈ ∘A⇘𝔄 i⇙ vpsnd gf⦇i⦈)
      )"
    and "(∏Ci∈∘I. 𝔄 i)⦇CId⦈ =
      (λa∈∘(∏∘i∈∘I. 𝔄 i⦇Obj⦈). (λi∈∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈))"
  unfolding cat_prod_def dg_field_simps by (simp_all add: nat_omega_simps)


text‹Slicing.›

lemma cat_smc_cat_prod[slicing_commute]: 
  "smc_prod I (λi. cat_smc (𝔄 i)) = cat_smc (∏Ci∈∘I. 𝔄 i)"
  unfolding dg_prod_def cat_smc_def cat_prod_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. cat_smc (𝔄 i)›, unfolded slicing_simps slicing_commute
  ]:
  cat_prod_ObjI = smc_prod_ObjI
  and cat_prod_ObjD = smc_prod_ObjD
  and cat_prod_ObjE = smc_prod_ObjE
  and cat_prod_Obj_cong = smc_prod_Obj_cong
  and cat_prod_ArrI = smc_prod_ArrI
  and cat_prod_ArrD = smc_prod_ArrD
  and cat_prod_ArrE = smc_prod_ArrE
  and cat_prod_Arr_cong = smc_prod_Arr_cong
  and cat_prod_Dom_vsv[cat_cs_intros] = smc_prod_Dom_vsv
  and cat_prod_Dom_vdomain[cat_cs_simps] = smc_prod_Dom_vdomain
  and cat_prod_Dom_app = smc_prod_Dom_app
  and cat_prod_Dom_app_component_app[cat_cs_simps] = 
    smc_prod_Dom_app_component_app
  and cat_prod_Cod_vsv[cat_cs_intros] = smc_prod_Cod_vsv
  and cat_prod_Cod_app = smc_prod_Cod_app
  and cat_prod_Cod_vdomain[cat_cs_simps] = smc_prod_Cod_vdomain
  and cat_prod_Cod_app_component_app[cat_cs_simps] = 
    smc_prod_Cod_app_component_app
  and cat_prod_Comp = smc_prod_Comp
  and cat_prod_Comp_vdomain[cat_cs_simps] = smc_prod_Comp_vdomain
  and cat_prod_Comp_app = smc_prod_Comp_app
  and cat_prod_Comp_app_component[cat_cs_simps] = 
    smc_prod_Comp_app_component
  and cat_prod_Comp_app_vdomain = smc_prod_Comp_app_vdomain
  and cat_prod_vunion_Obj_in_Obj = smc_prod_vunion_Obj_in_Obj
  and cat_prod_vdiff_vunion_Obj_in_Obj = smc_prod_vdiff_vunion_Obj_in_Obj
  and cat_prod_vunion_Arr_in_Arr = smc_prod_vunion_Arr_in_Arr
  and cat_prod_vdiff_vunion_Arr_in_Arr = smc_prod_vdiff_vunion_Arr_in_Arr

end



subsection‹Local assumptions for a product category›

locale pcategory_base = 𝒵 α for α I 𝔄 +
  assumes pcat_categories: "i ∈∘ I ⟹ category α (𝔄 i)"
    and pcat_index_in_Vset[cat_cs_intros]: "I ∈∘ Vset α"

lemma (in pcategory_base) pcat_categories'[cat_prod_cs_intros]:
  assumes "i ∈∘ I" and "α' = α"
  shows "category α' (𝔄 i)" 
  using assms(1) unfolding assms(2) by (rule pcat_categories)


text‹Rules.›

lemma (in pcategory_base) pcategory_base_axioms'[cat_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "pcategory_base α' I' 𝔄"
  unfolding assms by (rule pcategory_base_axioms)

mk_ide rf pcategory_base_def[unfolded pcategory_base_axioms_def]
  |intro pcategory_baseI|
  |dest pcategory_baseD[dest]|
  |elim pcategory_baseE[elim]|

lemma pcategory_base_psemicategory_baseI:
  assumes "psemicategory_base α I (λi. cat_smc (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ category α (𝔄 i)"
  shows "pcategory_base α I 𝔄"
proof-
  interpret psemicategory_base α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
  show ?thesis
    by (intro pcategory_baseI)
      (auto simp: assms(2) psmc_index_in_Vset psmc_Obj_in_Vset psmc_Arr_in_Vset) 
qed


text‹Product category is a product semicategory.›

context pcategory_base
begin

lemma pcat_psemicategory_base: "psemicategory_base α I (λi. cat_smc (𝔄 i))"
proof(intro psemicategory_baseI)
  from pcat_index_in_Vset show "I ∈∘ Vset α" by auto
qed (auto simp: category.cat_semicategory cat_prod_cs_intros)

interpretation psmc: psemicategory_base α I ‹λi. cat_smc (𝔄 i)› 
  by (rule pcat_psemicategory_base)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  pcat_Obj_in_Vset = psmc.psmc_Obj_in_Vset
  and pcat_Arr_in_Vset = psmc.psmc_Arr_in_Vset
  and pcat_smc_prod_Obj_in_Vset = psmc.psmc_smc_prod_Obj_in_Vset
  and pcat_smc_prod_Arr_in_Vset = psmc.psmc_smc_prod_Arr_in_Vset
  and cat_prod_Dom_app_in_Obj[cat_cs_intros] = psmc.smc_prod_Dom_app_in_Obj
  and cat_prod_Cod_app_in_Obj[cat_cs_intros] = psmc.smc_prod_Cod_app_in_Obj
  and cat_prod_is_arrI = psmc.smc_prod_is_arrI
  and cat_prod_is_arrD[dest] = psmc.smc_prod_is_arrD
  and cat_prod_is_arrE[elim] = psmc.smc_prod_is_arrE

end

lemma cat_prod_dg_prod_is_arr: 
  "g : b ↦⇘dg_prod I 𝔄⇙ c ⟷ g : b ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ c"
  unfolding is_arr_def cat_prod_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 (dg_prod I 𝔄) = composable_arrs (∏Ci∈∘I. 𝔄 i)"
  unfolding composable_arrs_def cat_prod_dg_prod_is_arr by simp


text‹Elementary properties.›

lemma (in pcategory_base) pcat_vsubset_index_pcategory_base:
  assumes "J ⊆∘ I"
  shows "pcategory_base α J 𝔄"
proof(intro pcategory_baseI)
  show "category α (𝔄 i)" if "i ∈∘ J" for i 
    using that assms by (auto intro: cat_prod_cs_intros)
  from assms show "J ∈∘ Vset α" by (simp add: vsubset_in_VsetI cat_cs_intros)
qed auto


subsubsection‹Identity›

lemma cat_prod_CId_vsv[cat_cs_intros]: "vsv ((∏Ci∈∘I. 𝔄 i)⦇CId⦈)"
  unfolding cat_prod_components by auto

lemma cat_prod_CId_vdomain[cat_cs_simps]: 
  "𝒟∘ ((∏Ci∈∘I. 𝔄 i)⦇CId⦈) = (∏Ci∈∘I. 𝔄 i)⦇Obj⦈" 
  unfolding cat_prod_components by simp

lemma cat_prod_CId_app: 
  assumes "a ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈"
  shows "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇a⦈ = (λi∈∘I. 𝔄 i⦇CId⦈⦇a⦇i⦈⦈)" 
  using assms unfolding cat_prod_components by simp

lemma cat_prod_CId_app_component[cat_cs_simps]: 
  assumes "a ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈" and "i ∈∘ I"
  shows "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇a⦈⦇i⦈ = 𝔄 i⦇CId⦈⦇a⦇i⦈⦈" 
  using assms unfolding cat_prod_components by simp

lemma (in pcategory_base) cat_prod_CId_vrange: 
  "ℛ∘ ((∏Ci∈∘I. 𝔄 i)⦇CId⦈) ⊆∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)" 
proof(intro vsubsetI)
  interpret CId: vsv ‹((∏Ci∈∘I. 𝔄 i)⦇CId⦈)› by (rule cat_prod_CId_vsv)
  fix f assume "f ∈∘ ℛ∘ ((∏Ci∈∘I. 𝔄 i)⦇CId⦈)"
  then obtain a where f_def: "f = ((∏Ci∈∘I. 𝔄 i)⦇CId⦈)⦇a⦈" 
    and "a ∈∘ 𝒟∘ ((∏Ci∈∘I. 𝔄 i)⦇CId⦈)"
    by (blast dest: CId.vrange_atD)
  then have a: "a ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈" 
    unfolding cat_prod_components by simp
  show "f ∈∘ (∏∘i∈∘I. 𝔄 i⦇Arr⦈)"
    unfolding f_def cat_prod_CId_app[OF a]
  proof(rule VLambda_in_vproduct)
    fix i assume prems: "i ∈∘ I"
    interpret 𝔄: category α ‹𝔄 i› 
      by (simp add: ‹i ∈∘ I› cat_cs_intros cat_prod_cs_intros)
    from prems a have "a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈" unfolding cat_prod_components by auto
    with is_arrD(1) show "𝔄 i⦇CId⦈⦇a⦇i⦈⦈ ∈∘ 𝔄 i⦇Arr⦈" 
      by (auto intro: cat_cs_intros)
  qed
qed


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

lemma (in pcategory_base) pcat_tiny_category_cat_prod:
  assumes "𝒵 β" and "α ∈∘ β" 
  shows "tiny_category β (∏Ci∈∘I. 𝔄 i)"
proof-

  interpret β: 𝒵 β by (rule assms(1))

  show ?thesis
  proof(intro tiny_categoryI, (unfold slicing_simps)?)
  
    show Π: "tiny_semicategory β (cat_smc (∏Ci∈∘I. 𝔄 i))"
      unfolding slicing_commute[symmetric]
      by 
        (
          intro psemicategory_base.psmc_tiny_semicategory_smc_prod; 
          (rule assms pcat_psemicategory_base)?
        )
    interpret Π: tiny_semicategory β ‹cat_smc (∏Ci∈∘I. 𝔄 i)› by (rule Π)
  
    show "vfsequence (∏Ci∈∘I. 𝔄 i)" unfolding cat_prod_def by auto
    show "vcard (∏Ci∈∘I. 𝔄 i) = 6ℕ"
      unfolding cat_prod_def by (simp add: nat_omega_simps)
  
    show CId: "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇a⦈ : a ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ a"
      if a: "a ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈" for a
    proof(rule cat_prod_is_arrI)
      have [cat_cs_intros]: "a⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈" if i: "i ∈∘ I" for i
        by (rule cat_prod_ObjD(3)[OF a i])
      from that show "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇a⦈⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ a⦇i⦈"
        if "i ∈∘ I" for i
        by 
          (
            cs_concl cs_shallow
              cs_simp: cat_cs_simps 
              cs_intro: cat_cs_intros cat_prod_cs_intros that
          )
    qed (use that in ‹auto simp: cat_prod_components cat_prod_CId_app that›)
  
    show "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ f = f"
      if "f : a ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ b" for f a b
    proof(rule cat_prod_Arr_cong)
      note f = Π.smc_is_arrD[unfolded slicing_simps, OF that]
      note a = f(2) and b = f(3) and f = f(1)
      from CId[OF b] have CId_b: 
        "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ : b ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ b"
        by simp
      from Π.smc_Comp_is_arr[unfolded slicing_simps, OF this that] show 
        "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ f ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈"
        by (simp add: cat_cs_intros)
      from that show "f ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈" by auto
      fix i assume prems: "i ∈∘ I"
      interpret 𝔄i: category α ‹𝔄 i› by (simp add: prems cat_prod_cs_intros)
      from prems cat_prod_is_arrD(7)[OF that] have fi: 
        "f⦇i⦈ : a⦇i⦈ ↦⇘𝔄 i⇙ b⦇i⦈" 
        by auto
      from prems show "((∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ f)⦇i⦈ = f⦇i⦈"
        unfolding cat_prod_Comp_app_component[OF CId_b that prems]
        unfolding cat_prod_CId_app[OF b]
        by (auto intro: 𝔄i.cat_CId_left_left[OF fi])
    qed

    show "f ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ = f"
      if "f : b ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ c" for f b c
    proof(rule cat_prod_Arr_cong)
      note f = Π.smc_is_arrD[unfolded slicing_simps, OF that]
      note b = f(2) and c = f(3) and f = f(1)
      from CId[OF b] have CId_b: 
        "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ : b ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ b"
        by simp
      from Π.smc_Comp_is_arr[unfolded slicing_simps, OF that this] show 
        "f ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈ ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈"
        by (simp add: cat_cs_intros)
      from that show "f ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈" by auto
      fix i assume prems: "i ∈∘ I"
      interpret 𝔄i: category α ‹𝔄 i› by (simp add: prems cat_prod_cs_intros)
      from prems cat_prod_is_arrD[OF that] have fi: "f⦇i⦈ : b⦇i⦈ ↦⇘𝔄 i⇙ c⦇i⦈"
        by simp
      from prems show "(f ∘A⇘(∏Ci∈∘I. 𝔄 i)⇙ (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇b⦈)⦇i⦈ = f⦇i⦈"
        unfolding cat_prod_Comp_app_component[OF that CId_b prems]
        unfolding cat_prod_CId_app[OF b]
        by (auto intro: 𝔄i.cat_CId_right_left[OF fi])
    qed
  
  qed (auto simp: cat_cs_intros cat_cs_simps intro: cat_cs_intros)

qed



subsection‹Further local assumptions for product categories›


subsubsection‹Definition and elementary properties›

locale pcategory = pcategory_base α I 𝔄 for α I 𝔄 +
  assumes pcat_Obj_vsubset_Vset: "J ⊆∘ I ⟹ (∏Ci∈∘J. 𝔄 i)⦇Obj⦈ ⊆∘ Vset α"
    and pcat_Hom_vifunion_in_Vset: 
      "⟦
        J ⊆∘ I;
        A ⊆∘ (∏Ci∈∘J. 𝔄 i)⦇Obj⦈;
        B ⊆∘ (∏Ci∈∘J. 𝔄 i)⦇Obj⦈;
        A ∈∘ Vset α;
        B ∈∘ Vset α
      ⟧ ⟹ (⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏Ci∈∘J. 𝔄 i) a b) ∈∘ Vset α"


text‹Rules.›

lemma (in pcategory) pcategory_axioms'[cat_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "pcategory α' I' 𝔄"
  unfolding assms by (rule pcategory_axioms)

mk_ide rf pcategory_def[unfolded pcategory_axioms_def]
  |intro pcategoryI|
  |dest pcategoryD[dest]|
  |elim pcategoryE[elim]|

lemmas [cat_prod_cs_intros] = pcategoryD(1)

lemma pcategory_psemicategoryI:
  assumes "psemicategory α I (λi. cat_smc (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ category α (𝔄 i)"
  shows "pcategory α I 𝔄"
proof-
  interpret psemicategory α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
  note [unfolded slicing_simps slicing_commute, cat_cs_intros] = 
    psmc_Obj_vsubset_Vset
    psmc_Hom_vifunion_in_Vset
  show ?thesis
    by (intro pcategoryI pcategory_base_psemicategory_baseI)
      (auto simp: assms(2) smc_prod_cs_intros intro!: cat_cs_intros)
qed


text‹Product category is a product semicategory.›

context pcategory
begin

lemma pcat_psemicategory: "psemicategory α I (λi. cat_smc (𝔄 i))"
proof(intro psemicategoryI, unfold slicing_simps slicing_commute)
  show "psemicategory_base α I (λi. cat_smc (𝔄 i))" 
    by (rule pcat_psemicategory_base)
qed (auto intro!: pcat_Obj_vsubset_Vset pcat_Hom_vifunion_in_Vset)

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)› 
  by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  pcat_Obj_vsubset_Vset' = psmc.psmc_Obj_vsubset_Vset'
  and pcat_Hom_vifunion_in_Vset' = psmc.psmc_Hom_vifunion_in_Vset'
  and pcat_cat_prod_vunion_is_arr = psmc.psmc_smc_prod_vunion_is_arr
  and pcat_cat_prod_vdiff_vunion_is_arr = psmc.psmc_smc_prod_vdiff_vunion_is_arr

lemmas_with [unfolded slicing_simps slicing_commute]: 
  pcat_cat_prod_vunion_Comp = psmc.psmc_smc_prod_vunion_Comp
  and pcat_cat_prod_vdiff_vunion_Comp = psmc.psmc_smc_prod_vdiff_vunion_Comp

end


text‹Elementary properties.›

lemma (in pcategory) pcat_vsubset_index_pcategory:
  assumes "J ⊆∘ I"
  shows "pcategory α J 𝔄"
proof(intro pcategoryI pcategory_psemicategoryI)
  show "cat_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" if ‹J' ⊆∘ J› for J'
  proof-
    from that assms have "J' ⊆∘ I" by simp
    then show "cat_prod J' 𝔄⦇Obj⦈ ⊆∘ Vset α" by (rule pcat_Obj_vsubset_Vset)
  qed
  fix A B J' assume prems:
    "J' ⊆∘ J"
    "A ⊆∘ (∏Ci∈∘J'. 𝔄 i)⦇Obj⦈"
    "B ⊆∘ (∏Ci∈∘J'. 𝔄 i)⦇Obj⦈"
    "A ∈∘ Vset α" 
    "B ∈∘ Vset α"
  show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom (∏Ci∈∘J'. 𝔄 i) a b) ∈∘ Vset α"
  proof-
    from prems(1) assms have "J' ⊆∘ I" by simp
    from pcat_Hom_vifunion_in_Vset[OF this prems(2-5)] show ?thesis.
  qed
  
qed (rule pcat_vsubset_index_pcategory_base[OF assms])


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

lemma (in pcategory) pcat_category_cat_prod: "category α (∏Ci∈∘I. 𝔄 i)"
proof-
  interpret tiny_category ‹α + ω› ‹∏Ci∈∘I. 𝔄 i›
    by (intro pcat_tiny_category_cat_prod) 
      (auto simp: 𝒵_α_αω 𝒵.intro 𝒵_Limit_αω 𝒵_ω_αω)
  show ?thesis
    by (rule category_if_category)  
      (
        auto 
          intro!: pcat_Hom_vifunion_in_Vset pcat_Obj_vsubset_Vset
          intro: cat_cs_intros
      )
qed



subsection‹Local assumptions for a finite product category›


subsubsection‹Definition and elementary properties›

locale finite_pcategory = pcategory_base α I 𝔄 for α I 𝔄 +
  assumes fin_pcat_index_vfinite: "vfinite I"


text‹Rules.›

lemma (in finite_pcategory) finite_pcategory_axioms[cat_prod_cs_intros]: 
  assumes "α' = α" and "I' = I"
  shows "finite_pcategory α' I' 𝔄"
  unfolding assms by (rule finite_pcategory_axioms)

mk_ide rf finite_pcategory_def[unfolded finite_pcategory_axioms_def]
  |intro finite_pcategoryI|
  |dest finite_pcategoryD[dest]|
  |elim finite_pcategoryE[elim]|

lemmas [cat_prod_cs_intros] = finite_pcategoryD(1)

lemma finite_pcategory_finite_psemicategoryI:
  assumes "finite_psemicategory α I (λi. cat_smc (𝔄 i))" 
    and "⋀i. i ∈∘ I ⟹ category α (𝔄 i)"
  shows "finite_pcategory α I 𝔄"
proof-
  interpret finite_psemicategory α I ‹λi. cat_smc (𝔄 i)› by (rule assms(1))
  show ?thesis
    by 
      (
        intro 
          assms
          finite_pcategoryI 
          pcategory_base_psemicategory_baseI 
          finite_psemicategoryD(1)[OF assms(1)]
          fin_psmc_index_vfinite
      )
qed


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

sublocale finite_pcategory ⊆ pcategory α I 𝔄
proof-
  interpret finite_psemicategory α I ‹λi. cat_smc (𝔄 i)›
  proof(intro finite_psemicategoryI psemicategory_baseI)
    fix i assume "i ∈∘ I"
    then interpret 𝔄i: category α ‹𝔄 i› by (simp add: pcat_categories)
    show "semicategory α (cat_smc (𝔄 i))" by (simp add: 𝔄i.cat_semicategory)
  qed (auto intro!: cat_cs_intros fin_pcat_index_vfinite)
  show "pcategory α I 𝔄"
    by (intro pcategory_psemicategoryI) 
      (simp_all add: pcat_categories psemicategory_axioms)
qed



subsection‹Binary union and complement›

lemma (in pcategory) pcat_cat_prod_vunion_CId:
  assumes "vdisjnt J K"
    and "J ⊆∘ I"
    and "K ⊆∘ I"
    and "a ∈∘ (∏Cj∈∘J. 𝔄 j)⦇Obj⦈"
    and "b ∈∘ (∏Cj∈∘K. 𝔄 j)⦇Obj⦈"
  shows 
    "(∏Cj∈∘J. 𝔄 j)⦇CId⦈⦇a⦈ ∪∘ (∏Cj∈∘K. 𝔄 j)⦇CId⦈⦇b⦈ = 
      (∏Ci∈∘J ∪∘ K. 𝔄 i)⦇CId⦈⦇a ∪∘ b⦈"
proof-

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

  interpret J𝔄': category α ‹cat_prod J 𝔄› 
    by (rule J𝔄.pcat_category_cat_prod)
  interpret K𝔄': category α ‹cat_prod K 𝔄› 
    by (rule K𝔄.pcat_category_cat_prod)
  interpret JK𝔄': category α ‹cat_prod (J ∪∘ K) 𝔄› 
    by (rule JK𝔄.pcat_category_cat_prod)

  from assms(4) have CId_a: "cat_prod J 𝔄⦇CId⦈⦇a⦈ : a ↦⇘(∏Cj∈∘J. 𝔄 j)⇙ a" 
    by (auto intro: cat_cs_intros)
  from assms(5) have CId_b: "cat_prod K 𝔄⦇CId⦈⦇b⦈ : b ↦⇘(∏Ck∈∘K. 𝔄 k)⇙ b" 
    by (auto intro: cat_cs_intros)
  have CId_a_CId_b: "cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪∘ cat_prod K 𝔄⦇CId⦈⦇b⦈ :
    a ∪∘ b ↦⇘cat_prod (J ∪∘ K) 𝔄⇙ a ∪∘ b"
    by (rule pcat_cat_prod_vunion_is_arr[OF assms(1-3) CId_a CId_b])
  from CId_a have a: "a ∈∘ cat_prod J 𝔄⦇Obj⦈" by (auto intro: cat_cs_intros)
  from CId_b have b: "b ∈∘ cat_prod K 𝔄⦇Obj⦈" by (auto intro: cat_cs_intros)
  from CId_a_CId_b have ab: "a ∪∘ b ∈∘ cat_prod (J ∪∘ K) 𝔄⦇Obj⦈" 
    by (auto intro: cat_cs_intros)

  note CId_aD = J𝔄.cat_prod_is_arrD[OF CId_a]
    and CId_bD = K𝔄.cat_prod_is_arrD[OF CId_b]

  show ?thesis
  proof(rule cat_prod_Arr_cong[of _ ‹J ∪∘ K› 𝔄])
    from CId_a_CId_b show 
      "cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪∘ cat_prod K 𝔄⦇CId⦈⦇b⦈ ∈∘ cat_prod (J ∪∘ K) 𝔄⦇Arr⦈"
      by auto
    from ab show "cat_prod (J ∪∘ K) 𝔄⦇CId⦈⦇a ∪∘ b⦈ ∈∘ cat_prod (J ∪∘ K) 𝔄⦇Arr⦈"
      by (auto intro: JK𝔄'.cat_is_arrD(1) cat_cs_intros)
    fix i assume "i ∈∘ J ∪∘ K"
    then consider (iJ) ‹i ∈∘ J› | (iK) ‹i ∈∘ K› by auto
    then show "(cat_prod J 𝔄⦇CId⦈⦇a⦈ ∪∘ cat_prod K 𝔄⦇CId⦈⦇b⦈)⦇i⦈ = 
      cat_prod (J ∪∘ K) 𝔄⦇CId⦈⦇a ∪∘ b⦈⦇i⦈"
      by cases
        (
          auto simp: 
            assms(1) 
            CId_aD(1-4) 
            CId_bD(1-4)
            cat_prod_CId_app[OF ab]
            cat_prod_CId_app[OF a]
            cat_prod_CId_app[OF b]
         )
  qed

qed

lemma (in pcategory) pcat_cat_prod_vdiff_vunion_CId:
  assumes "J ⊆∘ I"
    and "a ∈∘ (∏Cj∈∘I -∘ J. 𝔄 j)⦇Obj⦈"
    and "b ∈∘ (∏Cj∈∘J. 𝔄 j)⦇Obj⦈"
  shows 
    "(∏Cj∈∘I -∘ J. 𝔄 j)⦇CId⦈⦇a⦈ ∪∘ (∏Cj∈∘J. 𝔄 j)⦇CId⦈⦇b⦈ = 
      (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇a ∪∘ b⦈"
  by 
    (
      vdiff_of_vunion' 
        rule: pcat_cat_prod_vunion_CId assms: assms(2-3) subset: assms(1)
    )



subsection‹Projection›


subsubsection‹Definition and elementary properties›


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

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


text‹Components.›

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


text‹Slicing›

lemma cf_smcf_cf_proj[slicing_commute]: 
  "πSMC I (λi. cat_smc (𝔄 i)) i = cf_smcf (πC I 𝔄 i)"
  unfolding 
    cat_smc_def 
    cf_smcf_def 
    smcf_proj_def 
    cf_proj_def 
    cat_prod_def 
    smc_prod_def
    dg_prod_def
    dg_field_simps 
    dghm_field_simps 
  by (simp add: nat_omega_simps)

context pcategory
begin

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)› 
  by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  pcat_cf_proj_is_semifunctor = psmc.psmc_smcf_proj_is_semifunctor

end


subsubsection‹Projection functor is a functor›

lemma (in pcategory) pcat_cf_proj_is_functor: 
  assumes "i ∈∘ I"
  shows "πC I 𝔄 i : (∏Ci∈∘I. 𝔄 i) ↦↦C⇘α⇙ 𝔄 i"
proof(intro is_functorI)
  interpret 𝔄: category α ‹(∏Ci∈∘I. 𝔄 i)› 
    by (simp add: pcat_category_cat_prod)
  show "vfsequence (πC I 𝔄 i)" unfolding cf_proj_def by simp
  show "category α (∏Ci∈∘I. 𝔄 i)" by (simp add: 𝔄.category_axioms)
  show "vcard (πC I 𝔄 i) = 4ℕ"
    unfolding cf_proj_def by (simp add: nat_omega_simps)
  show "πC I 𝔄 i⦇ArrMap⦈⦇(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = 𝔄 i⦇CId⦈⦇πC I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈" for c
  proof-
    interpret 𝔄i: category α ‹𝔄 i› 
      by (auto intro: assms cat_prod_cs_intros)
    from that have "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈ : c ↦⇘(∏Ci∈∘I. 𝔄 i)⇙ c"
      by (simp add: 𝔄.cat_CId_is_arr)
    then have "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈ ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈" 
      by (auto intro: cat_cs_intros)
    with assms have 
      "πC I 𝔄 i⦇ArrMap⦈⦇(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈⦇i⦈"
      unfolding cf_proj_components cat_prod_components by simp
    also from assms have "… = 𝔄 i⦇CId⦈⦇c⦇i⦈⦈"
      unfolding cat_prod_CId_app[OF that] by simp
    also from that have "… = 𝔄 i⦇CId⦈⦇πC I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
      unfolding cf_proj_components cat_prod_components by simp
    finally show 
      "πC I 𝔄 i⦇ArrMap⦈⦇(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇c⦈⦈ = 𝔄 i⦇CId⦈⦇πC I 𝔄 i⦇ObjMap⦈⦇c⦈⦈"
      by simp
  qed
qed 
  (
    auto simp: 
      assms cf_proj_components pcat_cf_proj_is_semifunctor cat_prod_cs_intros
  ) 

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

lemmas [cat_cs_intros] = pcategory.pcat_cf_proj_is_functor'



subsection‹Category product universal property functor›


subsubsection‹Definition and elementary properties›

text‹
The functor that is presented in this section is used in the proof of 
the universal property of the product category later in this work.
›

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


text‹Components.›

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


text‹Slicing.›

lemma smcf_dghm_cf_up[slicing_commute]: 
  "smcf_up I (λi. cat_smc (𝔄 i)) (cat_smc ℭ) (λi. cf_smcf (φ i)) = 
    cf_smcf (cf_up I 𝔄 ℭ φ)"
  unfolding 
    cat_smc_def 
    cf_smcf_def 
    cf_up_def 
    smcf_up_def 
    cat_prod_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. cat_smc (𝔄 i)› and φ=‹λi. cf_smcf (φ i)› and ℭ = ‹cat_smc ℭ›, 
    unfolded slicing_simps slicing_commute
  ]:
  cf_up_ObjMap_vdomain[simp] = smcf_up_ObjMap_vdomain
  and cf_up_ObjMap_app = smcf_up_ObjMap_app
  and cf_up_ObjMap_app_vdomain[simp] = smcf_up_ObjMap_app_vdomain
  and cf_up_ObjMap_app_component = smcf_up_ObjMap_app_component
  and cf_up_ArrMap_vdomain[simp] = smcf_up_ArrMap_vdomain
  and cf_up_ArrMap_app = smcf_up_ArrMap_app
  and cf_up_ArrMap_app_vdomain[simp] = smcf_up_ArrMap_app_vdomain
  and cf_up_ArrMap_app_component = smcf_up_ArrMap_app_component

lemma cf_up_ObjMap_vrange:
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i"
  shows "ℛ∘ (cf_up I 𝔄 ℭ φ⦇ObjMap⦈) ⊆∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈"
proof
  (
    rule smcf_up_ObjMap_vrange[
      where 𝔄=‹λi. cat_smc (𝔄 i)› 
        and φ=‹λi. cf_smcf (φ i)› 
        and ℭ=‹cat_smc ℭ›, 
      unfolded slicing_simps slicing_commute
      ]
  )
  fix i assume "i ∈∘ I"
  then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
  show "cf_smcf (φ i) : cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (𝔄 i)"
    by (rule cf_is_semifunctor)
qed

lemma cf_up_ObjMap_app_vrange:
  assumes "a ∈∘ ℭ⦇Obj⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i"
  shows " ℛ∘ (cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Obj⦈)"
proof
  (
    rule smcf_up_ObjMap_app_vrange[
      where 𝔄=‹λi. cat_smc (𝔄 i)› 
        and φ=‹λi. cf_smcf (φ i)› 
        and ℭ=‹cat_smc ℭ›, 
      unfolded slicing_simps slicing_commute
      ]
  )
  show "a ∈∘ ℭ⦇Obj⦈" by (rule assms)
  fix i assume "i ∈∘ I"
  then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
  show "cf_smcf (φ i) : cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (𝔄 i)"
    by (rule cf_is_semifunctor)
qed

lemma cf_up_ArrMap_vrange:
  assumes "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i"
  shows "ℛ∘ (cf_up I 𝔄 ℭ φ⦇ArrMap⦈) ⊆∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈"
proof
  (
    rule smcf_up_ArrMap_vrange[
      where 𝔄=‹λi. cat_smc (𝔄 i)› 
        and φ=‹λi. cf_smcf (φ i)› 
        and ℭ=‹cat_smc ℭ›, 
      unfolded slicing_simps slicing_commute
      ]
  )
  fix i assume "i ∈∘ I"
  then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms)
  show "cf_smcf (φ i) : cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (𝔄 i)"
    by (rule cf_is_semifunctor)
qed

lemma cf_up_ArrMap_app_vrange:
  assumes "a ∈∘ ℭ⦇Arr⦈" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i"
  shows " ℛ∘ (cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇a⦈) ⊆∘ (⋃∘i∈∘I. 𝔄 i⦇Arr⦈)"
proof
  (
    rule smcf_up_ArrMap_app_vrange
      [
        where 𝔄=‹λi. cat_smc (𝔄 i)› 
          and φ=‹λi. cf_smcf (φ i)› 
          and ℭ=‹cat_smc ℭ›, 
        unfolded slicing_simps slicing_commute
      ]
  )
  fix i assume "i ∈∘ I"
  then interpret is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2))
  show "cf_smcf (φ i) : cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (𝔄 i)"
    by (rule cf_is_semifunctor)
qed (rule assms)

end

context pcategory
begin

interpretation psmc: psemicategory α I ‹λi. cat_smc (𝔄 i)› 
  by (rule pcat_psemicategory)

lemmas_with [unfolded slicing_simps slicing_commute]: 
  pcat_smcf_comp_smcf_proj_smcf_up = psmc.psmc_Comp_smcf_proj_smcf_up
  and pcat_smcf_up_eq_smcf_proj = psmc.psmc_smcf_up_eq_smcf_proj

end


subsubsection‹Category product universal property functor is a functor›

lemma (in pcategory) pcat_cf_up_is_functor:
  assumes "category α ℭ" and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i"
  shows "cf_up I 𝔄 ℭ φ : ℭ ↦↦C⇘α⇙ (∏Ci∈∘I. 𝔄 i)"
proof-
  interpret ℭ: category α ℭ by (simp add: assms(1))
  interpret 𝔄: category α ‹(∏Ci∈∘I. 𝔄 i)› by (rule pcat_category_cat_prod)
  show ?thesis
  proof(intro is_functorI)
    show "vfsequence (cf_up I 𝔄 ℭ φ)" unfolding cf_up_def by simp
    show "vcard (cf_up I 𝔄 ℭ φ) = 4ℕ"
      unfolding cf_up_def by (simp add: nat_omega_simps)
    show "cf_smcf (cf_up I 𝔄 ℭ φ) : cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (∏Ci∈∘I. 𝔄 i)"
      unfolding slicing_commute[symmetric]
      by (rule psemicategory.psmc_smcf_up_is_semifunctor)
        (
          auto simp: 
            assms(2)
            pcat_psemicategory 
            is_functor.cf_is_semifunctor 
            slicing_intros
        )
    show "cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 
      (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈"
      if "c ∈∘ ℭ⦇Obj⦈" for c
    proof(rule cat_prod_Arr_cong)
      from that is_arrD(1) have CId_c: "ℭ⦇CId⦈⦇c⦈ ∈∘ ℭ⦇Arr⦈" 
        by (auto intro: cat_cs_intros)
      from CId_c cf_up_ArrMap_vrange[OF assms(2), simplified]
      show "cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈"
        unfolding cf_up_components by force
      have cf_up_φ_c: "cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈ ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Obj⦈"
        unfolding cat_prod_components
      proof(intro vproductI ballI)
        fix i assume prems: "i ∈∘ I"
        interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (simp add: prems assms(2))
        from that show  "cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦇i⦈ ∈∘ 𝔄 i⦇Obj⦈"
          unfolding cf_up_ObjMap_app_component[OF that prems] 
          by (auto intro: cat_cs_intros)
      qed (simp_all add: cf_up_ObjMap_app that cf_up_ObjMap_app[OF that])
      from 𝔄.cat_CId_is_arr[OF this] show 
        "(∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈ ∈∘ (∏Ci∈∘I. 𝔄 i)⦇Arr⦈"
        by auto
      fix i assume prems: "i ∈∘ I"
      interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (simp add: prems assms(2))
      from cf_up_φ_c prems show 
        "cf_up I 𝔄 ℭ φ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈⦇i⦈ =
          (∏Ci∈∘I. 𝔄 i)⦇CId⦈⦇cf_up I 𝔄 ℭ φ⦇ObjMap⦈⦇c⦈⦈⦇i⦈"
        unfolding cf_up_ArrMap_app_component[OF CId_c prems] cat_prod_components
        by 
          (
            simp add: 
              that cf_up_ObjMap_app_component[OF that prems] φ.cf_ObjMap_CId 
          )
    qed 
  qed (auto simp: cf_up_components cat_cs_intros)
qed


subsubsection‹Further properties›

lemma (in pcategory) pcat_Comp_cf_proj_cf_up: 
  assumes "category α ℭ" 
    and "⋀i. i ∈∘ I ⟹ φ i : ℭ ↦↦C⇘α⇙ 𝔄 i" 
    and "i ∈∘ I" 
  shows "φ i = πC I 𝔄 i ∘CF (cf_up I 𝔄 ℭ φ)"
proof-
  interpret φ: is_functor α ℭ ‹𝔄 i› ‹φ i› by (rule assms(2)[OF assms(3)])
  interpret π: is_functor α ‹(∏Ci∈∘I. 𝔄 i)› ‹𝔄 i› ‹πC I 𝔄 i›
    by (simp add: assms(3) pcat_cf_proj_is_functor)
  interpret up: is_functor α ℭ ‹(∏Ci∈∘I. 𝔄 i)› ‹cf_up I 𝔄 ℭ φ›
    by (simp add: assms(2) φ.HomDom.category_axioms pcat_cf_up_is_functor)
  show ?thesis
  proof(rule cf_smcf_eqI)
    show "πC I 𝔄 i ∘CF cf_up I 𝔄 ℭ φ : ℭ ↦↦C⇘α⇙ 𝔄 i" 
      by (auto intro: cat_cs_intros)
    from assms show "cf_smcf (φ i) = cf_smcf (πC I 𝔄 i ∘CF cf_up I 𝔄 ℭ φ)"
      unfolding slicing_simps slicing_commute[symmetric]
      by 
        (
          intro pcat_smcf_comp_smcf_proj_smcf_up[
            where φ=‹λi. cf_smcf (φ i)›, unfolded slicing_commute[symmetric]
            ]
        )
        (auto simp: is_functor.cf_is_semifunctor)
  qed (auto intro: cat_cs_intros)
qed

lemma (in pcategory) pcat_cf_up_eq_cf_proj:
  assumes "𝔉 : ℭ ↦↦C⇘α⇙ (∏Ci∈∘I. 𝔄 i)"
    and "⋀i. i ∈∘ I ⟹ φ i = πC I 𝔄 i ∘CF 𝔉"
  shows "cf_up I 𝔄 ℭ φ = 𝔉"
proof(rule cf_smcf_eqI)
  interpret 𝔉: is_functor α ℭ ‹(∏Ci∈∘I. 𝔄 i)› 𝔉 by (rule assms(1))
  show "cf_up I 𝔄 ℭ φ : ℭ ↦↦C⇘α⇙ (∏Ci∈∘I. 𝔄 i)"
  proof(rule pcat_cf_up_is_functor)
    fix i assume prems: "i ∈∘ I"
    then interpret π: is_functor α ‹(∏Ci∈∘I. 𝔄 i)› ‹𝔄 i› ‹πC I 𝔄 i›
      by (rule pcat_cf_proj_is_functor)
    show "φ i : ℭ ↦↦C⇘α⇙ 𝔄 i" 
      unfolding assms(2)[OF prems] by (auto intro: cat_cs_intros)
  qed (auto intro: cat_cs_intros)
  show "𝔉 : ℭ ↦↦C⇘α⇙ (∏Ci∈∘I. 𝔄 i)" by (rule assms(1))
  from assms show "cf_smcf (cf_up I 𝔄 ℭ φ) = cf_smcf 𝔉"
    unfolding slicing_commute[symmetric]
    by (intro pcat_smcf_up_eq_smcf_proj) (auto simp: slicing_commute)
qed simp_all



subsection‹Prodfunctor with respect to a fixed argument›

text‹
A prodfunctor is a functor whose domain is a product category. 
It is a generalization of the concept of the bifunctor,
as presented in Chapter II-3 in cite‹"mac_lane_categories_2010"›.  
›

definition prodfunctor_proj :: "V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ V ⇒ V ⇒ V"
  where "prodfunctor_proj 𝔖 I 𝔄 𝔇 J c =
    [
      (λb∈∘(∏Ci∈∘I -∘ J. 𝔄 i)⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈),
      (λf∈∘(∏Ci∈∘I -∘ J. 𝔄 i)⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ (∏Cj∈∘J. 𝔄 j)⦇CId⦈⦇c⦈⦈),
      (∏Ci∈∘I -∘ J. 𝔄 i),
      𝔇
    ]∘"

syntax "_PPRODFUNCTOR_PROJ" :: "V ⇒ pttrn ⇒ V ⇒ V ⇒ (V ⇒ V) ⇒ V ⇒ V ⇒ V" 
  (‹(_⇘(3∏C_∈∘_-∘_./_),_⇙/'(/-,_/'))› [51, 51, 51, 51, 51, 51, 51] 51)
translations "𝔖⇘∏Ci∈∘I-∘J. 𝔄,𝔇⇙(-,c)" ⇌ 
  "CONST prodfunctor_proj 𝔖 I (λi. 𝔄) 𝔇 J c"


text‹Components.›

lemma prodfunctor_proj_components:
  shows "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c))⦇ObjMap⦈ = 
      (λb∈∘(∏Ci∈∘I -∘ J. 𝔄 i)⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈)"
    and "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c))⦇ArrMap⦈ = 
      (λf∈∘(∏Ci∈∘I -∘ J. 𝔄 i)⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ (∏Cj∈∘J. 𝔄 j)⦇CId⦈⦇c⦈⦈)"
    and "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c))⦇HomDom⦈ = (∏Ci∈∘I -∘ J. 𝔄 i)"
    and "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c))⦇HomCod⦈ = 𝔇"
  unfolding prodfunctor_proj_def dghm_field_simps
  by (simp_all add: nat_omega_simps)


subsubsection‹Object map›

mk_VLambda prodfunctor_proj_components(1)
  |vsv prodfunctor_proj_ObjMap_vsv[cat_cs_intros]|
  |vdomain prodfunctor_proj_ObjMap_vdomain[cat_cs_simps]|
  |app prodfunctor_proj_ObjMap_app[cat_cs_simps]|


subsubsection‹Arrow map›

mk_VLambda prodfunctor_proj_components(2)
  |vsv prodfunctor_proj_ArrMap_vsv[cat_cs_intros]|
  |vdomain prodfunctor_proj_ArrMap_vdomain[cat_cs_simps]|
  |app  prodfunctor_proj_ArrMap_app[cat_cs_simps]|


subsubsection‹Prodfunctor with respect to a fixed argument is a functor›

lemma (in pcategory) pcat_prodfunctor_proj_is_functor: 
  assumes "𝔖 : (∏Ci∈∘I. 𝔄 i) ↦↦C⇘α⇙ 𝔇" 
    and "c ∈∘ (∏Cj∈∘J. 𝔄 j)⦇Obj⦈"
    and "J ⊆∘ I"
  shows "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c)) : (∏Ci∈∘I -∘ J. 𝔄 i) ↦↦C⇘α⇙ 𝔇"
proof-

  interpret is_functor α ‹(∏Ci∈∘I. 𝔄 i)› 𝔇 𝔖 by (rule assms(1))
  interpret 𝔄: pcategory α J 𝔄
    using assms(3) by (intro pcat_vsubset_index_pcategory) auto
  interpret J_𝔄: category α ‹∏Ci∈∘J. 𝔄 i› by (rule 𝔄.pcat_category_cat_prod)
  interpret IJ: pcategory α ‹I -∘ J› 𝔄
    using assms(3) by (intro pcat_vsubset_index_pcategory) auto
  interpret IJ_𝔄: category α ‹∏Ci∈∘I -∘ J. 𝔄 i›
    by (rule IJ.pcat_category_cat_prod)

  let ?IJ𝔄 = ‹(∏Ci∈∘I -∘ J. 𝔄 i)›

  from assms(2) have "c ∈∘ (∏∘j∈∘J. 𝔄 j⦇Obj⦈)"
    unfolding cat_prod_components by simp
  then have "(∏∘j∈∘J. 𝔄 j⦇Obj⦈) ≠ 0" by (auto intro!: cat_cs_intros)

  show ?thesis
  proof(intro is_functorI', unfold prodfunctor_proj_components)

    show "vfsequence (prodfunctor_proj 𝔖 I 𝔄 𝔇 J c)"
      unfolding prodfunctor_proj_def by simp
    show "vcard (prodfunctor_proj 𝔖 I 𝔄 𝔇 J c) = 4ℕ"
      unfolding prodfunctor_proj_def by (simp add: nat_omega_simps)

    show "ℛ∘ (λb∈∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈) ⊆∘ 𝔇⦇Obj⦈"
    proof(intro vsubsetI)
      fix x assume "x ∈∘ ℛ∘ (λb∈∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈)"
      then obtain b where x_def: "x = 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈" and b: "b ∈∘ ?IJ𝔄⦇Obj⦈"  
        by auto
      have "b ∪∘ c ∈∘ cat_prod I 𝔄⦇Obj⦈"
      proof(rule cat_prod_vdiff_vunion_Obj_in_Obj)
        show "b ∈∘ ?IJ𝔄⦇Obj⦈" by (rule b)
      qed (intro assms(2,3))+
      then show "x ∈∘ 𝔇⦇Obj⦈" unfolding x_def by (auto intro: cat_cs_intros)
    qed

    show is_arr:
      "(λf∈∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇f⦈ : 
        (λb∈∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈)⦇a⦈ ↦⇘𝔇⇙ 
        (λb∈∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈)⦇b⦈"
      (is ‹?V_f: ?V_a ↦⇘𝔇⇙ ?V_b›)
      if "f : a ↦⇘?IJ𝔄⇙ b" for f a b
    proof-
      let ?fc = ‹f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈›
      have "?fc : a ∪∘ c ↦⇘cat_prod I 𝔄⇙ b ∪∘ c"
      proof(rule pcat_cat_prod_vdiff_vunion_is_arr)
        show "f : a ↦⇘?IJ𝔄⇙ b" by (rule that)
      qed (auto simp: assms cat_cs_intros)
      then have "𝔖⦇ArrMap⦈⦇?fc⦈ : 𝔖⦇ObjMap⦈⦇a ∪∘ c⦈ ↦⇘𝔇⇙ 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈"
        by (auto intro: cat_cs_intros)
      moreover from that have "f ∈∘ ?IJ𝔄⦇Arr⦈" "a ∈∘ ?IJ𝔄⦇Obj⦈" "b ∈∘ ?IJ𝔄⦇Obj⦈"
        by (auto intro: cat_cs_intros) 
      ultimately show ?thesis by simp
    qed

    show 
      "(λf∈∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇g ∘A⇘?IJ𝔄⇙ f⦈ =
      (λf∈∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇g⦈ ∘A⇘𝔇⇙ 
      (λf∈∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇f⦈"
      if "g : b' ↦⇘?IJ𝔄⇙ c'" and "f : a' ↦⇘?IJ𝔄⇙ b'" for g b' c' f a'
    proof-
      from that have gf: "g ∘A⇘?IJ𝔄⇙ f : a' ↦⇘?IJ𝔄⇙ c'" 
        by (auto intro: cat_cs_intros)
      from assms(2) have CId_c: "cat_prod J 𝔄⦇CId⦈⦇c⦈ : c ↦⇘cat_prod J 𝔄⇙ c" 
        by (auto intro: cat_cs_intros)
      then have [simp]:  
        "cat_prod J 𝔄⦇CId⦈⦇c⦈ ∘A⇘cat_prod J 𝔄⇙ cat_prod J 𝔄⦇CId⦈⦇c⦈ = 
          cat_prod J 𝔄⦇CId⦈⦇c⦈"
        by (auto simp: cat_cs_simps)
      from assms(3) that(1) CId_c have g_CId_c:
        "g ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ : b' ∪∘ c ↦⇘cat_prod I 𝔄⇙ c' ∪∘ c"
        by (rule pcat_cat_prod_vdiff_vunion_is_arr)
      from assms(3) that(2) CId_c have f_CId_c:
        "f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ : a' ∪∘ c ↦⇘cat_prod I 𝔄⇙ b' ∪∘ c"
        by (rule pcat_cat_prod_vdiff_vunion_is_arr)
      have 
        "𝔖⦇ArrMap⦈⦇(g ∘A⇘?IJ𝔄⇙ f) ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ = 
          𝔖⦇ArrMap⦈⦇g ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ ∘A⇘𝔇⇙
          𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈"
        unfolding 
          pcat_cat_prod_vdiff_vunion_Comp[
            OF assms(3) that(1) CId_c that(2) CId_c, simplified
            ]
        by (intro cf_ArrMap_Comp[OF g_CId_c f_CId_c])
      moreover from gf have "g ∘A⇘?IJ𝔄⇙ f ∈∘ ?IJ𝔄⦇Arr⦈" by auto
      moreover from that have "g ∈∘ ?IJ𝔄⦇Arr⦈" "f ∈∘ ?IJ𝔄⦇Arr⦈" by auto
      ultimately show ?thesis by simp
    qed

    show 
      "(λf∈∘?IJ𝔄⦇Arr⦈. 𝔖⦇ArrMap⦈⦇f ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈)⦇?IJ𝔄⦇CId⦈⦇c'⦈⦈ = 
        𝔇⦇CId⦈⦇(λb∈∘?IJ𝔄⦇Obj⦈. 𝔖⦇ObjMap⦈⦇b ∪∘ c⦈)⦇c'⦈⦈"
      if "c' ∈∘ ?IJ𝔄⦇Obj⦈" for c'
    proof-
      have "?IJ𝔄⦇CId⦈⦇c'⦈ ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈ = cat_prod I 𝔄⦇CId⦈⦇c' ∪∘ c⦈"
        unfolding pcat_cat_prod_vdiff_vunion_CId[OF assms(3) that assms(2)] ..
      moreover from assms(3) that assms(2) have "c' ∪∘ c ∈∘ cat_prod I 𝔄⦇Obj⦈"
        by (rule cat_prod_vdiff_vunion_Obj_in_Obj)
      ultimately have "𝔖⦇ArrMap⦈⦇?IJ𝔄⦇CId⦈⦇c'⦈ ∪∘ cat_prod J 𝔄⦇CId⦈⦇c⦈⦈ =
        𝔇⦇CId⦈⦇𝔖⦇ObjMap⦈⦇c' ∪∘ c⦈⦈"
        by (auto intro: cat_cs_intros) 
      moreover from that have CId_c': "?IJ𝔄⦇CId⦈⦇c'⦈ ∈∘ ?IJ𝔄⦇Arr⦈"
        by (auto dest!: IJ_𝔄.cat_CId_is_arr)
      ultimately show ?thesis by (simp add: that)
    qed

  qed (auto intro: cat_cs_intros) 

qed

lemma (in pcategory) pcat_prodfunctor_proj_is_functor': 
  assumes "𝔖 : (∏Ci∈∘I. 𝔄 i) ↦↦C⇘α⇙ 𝔇" 
    and "c ∈∘ (∏Cj∈∘J. 𝔄 j)⦇Obj⦈"
    and "J ⊆∘ I"
    and "𝔄' = (∏Ci∈∘I -∘ J. 𝔄 i)"
    and "𝔅' = 𝔇"
  shows "(𝔖⇘∏Ci∈∘I -∘ J. 𝔄 i,𝔇⇙(-,c)) : 𝔄' ↦↦C⇘α⇙ 𝔅'"
  using assms(1-3)
  unfolding assms(4,5)
  by (rule pcat_prodfunctor_proj_is_functor)

lemmas [cat_cs_intros] = pcategory.pcat_prodfunctor_proj_is_functor'



subsection‹Singleton category›


subsubsection‹Slicing›

context
  fixes ℭ :: V
begin

lemmas_with [where ℭ=‹cat_smc ℭ›, unfolded slicing_simps slicing_commute]:
  cat_singleton_ObjI = smc_singleton_ObjI
  and cat_singleton_ObjE = smc_singleton_ObjE
  and cat_singleton_ArrI = smc_singleton_ArrI
  and cat_singleton_ArrE = smc_singleton_ArrE

end

context category
begin

interpretation smc: semicategory α ‹cat_smc ℭ› by (rule cat_semicategory)

lemmas_with [unfolded slicing_simps slicing_commute]:
  cat_finite_psemicategory_cat_singleton = 
    smc.smc_finite_psemicategory_smc_singleton
  and cat_singleton_is_arrI = smc.smc_singleton_is_arrI
  and cat_singleton_is_arrD = smc.smc_singleton_is_arrD
  and cat_singleton_is_arrE = smc.smc_singleton_is_arrE

end


subsubsection‹Identity›

lemma cat_singleton_CId_app: 
  assumes "set {⟨j, a⟩} ∈∘ (∏Ci∈∘set {j}. ℭ)⦇Obj⦈"
  shows "(∏Ci∈∘set {j}. ℭ)⦇CId⦈⦇set {⟨j, a⟩}⦈ = set {⟨j, ℭ⦇CId⦈⦇a⦈⟩}"
  using assms unfolding cat_prod_components VLambda_vsingleton by simp


subsubsection‹Singleton category is a category›

lemma (in category) cat_finite_pcategory_cat_singleton: 
  assumes "j ∈∘ Vset α"
  shows "finite_pcategory α (set {j}) (λi. ℭ)"
  by 
    (
      auto intro: 
        assms
        category_axioms 
        finite_pcategory_finite_psemicategoryI 
        cat_finite_psemicategory_cat_singleton 
    )

lemma (in category) cat_category_cat_singleton:
  assumes "j ∈∘ Vset α"
  shows "category α (∏Ci∈∘set {j}. ℭ)"
proof-
  interpret finite_pcategory α ‹set {j}› ‹λi. ℭ›
    using assms by (rule cat_finite_pcategory_cat_singleton)
  show ?thesis by (rule pcat_category_cat_prod)
qed



subsection‹Singleton functor›


subsubsection‹Definition and elementary properties›

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


text‹Components.›

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


text‹Slicing.›

lemma cf_smcf_cf_singleton[slicing_commute]: 
  "smcf_singleton j (cat_smc ℭ)= cf_smcf (cf_singleton j ℭ)"
  unfolding smcf_singleton_def cf_singleton_def slicing_simps slicing_commute
  by 
    (
      simp add: 
        nat_omega_simps dghm_field_simps dg_field_simps cat_smc_def cf_smcf_def
     )

context
  fixes ℭ :: V
begin

lemmas_with [where ℭ=‹cat_smc ℭ›, unfolded slicing_simps slicing_commute]:
  cf_singleton_ObjMap_vsv[cat_cs_intros] = smcf_singleton_ObjMap_vsv
  and cf_singleton_ObjMap_vdomain[cat_cs_simps] = smcf_singleton_ObjMap_vdomain
  and cf_singleton_ObjMap_vrange = smcf_singleton_ObjMap_vrange
  and cf_singleton_ObjMap_app[cat_prod_cs_simps] = smcf_singleton_ObjMap_app
  and cf_singleton_ArrMap_vsv[cat_cs_intros] = smcf_singleton_ArrMap_vsv
  and cf_singleton_ArrMap_vdomain[cat_cs_simps] = smcf_singleton_ArrMap_vdomain
  and cf_singleton_ArrMap_vrange = smcf_singleton_ArrMap_vrange
  and cf_singleton_ArrMap_app[cat_prod_cs_simps] = smcf_singleton_ArrMap_app

end


subsubsection‹Singleton functor is an isomorphism of categories›

lemma (in category) cat_cf_singleton_is_functor:
  assumes "j ∈∘ Vset α"
  shows "cf_singleton j ℭ : ℭ ↦↦C.iso⇘α⇙ (∏Ci∈∘set {j}. ℭ)"
proof(intro is_iso_functorI is_functorI)
  from assms show smcf_singleton: "cf_smcf (cf_singleton j ℭ) : 
    cat_smc ℭ ↦↦SMC.iso⇘α⇙ cat_smc (∏Ci∈∘set {j}. ℭ)"
    unfolding slicing_commute[symmetric]
    by (intro semicategory.smc_smcf_singleton_is_iso_semifunctor) 
      (auto intro: smc_cs_intros slicing_intros)
  show "vfsequence (cf_singleton j ℭ)" unfolding cf_singleton_def by simp
  show "vcard (cf_singleton j ℭ) = 4ℕ"
    unfolding cf_singleton_def by (simp add: nat_omega_simps)
  show "cf_smcf (cf_singleton j ℭ) : 
    cat_smc ℭ ↦↦SMC⇘α⇙ cat_smc (∏Ci∈∘set {j}. ℭ)"
    by (intro is_iso_semifunctor.axioms(1) smcf_singleton)
  show "cf_singleton j ℭ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = 
    (∏Ci∈∘set {j}. ℭ)⦇CId⦈⦇cf_singleton j ℭ⦇ObjMap⦈⦇c⦈⦈"
    if "c ∈∘ ℭ⦇Obj⦈" for c 
  proof-
    from that have CId_c: "ℭ⦇CId⦈⦇c⦈ : c ↦⇘ℭ⇙ c" by (auto simp: cat_cs_intros)
    have "set {⟨j, c⟩} ∈∘ (∏Ci∈∘set {j}. ℭ)⦇Obj⦈"
      by (simp add: cat_singleton_ObjI that)
    with that have "(∏Ci∈∘set {j}. ℭ)⦇CId⦈⦇cf_singleton j ℭ⦇ObjMap⦈⦇c⦈⦈ = 
      set {⟨j, ℭ⦇CId⦈⦇c⦈⟩}"
      by (simp add: cf_singleton_ObjMap_app cat_singleton_CId_app)
    moreover from CId_c have 
      "cf_singleton j ℭ⦇ArrMap⦈⦇ℭ⦇CId⦈⦇c⦈⦈ = set {⟨j, ℭ⦇CId⦈⦇c⦈⟩}"
      by (auto simp: cf_singleton_ArrMap_app cat_cs_intros)
    ultimately show ?thesis by simp
  qed
qed 
  (
    auto simp: 
      cat_cs_intros assms cat_category_cat_singleton cf_singleton_components 
  )



subsection‹Product of two categories›


subsubsection‹Definition and elementary properties.›


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

definition cat_prod_2 :: "V ⇒ V ⇒ V" (infixr ‹×C› 80)
  where "𝔄 ×C 𝔅 ≡ cat_prod (2ℕ) (λi. if i = 0 then 𝔄 else 𝔅)"


text‹Slicing.›
  
lemma cat_smc_cat_prod_2[slicing_commute]: 
  "cat_smc 𝔄 ×SMC cat_smc 𝔅 = cat_smc (𝔄 ×C 𝔅)"
  unfolding cat_prod_2_def smc_prod_2_def slicing_commute[symmetric] if_distrib
  by simp

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

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

lemmas_with 
  [
    where 𝔄=‹cat_smc 𝔄› and 𝔅=‹cat_smc 𝔅›, 
    unfolded slicing_simps slicing_commute, 
    OF 𝔄.cat_semicategory 𝔅.cat_semicategory
  ]:
  cat_prod_2_ObjI = smc_prod_2_ObjI 
  and cat_prod_2_ObjI'[cat_prod_cs_intros] = smc_prod_2_ObjI'
  and cat_prod_2_ObjE = smc_prod_2_ObjE
  and cat_prod_2_ArrI = smc_prod_2_ArrI
  and cat_prod_2_ArrI'[cat_prod_cs_intros] = smc_prod_2_ArrI'
  and cat_prod_2_ArrE = smc_prod_2_ArrE
  and cat_prod_2_is_arrI = smc_prod_2_is_arrI
  and cat_prod_2_is_arrI'[cat_prod_cs_intros] = smc_prod_2_is_arrI'
  and cat_prod_2_is_arrE = smc_prod_2_is_arrE
  and cat_prod_2_Dom_vsv = smc_prod_2_Dom_vsv
  and cat_prod_2_Dom_vdomain[cat_cs_simps] = smc_prod_2_Dom_vdomain
  and cat_prod_2_Dom_app[cat_prod_cs_simps] = smc_prod_2_Dom_app
  and cat_prod_2_Dom_vrange = smc_prod_2_Dom_vrange
  and cat_prod_2_Cod_vsv = smc_prod_2_Cod_vsv
  and cat_prod_2_Cod_vdomain[cat_cs_simps] = smc_prod_2_Cod_vdomain
  and cat_prod_2_Cod_app[cat_prod_cs_simps] = smc_prod_2_Cod_app
  and cat_prod_2_Cod_vrange = smc_prod_2_Cod_vrange
  and cat_prod_2_op_cat_cat_Obj[cat_op_simps] = smc_prod_2_op_smc_smc_Obj
  and cat_prod_2_cat_op_cat_Obj[cat_op_simps] = smc_prod_2_smc_op_smc_Obj
  and cat_prod_2_op_cat_cat_Arr[cat_op_simps] = smc_prod_2_op_smc_smc_Arr
  and cat_prod_2_cat_op_cat_Arr[cat_op_simps] = smc_prod_2_smc_op_smc_Arr

lemmas_with 
  [
    where 𝔄=‹cat_smc 𝔄› and 𝔅=‹cat_smc 𝔅›, 
    unfolded slicing_simps slicing_commute, 
    OF 𝔄.cat_semicategory 𝔅.cat_semicategory
  ]:
  cat_prod_2_Comp_app[cat_prod_cs_simps] = smc_prod_2_Comp_app

end


subsubsection‹Product of two categories is a category›

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

interpretation 𝒵 α by (rule categoryD[OF 𝔄])
interpretation 𝔄: category α 𝔄 by (rule 𝔄)
interpretation 𝔅: category α 𝔅 by (rule 𝔅)

lemma finite_pcategory_cat_prod_2: "finite_pcategory α (2ℕ) (if2 𝔄 𝔅)"
proof(intro finite_pcategoryI pcategory_baseI)
  from Axiom_of_Infinity show z1_in_Vset: "2ℕ ∈∘ Vset α" by blast
  show "category α (i = 0 ? 𝔄 : 𝔅)" if "i ∈∘ 2ℕ" for i
    by (auto simp: cat_cs_intros)
qed auto

interpretation finite_pcategory α ‹2ℕ› ‹if2 𝔄 𝔅›
  by (intro finite_pcategory_cat_prod_2 𝔄 𝔅)

lemma category_cat_prod_2[cat_cs_intros]: "category α (𝔄 ×C 𝔅)"
  unfolding cat_prod_2_def by (rule pcat_category_cat_prod)

end


subsubsection‹Identity›

lemma cat_prod_2_CId_vsv[cat_cs_intros]: "vsv ((𝔄 ×C 𝔅)⦇CId⦈)"
  unfolding cat_prod_2_def cat_prod_components by simp

lemma cat_prod_2_CId_vdomain[cat_cs_simps]: 
  "𝒟∘ ((𝔄 ×C 𝔅)⦇CId⦈) = (𝔄 ×C 𝔅)⦇Obj⦈"
  unfolding cat_prod_2_def cat_prod_components by simp

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

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

interpretation finite_pcategory α ‹2ℕ› ‹(λi. if i = 0 then 𝔄 else 𝔅)›
  by (intro finite_pcategory_cat_prod_2 𝔄 𝔅)

lemma cat_prod_2_CId_app[cat_prod_cs_simps]:
  assumes "[a, b]∘ ∈∘ (𝔄 ×C 𝔅)⦇Obj⦈"
  shows "(𝔄 ×C 𝔅)⦇CId⦈⦇a, b⦈∙ = [𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]∘"
proof-
  have "(𝔄 ×C 𝔅)⦇CId⦈⦇a, b⦈∙ = 
    (λi∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]∘⦇i⦈⦈)"
    by 
      (
        rule 
          cat_prod_CId_app[
            OF assms[unfolded cat_prod_2_def], folded cat_prod_2_def
            ]
      )
  also have 
    "(λi∈∘2ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]∘⦇i⦈⦈) = 
      [𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]∘"
  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ℕ. (if i = 0 then 𝔄 else 𝔅)⦇CId⦈⦇[a, b]∘⦇i⦈⦈)⦇i⦈ = 
        [𝔄⦇CId⦈⦇a⦈, 𝔅⦇CId⦈⦇b⦈]∘⦇i⦈"
      by cases (simp_all add: two nat_omega_simps)
  qed (auto simp: two nat_omega_simps)
  finally show ?thesis by simp
qed

lemma cat_prod_2_CId_vrange: "ℛ∘ ((𝔄 ×C 𝔅)⦇CId⦈) ⊆∘ (𝔄 ×C 𝔅)⦇Arr⦈"
proof(rule vsv.vsv_vrange_vsubset, unfold cat_cs_simps)
  show "vsv ((𝔄 ×C 𝔅)⦇CId⦈)" by (rule cat_prod_2_CId_vsv)
  fix ab assume "ab ∈∘ (𝔄 ×C 𝔅)⦇Obj⦈"
  then obtain a b where ab_def: "ab = [a, b]∘" 
    and a: "a ∈∘ 𝔄⦇Obj⦈" 
    and b: "b ∈∘ 𝔅⦇Obj⦈"
    by (elim cat_prod_2_ObjE[OF 𝔄 𝔅])
  from 𝔄 𝔅 a b show "(𝔄 ×C 𝔅)⦇CId⦈⦇ab⦈ ∈∘ (𝔄 ×C 𝔅)⦇Arr⦈"
    unfolding ab_def by (cs_concl cs_intro: cat_cs_intros cat_prod_cs_intros)
qed

end


subsubsection‹Opposite product category›

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

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

lemma op_smc_smc_prod_2[smc_op_simps]: 
  "op_cat (𝔄 ×C 𝔅) = op_cat 𝔄 ×C op_cat 𝔅"
proof(rule cat_smc_eqI [of α])
  from 𝔄 𝔅 show cat_lhs: "category α (op_cat (𝔄 ×C 𝔅))"
    by 
      (
        cs_concl cs_shallow
          cs_simp: cat_op_simps cs_intro