Theory CZH_DG_Digraph

(* Copyright 2021 (C) Mihails Milehins *)

section‹Digraph\label{sec:digraph}›
theory CZH_DG_Digraph
  imports CZH_DG_Introduction
begin



subsection‹Background›

named_theorems dg_field_simps

definition Obj :: V where [dg_field_simps]: "Obj = 0"
definition Arr :: V where [dg_field_simps]: "Arr = 1ℕ"
definition Dom :: V where [dg_field_simps]: "Dom = 2ℕ"
definition Cod :: V where [dg_field_simps]: "Cod = 3ℕ"



subsection‹Arrow with a domain and a codomain›


text‹
The definition of and notation for an arrow with a domain and codomain is
adapted from Chapter I-1 in cite‹"mac_lane_categories_2010"›.
The definition is applicable to digraphs and all other relevant derived
entities, such as semicategories and categories, that are presented in
the subsequent chapters.

In this work, by convention, the definition of an arrow with a domain and a 
codomain is nearly always preferred to the explicit use of the domain 
and codomain functions for the specification of the fundamental properties 
of arrows.
Thus, to say that ‹f› is an arrow with the domain ‹a›, it is preferable
to write ‹f : a ↦ℭ b› (‹b› can be assumed to be arbitrary) instead
of term‹f ∈∘ ℭ⦇Arr⦈› and term‹ℭ⦇Dom⦈⦇f⦈ = a›.
›

definition is_arr :: "V ⇒ V ⇒ V ⇒ V ⇒ bool"
  where "is_arr ℭ a b f ⟷ f ∈∘ ℭ⦇Arr⦈ ∧ ℭ⦇Dom⦈⦇f⦈ = a ∧ ℭ⦇Cod⦈⦇f⦈ = b"

syntax "_is_arr" :: "V ⇒ V ⇒ V ⇒ V ⇒ bool" (‹_ : _ ↦ı _› [51, 51, 51] 51)
translations "f : a ↦⇘ℭ⇙ b" ⇌ "CONST is_arr ℭ a b f"


text‹Rules.›

mk_ide is_arr_def
  |intro is_arrI|
  |dest is_arrD[dest]|
  |elim is_arrE[elim]|

lemmas [dg_shared_cs_intros, dg_cs_intros] = is_arrD(1)
lemmas [dg_shared_cs_simps, dg_cs_simps] = is_arrD(2,3)



subsection‹‹Hom›-set›


text‹See Chapter I-8 in cite‹"mac_lane_categories_2010"›.›

abbreviation Hom :: "V ⇒ V ⇒ V ⇒ V" 
  where "Hom ℭ a b ≡ set {f. f : a ↦⇘ℭ⇙ b}"

lemma small_Hom[simp]: "small {f. f : a ↦⇘ℭ⇙ b}" unfolding is_arr_def by simp


text‹Rules.›

lemma HomI[dg_shared_cs_intros, dg_cs_intros]:
  assumes "f : a ↦⇘ℭ⇙ b"
  shows "f ∈∘ Hom ℭ a b"
  using assms by auto

lemma in_Hom_iff[dg_shared_cs_simps, dg_cs_simps]: 
  "f ∈∘ Hom ℭ a b ⟷ f : a ↦⇘ℭ⇙ b" 
  by simp


text‹
The ‹Hom›-sets in a given digraph are pairwise disjoint. This property 
was exposed as Axiom (v) in an alternative definition of a category presented 
in Chapter I-8 in cite‹"mac_lane_categories_2010"›. Within the scope of the 
definitional framework employed in this study, this property holds 
unconditionally.
›

lemma Hom_vdisjnt: 
  assumes "a ≠ a' ∨ b ≠ b'" 
    and "a ∈∘ ℭ⦇Obj⦈"
    and "a' ∈∘ ℭ⦇Obj⦈"
    and "b ∈∘ ℭ⦇Obj⦈" 
    and "b' ∈∘ ℭ⦇Obj⦈"
  shows "vdisjnt (Hom ℭ a b) (Hom ℭ a' b')"
