Theory CZH_ECAT_Ordinal

(* Copyright 2020 (C) Mihails Milehins *)

section‹Ordinal numbers›
theory CZH_ECAT_Ordinal
  imports CZH_ECAT_Small_Order
begin



subsection‹Background›


text‹
The content of this section is based on the treatment of the ordinal numbers
from the perspective of category theory as exposed, for example,
in Chapter I-2 in cite‹"mac_lane_categories_2010"›.
›

named_theorems cat_ordinal_cs_simps
named_theorems cat_ordinal_cs_intros



subsection‹Arrows associated with an ordinal number›

definition ordinal_arrs :: "V ⇒ V"
  where "ordinal_arrs A ≡ set {[a, b]∘ | a b. a ∈∘ A ∧ b ∈∘ A ∧ a ≤ b}"

lemma small_ordinal_arrs[simp]: 
  "small {[a, b]∘ | a b. a ∈∘ A ∧ b ∈∘ A ∧ a ≤ b}"
  by (rule down[where x=‹A ×∙ A›]) auto


text‹Rules.›

lemma ordinal_arrsI[cat_ordinal_cs_intros]:
  assumes "x = [a, b]∘" and "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" 
  shows "x ∈∘ ordinal_arrs A"
  using assms unfolding ordinal_arrs_def by auto

lemma ordinal_arrsD[dest]:
  assumes "[a, b]∘ ∈∘ ordinal_arrs A"
  shows "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" 
  using assms unfolding ordinal_arrs_def by auto

lemma ordinal_arrsE[elim]:
  assumes "x ∈∘ ordinal_arrs A"
  obtains a b where "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" and "x = [a, b]∘"
  using assms unfolding ordinal_arrs_def by clarsimp



subsection‹Composable arrows›

abbreviation ordinal_composable :: "V ⇒ V"
  where "ordinal_composable A ≡ set
    {
      [[b, c]∘, [a, b]∘]∘ | a b c. 
        a ∈∘ A ∧ b ∈∘ A ∧ c ∈∘ A ∧ a ≤ b ∧ b ≤ c
    }"

lemma small_ordinal_composable[simp]: 
  "small
    {
      [[b, c]∘, [a, b]∘]∘ | a b c.
        a ∈∘ A ∧ b ∈∘ A ∧ c ∈∘ A ∧ a ≤ b ∧ b ≤ c
    }"
  by (rule down[where x=‹(A ×∙ A) ×∙ (A ×∙ A)›]) auto


text‹Rules.›

lemma ordinal_composableI[cat_ordinal_cs_intros]:
  assumes "x = [[b, c]∘, [a, b]∘]∘" 
    and "a ∈∘ A"
    and "b ∈∘ A"
    and "c ∈∘ A"
    and "a ≤ b"
    and "b ≤ c"
  shows "x ∈∘ ordinal_composable A"
  using assms by auto

lemma ordinal_composableD[dest]:
  assumes "[[b, c]∘, [a, b]∘]∘ ∈∘ ordinal_composable A"
  shows "a ∈∘ A" and "b ∈∘ A" and "c ∈∘ A" and "a ≤ b" and "b ≤ c"
  using assms by auto

lemma ordinal_composableE[elim]:
  assumes "x ∈∘ ordinal_composable A"
  obtains a b c 
    where "x = [[b, c]∘, [a, b]∘]∘"
      and "a ∈∘ A" 
      and "b ∈∘ A" 
      and "c ∈∘ A"
      and "a ≤ b"
      and "b ≤ c"
  using assms by clarsimp



subsection‹Ordinal number as a category›


subsubsection‹Definition and elementary properties›

definition cat_ordinal :: "V ⇒ V"
  where "cat_ordinal A =
    [
      A,
      ordinal_arrs A,
      (λf∈∘ordinal_arrs A. f⦇0⦈),
      (λf∈∘ordinal_arrs A. f⦇1ℕ⦈),
      (λgf∈∘ordinal_composable A. [gf⦇1ℕ⦈⦇0⦈, gf⦇0⦈⦇1ℕ⦈]∘),
      (λx∈∘A. [x, x]∘)
    ]∘"


text‹Components.›