proof(intro vdisjntI, unfold in_Hom_iff)
  fix g f assume "g : a ↦⇘ℭ⇙ b" and "f : a' ↦⇘ℭ⇙ b'" 
  then have "g ∈∘ ℭ⦇Arr⦈"
    and "f ∈∘ ℭ⦇Arr⦈"
    and "ℭ⦇Dom⦈⦇g⦈ = a"
    and "ℭ⦇Cod⦈⦇g⦈ = b"
    and "ℭ⦇Dom⦈⦇f⦈ = a'"
    and "ℭ⦇Cod⦈⦇f⦈ = b'"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
  with assms(1) have "ℭ⦇Dom⦈⦇g⦈ ≠ ℭ⦇Dom⦈⦇f⦈ ∨ ℭ⦇Cod⦈⦇g⦈ ≠ ℭ⦇Cod⦈⦇f⦈" by auto
  then show "g ≠ f" by clarsimp
qed



subsection‹Digraph: background information›


text‹
The definition of a digraph that is employed in this work is similar
to the definition of a ‹directed graph› presented in Chapter I-2 in 
cite‹"mac_lane_categories_2010"›. However, there are notable differences.
More specifically, the definition is parameterized by a limit ordinal ‹α›, 
such that ‹ω < α›; the set of objects is assumed to be a subset 
of the set ‹Vα› in the von Neumann hierarchy of sets (e.g., 
see cite‹"takeuti_introduction_1971"›). Such digraphs are called ‹α›-‹digraphs› 
to make the dependence on the parameter ‹α› explicit.\footnote{
The prefix ``‹α›-'' may be omitted whenever it is possible to infer the value 
of ‹α› from the context. This applies not only to the digraphs, but all 
other entities that are parameterized by a limit ordinal ‹α› such that 
‹ω < α›.} This definition was inspired by the ideas expressed in 
cite‹"feferman_set-theoretical_1969"›, cite‹"sica_doing_2006"› and
cite‹"shulman_set_2008"›.

In ZFC in HOL, the predicate term‹small› is used for distinguishing the
terms of any type of the form typ‹'a set› that are isomorphic to elements 
of a term of the type typ‹V› (the elements can be exposed via the predicate
const‹elts›). Thus, the collection of the elements associated with any term of 
the type typ‹V› (e.g., term‹elts (a::V)›) is always small 
(see the theorem @{thm [source] small_elts} in cite‹"paulson_zermelo_2019"›).
Therefore, in this study, in an attempt to avoid confusion, the term ``small''
is never used to refer to digraphs. 
Instead, a new terminology is introduced in this body of work.

Thus, in this work, an ‹α›-digraph is a tiny ‹α›-digraph if and only if 
the set of its objects and the set of its arrows both belong to the set ‹Vα›. 
This notion is similar to the notion of a small category in the sense of 
the definition employed in Chapter I-6 in cite‹"mac_lane_categories_2010"›, 
if it is assumed that the ``smallness'' is determined with respect to the 
set ‹Vα› instead of the universe ‹U›. Also, in what follows, any member of 
the set ‹Vα› will be referred to as an ‹α›-tiny set.

All of the large (i.e. non-tiny) digraphs 
that are considered within the scope of this work have a slightly 
unconventional condition associated with the size of their ‹Hom›-sets. 
This condition implies that all ‹Hom›-sets of a digraph 
are tiny, but it is not equivalent to 
all ‹Hom›-sets being tiny. The condition was introduced in an attempt to
resolve some of the issues related to the lack of an analogue of the 
Axiom Schema of Replacement closed with respect to ‹Vα›. 
›



subsection‹Digraph: definition and elementary properties›