lemma cat_ordinal_components:
  shows [cat_ordinal_cs_simps]: "cat_ordinal A⦇Obj⦈ = A"
    and [cat_ordinal_cs_simps]: "cat_ordinal A⦇Arr⦈ = ordinal_arrs A"
    and "cat_ordinal A⦇Dom⦈ = (λf∈∘ordinal_arrs A. f⦇0⦈)"
    and "cat_ordinal A⦇Cod⦈ = (λf∈∘ordinal_arrs A. f⦇1ℕ⦈)"
    and "cat_ordinal A⦇Comp⦈ =
      (λgf∈∘ordinal_composable A. [gf⦇1ℕ⦈⦇0⦈, gf⦇0⦈⦇1ℕ⦈]∘)"
    and "cat_ordinal A⦇CId⦈ = (λx∈∘A. [x, x]∘)"
  unfolding cat_ordinal_def dg_field_simps by (simp_all add: nat_omega_simps)


subsubsection‹Domain›

mk_VLambda cat_ordinal_components(3)
  |vsv cat_ordinal_Dom_vsv[cat_ordinal_cs_intros]|
  |vdomain 
    cat_ordinal_Dom_vdomain[
      folded cat_ordinal_components, cat_ordinal_cs_simps
      ]
  |

lemma cat_ordinal_Dom_app[cat_ordinal_cs_simps]:
  assumes "x ∈∘ cat_ordinal A⦇Arr⦈" and "x = [a, b]∘"
  shows "cat_ordinal A⦇Dom⦈⦇x⦈ = a"
  using assms(1) unfolding assms(2) cat_ordinal_components by auto

lemma cat_ordinal_Dom_vrange: "ℛ∘ (cat_ordinal A⦇Dom⦈) ⊆∘ cat_ordinal A⦇Obj⦈"
  unfolding cat_ordinal_components
  by (intro vrange_VLambda_vsubset, elim ordinal_arrsE) simp


subsubsection‹Codomain›

mk_VLambda cat_ordinal_components(4)
  |vsv cat_ordinal_Cod_vsv[cat_ordinal_cs_intros]|
  |vdomain 
    cat_ordinal_Cod_vdomain[
      folded cat_ordinal_components, cat_ordinal_cs_simps
      ]
  |

lemma cat_ordinal_Cod_app[cat_ordinal_cs_simps]:
  assumes "x ∈∘ cat_ordinal A⦇Arr⦈" and "x = [a, b]∘"
  shows "cat_ordinal A⦇Cod⦈⦇x⦈ = b"
  using assms(1)
  unfolding assms(2) cat_ordinal_components 
  by (auto simp: nat_omega_simps)

lemma cat_ordinal_Cod_vrange: "ℛ∘ (cat_ordinal A⦇Cod⦈) ⊆∘ cat_ordinal A⦇Obj⦈"
  unfolding cat_ordinal_components
  by (intro vrange_VLambda_vsubset, elim ordinal_arrsE) 
    (simp add: nat_omega_simps)


subsubsection‹Arrow with a domain and a codomain›


text‹Rules.›

lemma cat_ordinal_is_arrI[cat_ordinal_cs_intros]:
  assumes "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" and "f = [a, b]∘"
  shows "f : a ↦⇘cat_ordinal A⇙ b"
proof(intro is_arrI, unfold cat_ordinal_components(2))
  from assms show "f ∈∘ ordinal_arrs A" by (intro ordinal_arrsI)
  then show "cat_ordinal A⦇Dom⦈⦇f⦈ = a" "cat_ordinal A⦇Cod⦈⦇f⦈ = b"
    by (cs_concl cs_simp: cat_ordinal_cs_simps assms(4))+
qed

lemma cat_ordinal_is_arrD[dest]:
  assumes "f : a ↦⇘cat_ordinal A⇙ b"
  shows "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" and "f = [a, b]∘"
proof-
  note f = is_arrD[OF assms, unfolded cat_ordinal_components(2)]
  from f(1) obtain a' b' 
    where a': "a' ∈∘ A" 
      and b': "b' ∈∘ A" 
      and a'b': "a' ≤ b'" 
      and f_def: "f = [a', b']∘"
    unfolding ordinal_arrs_def by clarsimp
  from f(2) a' b' a'b' have a'_def: "a' = a" 
    by 
      (
        cs_prems cs_shallow
          cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
      )
  from f(3) a' b' a'b' have b'_def: "b' = b"
    by 
      (
        cs_prems cs_shallow 
          cs_simp: cat_ordinal_cs_simps f_def cs_intro: cat_ordinal_cs_intros
      )
  from a' b' a'b' f_def show "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" and "f = [a, b]∘"
    unfolding a'_def b'_def by auto
qed

lemma cat_ordinal_is_arrE[elim]:
  assumes "f : a ↦⇘cat_ordinal A⇙ b"
  obtains "a ∈∘ A" and "b ∈∘ A" and "a ≤ b" and "f = [a, b]∘"
  using assms by auto


text‹Elementary properties.›

lemma cat_ordinal_is_arr_not:
  assumes "¬a ≤ b"
  shows "¬f : a ↦⇘cat_ordinal A⇙ b"
proof(rule ccontr, unfold not_not)
  assume "f : a ↦⇘cat_ordinal A⇙ b"
  with cat_ordinal_is_arrD(3)[OF this] assms show False by simp
qed

lemma cat_ordinal_is_arr_is_unique:
  assumes "f : a ↦⇘cat_ordinal A⇙ b" and "g : a ↦⇘cat_ordinal A⇙ b"  
  shows "f = g"
  by 
    (
      simp add: 
        cat_ordinal_is_arrD(4)[OF assms(1)] 
        cat_ordinal_is_arrD(4)[OF assms(2)]
    )

lemma cat_ordinal_Hom_ne:
  assumes "f : a ↦⇘cat_ordinal A⇙ b"
  shows "Hom (cat_ordinal A) a b = set {f}"
  using assms cat_ordinal_is_arr_is_unique 
  by (intro vsubset_antisym vsubsetI) auto

lemma cat_ordinal_Hom_empty:
  assumes "¬a ≤ b"
  shows "Hom (cat_ordinal A) a b = 0"
  using assms by (intro vsubset_antisym vsubsetI) auto

lemma cat_ordinal_inj:
  assumes "cat_ordinal m = cat_ordinal n"
  shows "m = n"
  by (metis assms cat_ordinal_components(1))


subsubsection‹Composition›

mk_VLambda cat_ordinal_components(5)
  |vsv cat_ordinal_Comp_vsv[cat_ordinal_cs_intros]|
  |vdomain cat_ordinal_Comp_vdomain[folded cat_ordinal_components, cat_cs_simps]|

lemma cat_ordinal_Comp_app[cat_ordinal_cs_simps]:
  assumes "g : b ↦⇘cat_ordinal A⇙ c" and "f : a ↦⇘cat_ordinal A⇙ b" 
  shows "g ∘A⇘cat_ordinal A⇙ f = [a, c]∘"
proof-
  from assms(2) have a: "a ∈∘ A" 
    and b: "b ∈∘ A" 
    and ab: "a ≤ b" 
    and f_def: "f = [a, b]∘" 
    by auto
  from assms(1) have c: "c ∈∘ A" and bc: "b ≤ c" and g_def: "g = [b, c]∘" 
    by auto
  from a b c ab bc have "[g, f]∘ ∈∘ ordinal_composable A"
    by (cs_concl cs_shallow cs_simp: g_def f_def cs_intro: cat_ordinal_cs_intros)
  then show "g ∘A⇘cat_ordinal A⇙ f = [a, c]∘"
    unfolding cat_ordinal_components by (simp add: g_def f_def nat_omega_simps)
qed


subsubsection‹Identity›

mk_VLambda cat_ordinal_components(6)
  |vsv cat_ordinal_CId_vsv[cat_ordinal_cs_intros]|
  |vdomain cat_ordinal_CId_vdomain[cat_ordinal_cs_simps]|
  |app cat_ordinal_CId_app[cat_ordinal_cs_simps]|


subsubsection‹Order relation›

lemma cat_ordinal_is_leD[dest]:
  assumes "a ≤O⇘cat_ordinal A⇙ b"
  shows "[a, b]∘ : a ↦⇘cat_ordinal A⇙ b"
proof(intro cat_ordinal_is_arrI)
  from is_leD[OF assms] obtain f where "f : a ↦⇘cat_ordinal A⇙ b" by fastforce
  then show "a ∈∘ A" "b ∈∘ A" "a ⊆∘ b" by auto
qed simp

lemma cat_ordinal_is_leE[elim]:
  assumes "a ≤O⇘cat_ordinal A⇙ b"
  obtains "[a, b]∘ : a ↦⇘cat_ordinal A⇙ b"
  using assms by auto 