locale digraph = 𝒵 α + vfsequence ℭ + Dom: vsv ‹ℭ⦇Dom⦈› + Cod: vsv ‹ℭ⦇Cod⦈› 
  for α ℭ +
  assumes dg_length[dg_cs_simps]: "vcard ℭ = 4ℕ"  
    and dg_Dom_vdomain[dg_cs_simps]: "𝒟∘ (ℭ⦇Dom⦈) = ℭ⦇Arr⦈"    
    and dg_Dom_vrange: "ℛ∘ (ℭ⦇Dom⦈) ⊆∘ ℭ⦇Obj⦈"
    and dg_Cod_vdomain[dg_cs_simps]: "𝒟∘ (ℭ⦇Cod⦈) = ℭ⦇Arr⦈"
    and dg_Cod_vrange: "ℛ∘ (ℭ⦇Cod⦈) ⊆∘ ℭ⦇Obj⦈"
    and dg_Obj_vsubset_Vset: "ℭ⦇Obj⦈ ⊆∘ Vset α"
    and dg_Hom_vifunion_in_Vset[dg_cs_intros]: 
      "⟦ A ⊆∘ ℭ⦇Obj⦈; B ⊆∘ ℭ⦇Obj⦈; A ∈∘ Vset α; B ∈∘ Vset α ⟧ ⟹ 
        (⋃∘a∈∘A. ⋃∘b∈∘B. Hom ℭ a b) ∈∘ Vset α"

lemmas [dg_cs_simps] = 
  digraph.dg_length
  digraph.dg_Dom_vdomain
  digraph.dg_Cod_vdomain

lemmas [dg_cs_intros] = 
  digraph.dg_Hom_vifunion_in_Vset


text‹Rules.›

lemma (in digraph) digraph_axioms'[dg_cs_intros]:
  assumes "α' = α"
  shows "digraph α' ℭ"
  unfolding assms by (rule digraph_axioms)

mk_ide rf digraph_def[unfolded digraph_axioms_def]
  |intro digraphI|
  |dest digraphD[dest]|
  |elim digraphE[elim]|


text‹Elementary properties.›

lemma dg_eqI:
  assumes "digraph α 𝔄" 
    and "digraph α 𝔅"
    and "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈"
    and "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈"
    and "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈"
    and "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
  shows "𝔄 = 𝔅"
proof-
  interpret 𝔄: digraph α 𝔄 by (rule assms(1))
  interpret 𝔅: digraph α 𝔅 by (rule assms(2))
  show ?thesis
  proof(rule vsv_eqI)
    have dom_lhs: "𝒟∘ 𝔄 = 4ℕ" 
      by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps)
    show "a ∈∘ 𝒟∘ 𝔄 ⟹ 𝔄⦇a⦈ = 𝔅⦇a⦈" for a 
      by (unfold dom_lhs, elim_in_numeral, insert assms)
        (auto simp: dg_field_simps)
  qed 
    (
      cs_concl cs_shallow 
        cs_simp: V_cs_simps dg_cs_simps cs_intro: V_cs_intros
    )+
qed

lemma (in digraph) dg_def: "ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]∘"
proof(rule vsv_eqI)
  have dom_lhs: "𝒟∘ ℭ = 4ℕ" 
    by (cs_concl cs_shallow cs_simp: V_cs_simps dg_cs_simps)
  have dom_rhs: "𝒟∘ [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]∘ = 4ℕ"
    by (simp add: nat_omega_simps)
  then show "𝒟∘ ℭ = 𝒟∘ [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]∘"
    unfolding dom_lhs dom_rhs by simp
  show "a ∈∘ 𝒟∘ ℭ ⟹ ℭ⦇a⦈ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Dom⦈, ℭ⦇Cod⦈]∘⦇a⦈" for a
    by (unfold dom_lhs, elim_in_numeral, unfold dg_field_simps)
      (simp_all add: nat_omega_simps)
qed (auto simp: vsv_axioms)

lemma (in digraph) dg_Obj_if_Dom_vrange:
  assumes "a ∈∘ ℛ∘ (ℭ⦇Dom⦈)"
  shows "a ∈∘ ℭ⦇Obj⦈"
  using assms dg_Dom_vrange by auto

lemma (in digraph) dg_Obj_if_Cod_vrange:
  assumes "a ∈∘ ℛ∘ (ℭ⦇Cod⦈)"
  shows "a ∈∘ ℭ⦇Obj⦈"
  using assms dg_Cod_vrange by auto

lemma (in digraph) dg_is_arrD:
  assumes "f : a ↦⇘ℭ⇙ b" 
  shows "f ∈∘ ℭ⦇Arr⦈" 
    and "a ∈∘ ℭ⦇Obj⦈"
    and "b ∈∘ ℭ⦇Obj⦈"
    and "ℭ⦇Dom⦈⦇f⦈ = a" 
    and "ℭ⦇Cod⦈⦇f⦈ = b"
proof-
  from assms show prems: "f ∈∘ ℭ⦇Arr⦈" 
    and fa[symmetric]: "ℭ⦇Dom⦈⦇f⦈ = a"
    and fb[symmetric]: "ℭ⦇Cod⦈⦇f⦈ = b"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
  from digraph_axioms prems have "f ∈∘ 𝒟∘ (ℭ⦇Dom⦈)" "f ∈∘ 𝒟∘ (ℭ⦇Cod⦈)"
    by (cs_concl cs_shallow cs_simp: dg_cs_simps)+
  with assms show "a ∈∘ ℭ⦇Obj⦈" "b ∈∘ ℭ⦇Obj⦈"  
    by 
      (
        cs_concl 
          cs_intro: dg_Obj_if_Dom_vrange dg_Obj_if_Cod_vrange V_cs_intros
          cs_simp: fa fb
      )+
qed

lemmas [dg_cs_intros] = digraph.dg_is_arrD(1-3)

lemma (in digraph) dg_is_arrE[elim]:
  assumes "f : a ↦⇘ℭ⇙ b" 
  obtains "f ∈∘ ℭ⦇Arr⦈" 
    and "a ∈∘ ℭ⦇Obj⦈"
    and "b ∈∘ ℭ⦇Obj⦈"
    and "ℭ⦇Dom⦈⦇f⦈ = a" 
    and "ℭ⦇Cod⦈⦇f⦈ = b"
  using assms by (blast dest: dg_is_arrD)

lemma (in digraph) dg_in_ArrE[elim]:
  assumes "f ∈∘ ℭ⦇Arr⦈"
  obtains a b where "f : a ↦⇘ℭ⇙ b" and "a ∈∘ ℭ⦇Obj⦈" and "b ∈∘ ℭ⦇Obj⦈"
  using assms by (auto dest: dg_is_arrD(2,3) is_arrI)

lemma (in digraph) dg_Hom_in_Vset[dg_cs_intros]: 
  assumes "a ∈∘ ℭ⦇Obj⦈" and "b ∈∘ ℭ⦇Obj⦈"
  shows "Hom ℭ a b ∈∘ Vset α"
proof-
  let ?A = ‹set {a}› and ?B = ‹set {b}›
  from assms have A: "?A ⊆∘ ℭ⦇Obj⦈" and B: "?B ⊆∘ ℭ⦇Obj⦈" by auto
  from assms dg_Obj_vsubset_Vset have "a ∈∘ Vset α" and "b ∈∘ Vset α" by auto
  then have a: "set {a} ∈∘ Vset α" and b: "set {b} ∈∘ Vset α" 
    by (metis Axiom_of_Pairing insert_absorb2)+
  from dg_Hom_vifunion_in_Vset[OF A B a b] show "Hom ℭ a b ∈∘ Vset α" by simp
qed

lemmas [dg_cs_intros] = digraph.dg_Hom_in_Vset


text‹Size.›

lemma (in digraph) dg_Arr_vsubset_Vset: "ℭ⦇Arr⦈ ⊆∘ Vset α"
proof(intro vsubsetI)
  fix f assume "f ∈∘ ℭ⦇Arr⦈"
  then obtain a b 
    where f: "f : a ↦⇘ℭ⇙ b" and a: "a ∈∘ ℭ⦇Obj⦈" and b: "b ∈∘ ℭ⦇Obj⦈"
    by blast
  show "f ∈∘ Vset α"
    by (rule Vset_trans, rule HomI[OF f], rule dg_Hom_in_Vset[OF a b])
qed

lemma (in digraph) dg_Dom_vsubset_Vset: "ℭ⦇Dom⦈ ⊆∘ Vset α"
  by 
    (
      rule Dom.vbrelation_Limit_vsubset_VsetI, 
      unfold dg_cs_simps, 
      insert dg_Dom_vrange dg_Obj_vsubset_Vset
    )
    (auto intro!: dg_Arr_vsubset_Vset)