lemma cat_ordinal_is_le_iff:
  "a ≤O⇘cat_ordinal A⇙ b ⟷ [a, b]∘ : a ↦⇘cat_ordinal A⇙ b"
  using cat_ordinal_is_leD cat_ordinal_is_leE 
  by (metis HomI is_le_def vempty_nin)


subsubsection‹Every ordinal number is a category›

lemma (in 𝒵) cat_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "Ord A" and "A ⊆∘ α"
  shows "cat_linear_order α (cat_ordinal A)"
proof(intro cat_linear_orderI cat_partial_orderI cat_preorderI categoryI')
  show "vfsequence (cat_ordinal A)" unfolding cat_ordinal_def by auto
  show "vcard (cat_ordinal A) = 6ℕ"
    unfolding cat_ordinal_def by (simp add: nat_omega_simps)
  show "ℛ∘ (cat_ordinal A⦇Dom⦈) ⊆∘ cat_ordinal A⦇Obj⦈"
    by (rule cat_ordinal_Dom_vrange)
  show "ℛ∘ (cat_ordinal A⦇Cod⦈) ⊆∘ cat_ordinal A⦇Obj⦈"
    by (rule cat_ordinal_Cod_vrange)
  show "(gf ∈∘ 𝒟∘ (cat_ordinal A⦇Comp⦈)) ⟷
    (
      ∃g f b c a.
        gf = [g, f]∘ ∧ g : b ↦⇘cat_ordinal A⇙ c ∧ f : a ↦⇘cat_ordinal A⇙ b
    )"
    for gf
    unfolding cat_ordinal_Comp_vdomain
  proof
    assume "gf ∈∘ ordinal_composable A"
    then obtain a b c
      where gf_def: "gf = [[b, c]∘, [a, b]∘]∘" 
        and a: "a ∈∘ A" 
        and b: "b ∈∘ A"
        and c: "c ∈∘ A"
        and ab: "a ≤ b"
        and bc: "b ≤ c"
      by clarsimp
    from a b c ab bc show 
      "∃g f b c a.
        gf = [g, f]∘ ∧ g : b ↦⇘cat_ordinal A⇙ c ∧ f : a ↦⇘cat_ordinal A⇙ b"
      unfolding gf_def
      by (intro exI conjI)
        (
          cs_concl cs_shallow 
            cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
        )+
  next
    assume 
      "∃g f b c a.
        gf = [g, f]∘ ∧
        g : b ↦⇘cat_ordinal A⇙ c ∧ 
        f : a ↦⇘cat_ordinal A⇙ b"
    then obtain g f b c a
      where gf_def: "gf = [g, f]∘"
        and g: "g : b ↦⇘cat_ordinal A⇙ c"
        and f: "f : a ↦⇘cat_ordinal A⇙ b"
      by clarsimp
    note g = cat_ordinal_is_arrD[OF g]
    note f = cat_ordinal_is_arrD[OF f]
    from g(1-3) f(1-3) show "gf ∈∘ ordinal_composable A"
      unfolding gf_def g(4) f(4)
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
        )
  qed
  show [cat_ordinal_cs_intros]: "g ∘A⇘cat_ordinal A⇙ f : a ↦⇘cat_ordinal A⇙ c"
    if "g : b ↦⇘cat_ordinal A⇙ c" and "f : a ↦⇘cat_ordinal A⇙ b" for b c g a f
  proof-
    note g = cat_ordinal_is_arrD[OF that(1)]
    note f = cat_ordinal_is_arrD[OF that(2)]
    show ?thesis
    proof(intro cat_ordinal_is_arrI g(1,2) f(1,2), unfold g(4) f(4))
      from g(3) f(3) show "a ⊆∘ c" by auto
      from g(1,2,3) f(1,2,3) show " [b, c]∘ ∘A⇘cat_ordinal A⇙ [a, b]∘ = [a, c]∘"
        by 
          (
            cs_concl cs_shallow 
              cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros
          )
    qed
  qed
  show
    "h ∘A⇘cat_ordinal A⇙ g ∘A⇘cat_ordinal A⇙ f =
      h ∘A⇘cat_ordinal A⇙ (g ∘A⇘cat_ordinal A⇙ f)"
    if "h : c ↦⇘cat_ordinal A⇙ d"
      and "g : b ↦⇘cat_ordinal A⇙ c"
      and "f : a ↦⇘cat_ordinal A⇙ b"
    for c d h b g a f
  proof-
    note h = cat_ordinal_is_arrD[OF that(1)]
    note g = cat_ordinal_is_arrD[OF that(2)]
    note f = cat_ordinal_is_arrD[OF that(3)]
    from that(1-3) h(1-3) g(1-4) f(1-3) show ?thesis
      unfolding h(4) g(4) f(4) (*slow*)
      by (cs_concl cs_simp: cat_ordinal_cs_simps cs_intro: cat_ordinal_cs_intros)
  qed
  show "cat_ordinal A⦇CId⦈⦇a⦈ : a ↦⇘cat_ordinal A⇙ a"
    if "a ∈∘ cat_ordinal A⦇Obj⦈" for a
  proof- 
    from that have "a ∈∘ A" unfolding cat_ordinal_components by simp
    then show "cat_ordinal A⦇CId⦈⦇a⦈ : a ↦⇘cat_ordinal A⇙ a"
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_ordinal_cs_simps
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
  qed
  show "cat_ordinal A⦇CId⦈⦇b⦈ ∘A⇘cat_ordinal A⇙ f = f"
    if "f : a ↦⇘cat_ordinal A⇙ b" for a b f
  proof-
    note f = cat_ordinal_is_arrD[OF that]
    from f(1-3) show ?thesis
      by 
        (
          cs_concl cs_shallow
            cs_simp: cat_ordinal_cs_simps f(4)
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
  qed
  show "f ∘A⇘cat_ordinal A⇙ cat_ordinal A⦇CId⦈⦇b⦈ = f"
    if "f : b ↦⇘cat_ordinal A⇙ c" for b c f
  proof-
    note f = cat_ordinal_is_arrD[OF that]
    from f(1-3) show ?thesis
      by 
        (
          cs_concl cs_shallow 
            cs_simp: cat_ordinal_cs_simps f(4)
            cs_intro: cat_ordinal_cs_intros V_cs_intros
        )
  qed
  from assms Ord_α show "cat_ordinal A⦇Obj⦈ ⊆∘ Vset α"
    unfolding cat_ordinal_components by auto
  show "(⋃∘b∈∘B. ⋃∘c∈∘C. Hom (cat_ordinal A) b c) ∈∘ Vset α"
    if "B ⊆∘ cat_ordinal A⦇Obj⦈" 
      and "C ⊆∘ cat_ordinal A⦇Obj⦈"
      and "B ∈∘ Vset α"
      and "C ∈∘ Vset α"
    for B C
  proof-
    have "(⋃∘b∈∘B. ⋃∘c∈∘C. Hom (cat_ordinal A) b c) ⊆∘ B ×∙ C"
    proof(rule vsubsetI)
      fix f assume "f ∈∘ (⋃∘b∈∘B. ⋃∘c∈∘C. Hom (cat_ordinal A) b c)"
      then obtain b c 
        where b: "b ∈∘ B" and c: "c ∈∘ C" and f: "f : b ↦⇘cat_ordinal A⇙ c" 
        by auto
      note f = cat_ordinal_is_arrD[OF f]
      from b c show "f ∈∘ B ×∙ C"
        unfolding f(4) by auto
    qed
    moreover from that(3,4) have "B ×∙ C ∈∘ Vset α"
      by (auto intro: Limit_ftimes_in_VsetI)
    ultimately show ?thesis by blast
  qed
  show "(∃f. Hom (cat_ordinal A) a b = set {f}) ∨ Hom (cat_ordinal A) a b = 0"
    if "a ∈∘ cat_ordinal A⦇Obj⦈" and "b ∈∘ cat_ordinal A⦇Obj⦈" for a b
  proof-
    from that have a: "a ∈∘ A" and b: "b ∈∘ A"
      unfolding cat_ordinal_components by simp_all
    then consider ‹a ≤ b› | ‹¬a ≤ b› by auto
    then show ?thesis
    proof cases
      case 1
      with a b have "[a, b]∘ : a ↦⇘cat_ordinal A⇙ b"
        by (auto intro: cat_ordinal_is_arrI)
      then show ?thesis by (simp add: cat_ordinal_Hom_ne)
    qed (simp add: cat_ordinal_Hom_empty)
  qed
  show "a = b"
    if "a ∈∘ cat_ordinal A⦇Obj⦈"
      and "b ∈∘ cat_ordinal A⦇Obj⦈"
      and "a ≤O⇘cat_ordinal A⇙ b"
      and "b ≤O⇘cat_ordinal A⇙ a"
    for a b
    using 
      that(3,4)[unfolded cat_ordinal_is_le_iff cat_ordinal_components]
      cat_ordinal_is_arr_is_unique
    by auto
  show "a ≤O⇘cat_ordinal A⇙ b ∨ b ≤O⇘cat_ordinal A⇙ a"
    if "a ∈∘ cat_ordinal A⦇Obj⦈" and "b ∈∘ cat_ordinal A⦇Obj⦈" for a b
  proof-
    from that[unfolded cat_ordinal_components] have a: "a ∈∘ A" and b: "b ∈∘ A"
      by simp_all
    with assms have "Ord a" "Ord b" by auto
    then consider ‹a ≤ b› | ‹b ≤ a› by (meson Ord_linear_le)
    then show "a ≤O⇘cat_ordinal A⇙ b ∨ b ≤O⇘cat_ordinal A⇙ a"
      by cases (auto simp: a b cat_ordinal_is_le_iff intro: cat_ordinal_is_arrI)
  qed
qed (auto intro: cat_ordinal_cs_intros simp: cat_ordinal_cs_simps)

lemmas [cat_ordinal_cs_intros] = 𝒵.cat_linear_order_cat_ordinal

lemma (in 𝒵) cat_tiny_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "Ord A" and "A ∈∘ α"
  shows "cat_tiny_linear_order α (cat_ordinal A)"
proof(intro cat_tiny_linear_orderI' cat_linear_order_cat_ordinal assms(1))
  from assms show "A ⊆∘ α"
    by (meson Ord_α Ord_linear_le mem_not_refl vsubsetE)
  from assms(1) this interpret A: cat_linear_order α ‹cat_ordinal A›
    by (intro cat_linear_order_cat_ordinal)
  from assms(2) have A_in_Vset: "A ∈∘ Vset α" by (simp add: Ord_α Ord_in_in_VsetI)
  have "cat_ordinal A⦇Arr⦈ ⊆∘ A ×∙ A"
    unfolding ordinal_arrs_def cat_ordinal_components by clarsimp
  moreover from A_in_Vset have "A ×∙ A ∈∘ Vset α"
    by (intro Limit_ftimes_in_VsetI) auto
  ultimately have "cat_ordinal A⦇Arr⦈ ∈∘ Vset α"
    using vsubset_in_VsetI unfolding cat_ordinal_components by simp
  moreover have "cat_ordinal A⦇Obj⦈ ∈∘ Vset α"
    unfolding cat_ordinal_components by (intro A_in_Vset)
  ultimately show "tiny_category α (cat_ordinal A)"
    by (cs_concl cs_shallow cs_intro: cat_cs_intros tiny_categoryI')
qed

lemmas [cat_ordinal_cs_intros] = 𝒵.cat_linear_order_cat_ordinal

lemma (in 𝒵) finite_category_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "a ∈∘ ω"
  shows "finite_category α (cat_ordinal a)"
proof-
  from assms have "Ord a" "a ∈∘ α" by (auto simp: Ord_α Ord_trans)
  then interpret cat_ordinal: cat_tiny_linear_order α ‹cat_ordinal a›
    by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
  show ?thesis
  proof(intro finite_categoryI')
    from assms show "category α (cat_ordinal a)"
      by (cs_concl cs_shallow cs_intro: cat_cs_intros)
    from assms show "vfinite (cat_ordinal a⦇Obj⦈)"
      unfolding cat_ordinal_components by auto
    from assms show "vfinite (cat_ordinal a⦇Arr⦈)"
    proof-
      have "cat_ordinal a⦇Arr⦈ ⊆∘ a ×∙ a"
        unfolding cat_ordinal_components by auto
      moreover from assms have "vfinite (a ×∙ a)"
        by (intro vfinite_ftimesI) auto
      ultimately show ?thesis by (auto simp: vfinite_vsubset)
    qed
  qed
qed

lemmas [cat_ordinal_cs_intros] = 𝒵.finite_category_cat_ordinal

end