lemma (in digraph) dg_Cod_vsubset_Vset: "ℭ⦇Cod⦈ ⊆∘ Vset α"
  by 
    (
      rule Cod.vbrelation_Limit_vsubset_VsetI, 
      unfold dg_cs_simps, 
      insert dg_Cod_vrange dg_Obj_vsubset_Vset
    )
    (auto intro!: dg_Arr_vsubset_Vset)

lemma (in digraph) dg_digraph_in_Vset_4: "ℭ ∈∘ Vset (α + 4ℕ)"
proof-
  note [folded VPow_iff, folded Vset_succ[OF Ord_α], dg_cs_intros] =
    dg_Obj_vsubset_Vset
    dg_Arr_vsubset_Vset
    dg_Dom_vsubset_Vset
    dg_Cod_vsubset_Vset
  show ?thesis
    by (subst dg_def, succ_of_numeral)
      (
        cs_concl 
          cs_simp: plus_V_succ_right V_cs_simps 
          cs_intro: dg_cs_intros V_cs_intros
      )
qed

lemma (in digraph) dg_Obj_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β"
  shows "ℭ⦇Obj⦈ ∈∘ Vset β"
  using assms dg_Obj_vsubset_Vset Vset_in_mono by auto

lemma (in digraph) dg_in_Obj_in_Vset[dg_cs_intros]:
  assumes "a ∈∘ ℭ⦇Obj⦈"
  shows "a ∈∘ Vset α"
  using assms dg_Obj_vsubset_Vset by auto

lemma (in digraph) dg_Arr_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β"
  shows "ℭ⦇Arr⦈ ∈∘ Vset β"
  using assms dg_Arr_vsubset_Vset Vset_in_mono by auto

lemma (in digraph) dg_in_Arr_in_Vset[dg_cs_intros]:
  assumes "a ∈∘ ℭ⦇Arr⦈"
  shows "a ∈∘ Vset α"
  using assms dg_Arr_vsubset_Vset by auto

lemma (in digraph) dg_Dom_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β"
  shows "ℭ⦇Dom⦈ ∈∘ Vset β"
  by (meson assms dg_Dom_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in digraph) dg_Cod_in_Vset:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "ℭ⦇Cod⦈ ∈∘ Vset β"
  by (meson assms dg_Cod_vsubset_Vset Vset_in_mono vsubset_in_VsetI)

lemma (in digraph) dg_in_Vset:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "ℭ ∈∘ Vset β"
proof-
  interpret β: 𝒵 β by (rule assms(1))
  note [dg_cs_intros] = 
    dg_Obj_in_Vset dg_Arr_in_Vset dg_Dom_in_Vset dg_Cod_in_Vset 
  from assms(2) show ?thesis
    by (subst dg_def) 
      (cs_concl cs_shallow cs_intro: dg_cs_intros V_cs_intros)
 qed

lemma (in digraph) dg_digraph_if_ge_Limit:
  assumes "𝒵 β" and "α ∈∘ β"
  shows "digraph β ℭ"
proof(rule digraphI)
  show "vfsequence ℭ" by (simp add: vfsequence_axioms)
  show "ℭ⦇Obj⦈ ⊆∘ Vset β"
    by (rule vsubsetI) 
      (meson Vset_in_mono Vset_trans assms(2) dg_Obj_vsubset_Vset vsubsetE)
  fix A B assume "A ⊆∘ ℭ⦇Obj⦈" "B ⊆∘ ℭ⦇Obj⦈" "A ∈∘ Vset β" "B ∈∘ Vset β"
  then have "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom ℭ a b) ⊆∘ ℭ⦇Arr⦈" by auto
  moreover note dg_Arr_vsubset_Vset
  moreover have "Vset α ∈∘ Vset β" by (simp add: Vset_in_mono assms(2))
  ultimately show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom ℭ a b) ∈∘ Vset β" by auto
qed (auto simp: assms(1) dg_Dom_vrange dg_Cod_vrange dg_cs_simps)

lemma small_digraph[simp]: "small {ℭ. digraph α ℭ}"
proof(cases ‹𝒵 α›)
  case True
  with digraph.dg_in_Vset show ?thesis
    by (intro down[of _ ‹Vset (α + ω)›] subsetI)
      (auto simp: 𝒵.𝒵_Limit_αω 𝒵.𝒵_ω_αω 𝒵.intro 𝒵.𝒵_α_αω)
next
  case False
  then have "{ℭ. digraph α ℭ} = {}" by auto
  then show ?thesis by simp
qed

lemma (in 𝒵) digraphs_in_Vset: 
  assumes "𝒵 β" and "α ∈∘ β"
  shows "set {ℭ. digraph α ℭ} ∈∘ Vset β"
proof(rule vsubset_in_VsetI)
  interpret β: 𝒵 β by (rule assms(1))
  show "set {ℭ. digraph α ℭ} ⊆∘ Vset (α + 4ℕ)"
  proof(intro vsubsetI)
    fix ℭ assume "ℭ ∈∘ set {ℭ. digraph α ℭ}"
    then interpret digraph α ℭ by simp
    show "ℭ ∈∘ Vset (α + 4ℕ)"
      unfolding VPow_iff by (rule dg_digraph_in_Vset_4)
  qed
  from assms(2) show "Vset (α + 4ℕ) ∈∘ Vset β"
    by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
qed

lemma digraph_if_digraph:
  assumes "digraph β ℭ"
    and "𝒵 α"
    and "ℭ⦇Obj⦈ ⊆∘ Vset α"
    and "⋀A B. ⟦ A ⊆∘ ℭ⦇Obj⦈; B ⊆∘ ℭ⦇Obj⦈; A ∈∘ Vset α; B ∈∘ Vset α ⟧ ⟹
      (⋃∘a∈∘A. ⋃∘b∈∘B. Hom ℭ a b) ∈∘ Vset α"
  shows "digraph α ℭ"
proof-
  interpret digraph β ℭ by (rule assms(1))
  interpret α: 𝒵 α by (rule assms(2))
  show ?thesis
  proof(intro digraphI)
    show "vfsequence ℭ" by (simp add: vfsequence_axioms)
    show "(⋃∘a∈∘A. ⋃∘b∈∘B. Hom ℭ a b) ∈∘ Vset α"
      if "A ⊆∘ ℭ⦇Obj⦈" "B ⊆∘ ℭ⦇Obj⦈" "A ∈∘ Vset α" "B ∈∘ Vset α" for A B
      by (rule assms(4)[OF that])
  qed (auto simp: assms(3) dg_Cod_vrange dg_cs_simps intro!: dg_Dom_vrange)
qed


text‹Further properties.›

lemma (in digraph) dg_Dom_app_in_Obj:
  assumes "f ∈∘ ℭ⦇Arr⦈"
  shows "ℭ⦇Dom⦈⦇f⦈ ∈∘ ℭ⦇Obj⦈"
  using assms dg_Dom_vrange by (auto simp: Dom.vsv_vimageI2)

lemma (in digraph) dg_Cod_app_in_Obj:
  assumes "f ∈∘ ℭ⦇Arr⦈"
  shows "ℭ⦇Cod⦈⦇f⦈ ∈∘ ℭ⦇Obj⦈"
  using assms dg_Cod_vrange by (auto simp: Cod.vsv_vimageI2)

lemma (in digraph) dg_Arr_vempty_if_Obj_vempty:
  assumes "ℭ⦇Obj⦈ = 0"
  shows "ℭ⦇Arr⦈ = 0"
  by (metis assms eq0_iff dg_Cod_app_in_Obj)

lemma (in digraph) dg_Dom_vempty_if_Arr_vempty:
  assumes "ℭ⦇Arr⦈ = 0"
  shows "ℭ⦇Dom⦈ = 0"
  using assms Dom.vdomain_vrange_is_vempty 
  by (auto intro: Dom.vsv_vrange_vempty simp: dg_cs_simps)

lemma (in digraph) dg_Cod_vempty_if_Arr_vempty:
  assumes "ℭ⦇Arr⦈ = 0"
  shows "ℭ⦇Cod⦈ = 0"
  using assms Cod.vdomain_vrange_is_vempty 
  by (auto intro: Cod.vsv_vrange_vempty simp: dg_cs_simps)



subsection‹Opposite digraph›


subsubsection‹Definition and elementary properties›


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

definition op_dg :: "V ⇒ V"
  where "op_dg ℭ = [ℭ⦇Obj⦈, ℭ⦇Arr⦈, ℭ⦇Cod⦈, ℭ⦇Dom⦈]∘"


text‹Components.›

lemma op_dg_components[dg_op_simps]:
  shows "op_dg ℭ⦇Obj⦈ = ℭ⦇Obj⦈"
    and "op_dg ℭ⦇Arr⦈ = ℭ⦇Arr⦈"
    and "op_dg ℭ⦇Dom⦈ = ℭ⦇Cod⦈"
    and "op_dg ℭ⦇Cod⦈ = ℭ⦇Dom⦈"
  unfolding op_dg_def dg_field_simps by (auto simp: nat_omega_simps)

lemma op_dg_component_intros[dg_op_intros]:
  shows "a ∈∘ ℭ⦇Obj⦈ ⟹ a ∈∘ op_dg ℭ⦇Obj⦈"
    and "f ∈∘ ℭ⦇Arr⦈ ⟹ f ∈∘ op_dg ℭ⦇Arr⦈"
  unfolding dg_op_simps by simp_all


text‹Elementary properties.›

lemma op_dg_is_arr[dg_op_simps]: "f : b ↦⇘op_dg ℭ⇙ a ⟷ f : a ↦⇘ℭ⇙ b"
  unfolding dg_op_simps is_arr_def by auto

lemmas [dg_op_intros] = op_dg_is_arr[THEN iffD2]

lemma op_dg_Hom[dg_op_simps]: "Hom (op_dg ℭ) a b = Hom ℭ b a"
  unfolding dg_op_simps by simp


subsubsection‹Further properties›

lemma (in digraph) digraph_op[dg_op_intros]: "digraph α (op_dg ℭ)"
proof(intro digraphI, unfold op_dg_components dg_op_simps)
  show "vfsequence (op_dg ℭ)" unfolding op_dg_def by simp
  show "vcard (op_dg ℭ) = 4ℕ"
    unfolding op_dg_def by (simp add: nat_omega_simps)
  fix A B assume "A ⊆∘ ℭ⦇Obj⦈" "B ⊆∘ ℭ⦇Obj⦈" "A ∈∘ Vset α" "B ∈∘ Vset α"
  then show "⋃∘((λa∈∘A. ⋃∘((λaa∈∘B. Hom ℭ aa a) `∘ B)) `∘ A) ∈∘ Vset α"
    by (subst vifunion_vifunion_flip) (intro dg_Hom_vifunion_in_Vset)
qed (auto simp: dg_Dom_vrange dg_Cod_vrange dg_Obj_vsubset_Vset dg_cs_simps)

lemmas digraph_op[dg_op_intros] = digraph.digraph_op

lemma (in digraph) dg_op_dg_op_dg[dg_op_simps]: "op_dg (op_dg ℭ) = ℭ"
  by (rule dg_eqI[of α], unfold dg_op_simps)
    (simp_all add: digraph_axioms digraph.digraph_op digraph_op)

lemmas dg_op_dg_op_dg[dg_op_simps] = digraph.dg_op_dg_op_dg

lemma eq_op_dg_iff[dg_op_simps]: 
  assumes "digraph α 𝔄" and "digraph α 𝔅"
  shows "op_dg 𝔄 = op_dg 𝔅 ⟷ 𝔄 = 𝔅"
proof
  interpret 𝔄: digraph α 𝔄 by (rule assms(1))
  interpret 𝔅: digraph α 𝔅 by (rule assms(2))
  assume prems: "op_dg 𝔄 = op_dg 𝔅"
  show "𝔄 = 𝔅"
  proof(rule dg_eqI[of α])
    from prems show 
      "𝔄⦇Obj⦈ = 𝔅⦇Obj⦈" "𝔄⦇Arr⦈ = 𝔅⦇Arr⦈" "𝔄⦇Dom⦈ = 𝔅⦇Dom⦈" "𝔄⦇Cod⦈ = 𝔅⦇Cod⦈"
      by (metis prems 𝔄.dg_op_dg_op_dg 𝔅.dg_op_dg_op_dg)+
  qed (simp_all add: assms)
qed auto

text‹\newpage›

end