Theory AxiomaticCategoryTheory

(*<*)
theory AxiomaticCategoryTheory imports Main

abbrevs
 f_neg="¬" and f_or="∨" and f_and="∧" and f_impl="→" and f_imp="←" and mequ="↔" and f_all="∀"
 and f_exi="∃" and f_all2="(∀x.)" and f_exi2="(∃x.)" and f_kleeneeq="≅" and f_primeq="≃" and
 f_comp2="(⋅)" and f_comp="⋅"

begin
 (*Begin: some useful parameter settings*)
  nitpick_params[user_axioms, show_all, format = 2, expect = genuine]
 (*End: some useful parameter settings*)
(*>*)

section‹Introduction›

  text‹This document provides a concise overview on the core results of our previous
       work \cite{C67,R58,C57} on the exploration of axiom systems for category theory.
       Extending the previous studies we
       include one further axiomatic theory in our experiments. This additional
       theory has been suggested by Mac Lane~\cite{MacLane48} in
       1948. We show that the axioms proposed by Mac Lane are equivalent to the ones studied
       in~\cite{R58}, which includes an axioms set suggested by Scott~\cite{Scott79}
       in the 1970s and another axioms set proposed by Freyd and Scedrov~\cite{FreydScedrov90} in 1990,
       which we slightly modified in~\cite{R58} to remedy a minor technical issue.

      The explanations given below are minimal, for more details we refer to the referenced
      papers, in particular, to~\cite{R58}.›


section‹Embedding of Free Logic in HOL›

text‹We introduce a shallow semantical embedding of free logic \cite{R58} in Isabelle/HOL.
     Definite description is omitted, since it is not needed in the studies below and also
     since the definition provided in \cite{C57} introduces the here undesired commitment
     that at least one non-existing element of type $i$ is a priori given. We here want to
     consider this an optional condition.›

 typedecl i ― ‹Type for individuals›
 consts fExistence:: "i⇒bool" (‹E›) ― ‹Existence/definedness predicate in free logic›

 abbreviation fNot   (‹¬›)               where "¬φ ≡ ¬φ"
 abbreviation fImpl  (infixr ‹→› 13)  where "φ → ψ ≡ φ ⟶ ψ"
 abbreviation fId     (infixr ‹=› 25)   where "l = r ≡ l = r"
 abbreviation fAll    (‹∀›)               where "∀Φ ≡ ∀x. E x ⟶ Φ x"
 abbreviation fAllBi (binder ‹∀› [8]9) where "∀x. φ x ≡ ∀φ"
 abbreviation fOr    (infixr ‹∨› 21)     where "φ ∨ ψ ≡ (¬φ) → ψ"
 abbreviation fAnd   (infixr ‹∧› 22)     where "φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ)"
 abbreviation fImpli (infixr ‹←› 13)    where "φ ← ψ ≡ ψ → φ"
 abbreviation fEquiv (infixr ‹↔› 15)    where "φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ)"
 abbreviation fEx     (‹∃›)                 where "∃Φ ≡ ¬(∀(λy. ¬(Φ y)))"
 abbreviation fExiBi (binder ‹∃› [8]9)  where "∃x. φ x ≡ ∃φ"



section‹Some Basic Notions in Category Theory›

text ‹Morphisms in the category are modeled as objects of type $i$.
We introduce three partial functions,
$dom$ (domain), $cod$ (codomain), and morphism composition ($\cdot$).

For composition we assume set-theoretical composition here (i.e., functional
composition from right to left). \label{IDMcL}›

 consts
  domain:: "i⇒i" (‹dom _› [108] 109)
  codomain:: "i⇒i" (‹cod _› [110] 111)
  composition:: "i⇒i⇒i" (infix ‹⋅› 110)

 ― ‹Kleene Equality›
 abbreviation KlEq (infixr ‹≅› 56) where "x ≅ y ≡ (E x ∨ E y) → x = y"
 ― ‹Existing Identity›
 abbreviation ExId (infixr ‹≃› 56) where "x ≃ y ≡ (E x ∧ E y ∧ x = y)"

 ― ‹Identity-morphism: see also p.~4. of \cite{FreydScedrov90}.›
 abbreviation "ID i ≡ (∀x. E(i⋅x) → i⋅x ≅ x) ∧ (∀x. E(x⋅i) → x⋅i ≅ x)"
 ― ‹Identity-morphism: Mac Lane's definition, the same as ID except for notion of equality.›
 abbreviation "IDMcL ρ ≡ (∀α. E(ρ⋅α) → ρ⋅α = α) ∧ (∀β. E(β⋅ρ) → β⋅ρ = β)"

 ― ‹The two notions of identity-morphisms are obviously equivalent.›
 lemma IDPredicates: "ID ≡ IDMcL" by auto


section‹The Axioms Sets studied by Benzm\"uller and Scott \cite{R58}›

subsection‹AxiomsSet1›

 text‹AxiomsSet1 generalizes the notion of a monoid by introducing a partial, strict binary
      composition operation ``$\cdot$''. The existence of left and right identity elements is
      addressed in axioms @{term "Ci"} and @{term "Di"}. The notions of $dom$ (domain) and
      $cod$ (codomain)
      abstract from their common meaning in the context of sets. In category theory we
     work with just a single type of objects (the type $i$ in our setting) and therefore
     identity morphisms are employed to suitably characterize their
     meanings.›

 locale AxiomsSet1 =
  assumes
   Si: "E(x⋅y) → (E x ∧ E y)" and
   Ei: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" and
   Ai: "x⋅(y⋅z) ≅ (x⋅y)⋅z" and
   Ci: "∀y.∃i. ID i ∧ i⋅y ≅ y" and
   Di: "∀x.∃j. ID j ∧ x⋅j ≅ x"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›

   lemma EiImpl: "E(x⋅y) → (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" by (metis Ai Ci Si)
   ― ‹Uniqueness of i and j in the latter two axioms.›
   lemma UCi: "∀y.∃i. ID i ∧ i⋅y ≅ y ∧ (∀j.(ID j ∧ j⋅y ≅ y) → i ≅ j)" by (smt (verit) Ai Ci Si)
   lemma UDi: "∀x.∃j. ID j ∧ x⋅j ≅ x ∧ (∀i.(ID i ∧ x⋅i ≅ x) → j ≅ i)" by (smt (verit) Ai Di Si)
   ― ‹But i and j need not to equal.›
   lemma "(∃C D. (∀y. ID (C y) ∧ (C y)⋅y ≅ y) ∧ (∀x. ID (D x) ∧ x⋅(D x) ≅ x) ∧ ¬(D = C))"
     nitpick [satisfy] oops ― ‹Model found›
   lemma "(∃x. E x) ∧ (∃C D. (∀y. ID(C y) ∧ (C y)⋅y ≅ y) ∧ (∀x. ID(D x) ∧ x⋅(D x) ≅ x) ∧ ¬(D = C))"
     nitpick [satisfy] oops ― ‹Model found›
  end



subsection‹AxiomsSet2›

text‹AxiomsSet2 is developed from AxiomsSet1 by Skolemization of the
     existentially quantified variables $i$ and $j$ in axioms $C_i$ and
     $D_i$. We can argue semantically that every model of AxiomsSet1 has
     such functions. Hence, we get a conservative extension of AxiomsSet1.
     The strictness axiom $S$ is extended, so
     that strictness is now also postulated for the new Skolem functions
     $dom$ and $cod$.›

 locale AxiomsSet2 =
  assumes
   Sii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x) → E x) ∧ (E(cod y) → E y)"  and
   Eii: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" and
   Aii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" and
   Cii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" and
   Dii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›

   lemma EiiImpl: "E(x⋅y) → (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" by (metis Aii Cii Sii)
   lemma domTotal: "E x → E(dom x)" by (metis Dii Sii)
   lemma codTotal: "E x → E(cod x)" by (metis Cii Sii)
  end

 subsubsection‹AxiomsSet2 entails AxiomsSet1›

 context AxiomsSet2
  begin
   lemma Si: "E(x⋅y) → (E x ∧ E y)" using Sii by blast
   lemma Ei: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" using Eii by blast
   lemma Ai: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aii by blast
   lemma Ci: "∀y.∃i. ID i ∧ i⋅y ≅ y" by (metis Cii Sii)
   lemma Di: "∀x.∃j. ID j ∧ x⋅j ≅ x" by (metis Dii Sii)
  end

 subsubsection‹AxiomsSet1 entails AxiomsSet2 (by semantic means)›
 text‹By semantic means (Skolemization).›



 subsection‹AxiomsSet3›

 text‹In AxiomsSet3 the existence  axiom  $E_{ii}$ from AxiomsSet2  is simplified by taking
      advantage of the two new Skolem functions $dom$ and $cod$.

      The left-to-right direction of existence axiom $E_{iii}$ is implied.›

 locale AxiomsSet3 =
  assumes
   Siii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x ) → E x) ∧ (E(cod y) → E y)"  and
   Eiii: "E(x⋅y) ← (dom x ≅ cod y ∧ E(cod y))" and
   Aiii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" and
   Ciii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" and
   Diii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›

   lemma EiiiImpl: "E(x⋅y) → (dom x ≅ cod y ∧ E(cod y))" by (metis (full_types) Aiii Ciii Diii Siii)
  end


 subsubsection‹AxiomsSet3 entails AxiomsSet2›

 context AxiomsSet3
  begin
   lemma Sii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x ) → E x) ∧ (E(cod y) → E y)" using Siii by blast
   lemma Eii: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" by (metis Aiii Ciii Diii Eiii Siii)
   lemma Aii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aiii by blast
   lemma Cii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" using Ciii by auto
   lemma Dii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)" using Diii by auto
  end


 subsubsection‹AxiomsSet2 entails AxiomsSet3›

 context AxiomsSet2
  begin
   lemma Siii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x) → E x) ∧ (E(cod y) → E y)" using Sii by blast
   lemma Eiii: "E(x⋅y) ← (dom x ≅ cod y ∧ E(cod y))" by (metis Cii Dii Eii Sii)
   lemma Aiii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aii by blast
   lemma Ciii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" using Cii by auto
   lemma Diii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)" using Dii by auto
  end




  subsection‹The Axioms Set AxiomsSet4›

  text‹AxiomsSet4 simplifies the axioms $C_{iii}$ and  $D_{iii}$. However, as it turned
       out, these simplifications also require the existence axiom $E_{iii}$ to be strengthened
       into an equivalence.›

 locale AxiomsSet4 =
  assumes
   Siv: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x) → E x) ∧ (E(cod y) → E y)"  and
   Eiv: "E(x⋅y) ↔ (dom x ≅ cod y ∧ E(cod y))" and
   Aiv: "x⋅(y⋅z) ≅ (x⋅y)⋅z" and
   Civ: "(cod y)⋅y ≅ y" and
   Div: "x⋅(dom x) ≅ x"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end

 subsubsection‹AxiomsSet4 entails AxiomsSet3›

 context AxiomsSet4
  begin
   lemma Siii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x) → E x) ∧ (E(cod y) → E y)" using Siv by blast
   lemma Eiii: "E(x⋅y) ← (dom x ≅ cod y ∧ (E(cod y)))" using Eiv by blast
   lemma Aiii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aiv by blast
   lemma Ciii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" by (metis Civ Div Eiv)
   lemma Diii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)" by (metis Civ Div Eiv)
  end


 subsubsection‹AxiomsSet3 entails AxiomsSet4›

 context AxiomsSet3
  begin
   lemma Siv: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x ) → E x) ∧ (E(cod y) → E y)"  using Siii by blast
   lemma Eiv: "E(x⋅y) ↔ (dom x ≅ cod y ∧ E(cod y))" by (metis (full_types) Aiii Ciii Diii Eiii Siii)
   lemma Aiv: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aiii by blast
   lemma Civ: "(cod y)⋅y ≅ y" using Ciii Siii by blast
   lemma Div: "x⋅(dom x) ≅ x" using Diii Siii by blast
  end




subsection‹AxiomsSet5›

  text‹AxiomsSet5 has been proposed by Scott \cite{Scott79} in the 1970s. This set of
 axioms is equivalent to the axioms set presented by Freyd and Scedrov in their textbook
 ``Categories, Allegories'' \cite{FreydScedrov90} when encoded in free logic, corrected/adapted
 and further simplified, see Section 5.›

 locale AxiomsSet5 =
  assumes
   S1: "E(dom x) → E x" and
   S2: "E(cod y) → E y" and
   S3: "E(x⋅y) ↔ dom x ≃ cod y" and
   S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z" and
   S5: "(cod y)⋅y ≅ y" and
   S6: "x⋅(dom x) ≅ x"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end



 subsubsection‹AxiomsSet5 entails AxiomsSet4›

 context AxiomsSet5
  begin
   lemma Siv: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x ) → E x) ∧ (E(cod y) → E y)" using S1 S2 S3 by blast
   lemma Eiv: "E(x⋅y) ↔ (dom x ≅ cod y ∧ E(cod y))" using S3 by metis
   lemma Aiv: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using S4 by blast
   lemma Civ: "(cod y)⋅y ≅ y" using S5 by blast
   lemma Div: "x⋅(dom x) ≅ x" using S6 by blast
  end


 subsubsection‹AxiomsSet4 entails AxiomsSet5›

 context AxiomsSet4
  begin
   lemma S1: "E(dom x) → E x" using Siv by blast
   lemma S2: "E(cod y) → E y" using Siv by blast
   lemma S3: "E(x⋅y) ↔ dom x ≃ cod y" using Eiv by metis
   lemma S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using Aiv by blast
   lemma S5: "(cod y)⋅y ≅ y" using Civ by blast
   lemma S6: "x⋅(dom x) ≅ x" using Div by blast
  end




section‹The Axioms Sets by Freyd and Scedrov \cite{FreydScedrov90}›

subsection‹AxiomsSet6›
text‹The axioms by Freyd and Scedrov  \cite{FreydScedrov90} in our notation, when being
     corrected (cf. the modification in axiom A1).

     Freyd and Scedrov employ a different notation for $dom\ x$ and $cod\ 
     x$. They denote these operations by $\Box x$
     and $x\Box$. Moreover, they employ diagrammatic composition instead of the set-theoretic
     definition (functional composition from right to left) used so
     far.
     We leave it to the reader to verify that their axioms corresponds to the axioms presented
     here modulo an appropriate conversion of notation.›

 locale AxiomsSet6 =
  assumes
    A1: "E(x⋅y) ↔ dom x ≃ cod y" and
   A2a: "cod(dom x) ≅ dom x" and
   A2b: "dom(cod y) ≅ cod y" and
   A3a: "x⋅(dom x) ≅ x" and
   A3b: "(cod y)⋅y ≅ y" and
   A4a: "dom(x⋅y) ≅ dom((dom x)⋅y)" and
   A4b: "cod(x⋅y) ≅ cod(x⋅(cod y))" and
    A5: "x⋅(y⋅z) ≅ (x⋅y)⋅z"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
end


 subsubsection‹AxiomsSet6 entails AxiomsSet5›

 context AxiomsSet6
  begin
   lemma S1: "E(dom x) → E x" by (metis A1 A2a A3a)
   lemma S2: "E(cod y) → E y" using A1 A2b A3b by metis
   lemma S3: "E(x⋅y) ↔ dom x ≃ cod y" by (metis A1)
   lemma S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using A5 by blast
   lemma S5: "(cod y)⋅y ≅ y" using A3b by blast
   lemma S6: "x⋅(dom x) ≅ x" using A3a by blast

   lemma A4aRedundant: "dom(x⋅y) ≅ dom((dom x)⋅y)" using A1 A2a A3a A5 by metis
   lemma A4bRedundant: "cod(x⋅y) ≅ cod(x⋅(cod y))" using A1 A2b A3b A5 by (smt (verit))
   lemma A2aRedundant: "cod(dom x) ≅ dom x" using A1 A3a A3b A4a A4b by (smt (verit))
   lemma A2bRedundant: "dom(cod y) ≅ cod y" using  A1 A3a A3b A4a A4b by (smt (verit))
  end


 subsubsection‹AxiomsSet5 entails AxiomsSet6›

 context AxiomsSet5
  begin
   lemma A1: "E(x⋅y) ↔ dom x ≃ cod y" using S3 by blast
   lemma A2: "cod(dom x) ≅ dom x" by (metis S1 S2 S3 S6)
   lemma A2b: "dom(cod y) ≅ cod y" using S1 S2 S3 S5 by metis
   lemma A3a: "x⋅(dom x) ≅ x" using S6 by auto
   lemma A3b: "(cod y)⋅y ≅ y" using S5 by blast
   lemma A4a: "dom(x⋅y) ≅ dom((dom x)⋅y)" by (metis S1 S3 S4 S5 S6)
   lemma A4b: "cod(x⋅y) ≅ cod(x⋅(cod y))" by (metis (full_types) S2 S3 S4 S5 S6)
   lemma  A5: "x⋅(y⋅z) ≅ (x⋅y)⋅z" using S4 by blast
  end



subsection‹AxiomsSet7 (technically flawed)›
  text‹The axioms by Freyd and Scedrov in our notation, without the suggested correction of
       axiom A1. This axioms set is technically flawed
       when encoded in our given context. It leads to a constricted inconsistency.›


 locale AxiomsSet7 =
  assumes
    A1: "E(x⋅y) ↔ dom x ≅ cod y" and
   A2a: "cod(dom x) ≅ dom x " and
   A2b: "dom(cod y) ≅ cod y" and
   A3a: "x⋅(dom x) ≅ x" and
   A3b: "(cod y)⋅y ≅ y" and
   A4a: "dom(x⋅y) ≅ dom((dom x)⋅y)" and
   A4b: "cod(x⋅y) ≅ cod(x⋅(cod y))" and
    A5: "x⋅(y⋅z) ≅ (x⋅y)⋅z"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   (*
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  --{*No model found*}
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  --{*No model found*}
   *)
   lemma InconsistencyAutomatic: "(∃x. ¬(E x)) → False" by (metis A1 A2a A3a) ― ‹Inconsistency›
   lemma "∀x. E x" using InconsistencyAutomatic by auto

   lemma InconsistencyInteractive:
    assumes NEx: "∃x. ¬(E x)" shows False
    proof -
    obtain a where 1: "¬(E a)" using NEx by auto
    have 2: "a⋅(dom a) ≅ a" using A3a by blast
    have 3: "¬(E(a⋅(dom a)))" using 1 2 by metis
    have 4: "E(a⋅(dom a)) ↔ dom a ≅ cod(dom a)" using A1 by blast
    have 5: "cod(dom a) ≅ dom a" using A2a by blast
    have 6: "E(a⋅(dom a)) ↔ dom a ≅ dom a" using 4 5 by auto
    have 7: "E(a⋅(dom a))" using 6 by blast
    then show ?thesis using 7 3 by blast
    qed
  end



subsection‹AxiomsSet7orig (technically flawed)›

text‹The axioms by Freyd and Scedrov in their original notation, without the suggested
     correction of axiom A1.

      We present the constricted inconsistency argument from above once again,
      but this time in the original notation of Freyd and Scedrov.›

 locale AxiomsSet7orig =
  fixes
   source:: "i⇒i" (‹□_› [108] 109) and
   target:: "i⇒i" (‹_□› [110] 111) and
   compositionF:: "i⇒i⇒i" (infix ‹⋅› 110)
  assumes
    A1: "E(x⋅y) ↔ (x□ ≅ □y)" and
   A2a: "((□x)□) ≅ □x" and
   A2b: "□(x□) ≅ □x" and
   A3a: "(□x)⋅x ≅ x" and
   A3b: "x⋅(x□) ≅ x" and
   A4a: "□(x⋅y) ≅ □(x⋅(□y))" and
   A4b: "(x⋅y)□ ≅ ((x□)⋅y)□" and
    A5: "x⋅(y⋅z) ≅ (x⋅y)⋅z"
  begin
   lemma True nitpick [satisfy] oops ― ‹Consistency›
   (*
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  --{*No model found*}
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  --{*No model found*}
    *)
   lemma InconsistencyAutomatic: "(∃x. ¬(E x)) → False" by (metis A1 A2a A3a) ― ‹Inconsistency›
   lemma "∀x. E x" using InconsistencyAutomatic by auto

   lemma InconsistencyInteractive:
    assumes NEx: "∃x. ¬(E x)" shows False
    proof -
    obtain a where 1: "¬(E a)" using assms by auto
    have 2: "(□a)⋅a ≅ a" using A3a by blast
    have 3: "¬(E((□a)⋅a))" using 1 2 by metis
    have 4: "E((□a)⋅a) ↔ (□a)□ ≅ □a" using A1 by blast
    have 5: "(□a)□ ≅ □a" using A2a by blast
    have 6: "E((□a)⋅a)" using 4 5 by blast
    then show ?thesis using 6 3 by blast
    qed
  end


subsection‹AxiomsSet8 (algebraic reading, still technically flawed)›

 text‹The axioms by Freyd and Scedrov in our notation again, but this time we adopt
      an algebraic reading of the free variables, meaning that they range over existing
      morphisms only.›

 locale AxiomsSet8 =
  assumes
    B1: "∀x.∀y. E(x⋅y) ↔ dom x ≅ cod y" and
   B2a: "∀x. cod(dom x) ≅ dom x " and
   B2b: "∀y. dom(cod y) ≅ cod y" and
   B3a: "∀x. x⋅(dom x) ≅ x" and
   B3b: "∀y. (cod y)⋅y ≅ y" and
   B4a: "∀x.∀y. dom(x⋅y) ≅ dom((dom x)⋅y)" and
   B4b: "∀x.∀y. cod(x⋅y) ≅ cod(x⋅(cod y))" and
    B5: "∀x.∀y.∀z. x⋅(y⋅z) ≅ (x⋅y)⋅z"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end


 text‹None of the axioms in AxiomsSet5 are implied.›

 context AxiomsSet8
  begin
   lemma S1: "E(dom x) → E x" nitpick oops ― ‹Nitpick finds a countermodel›
   lemma S2: "E(cod y) → E y" nitpick oops ― ‹Nitpick finds a countermodel›
   lemma S3: "E(x⋅y) ↔ dom x ≃ cod y" nitpick oops ― ‹Nitpick finds a countermodel›
   lemma S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z" nitpick oops ― ‹Nitpick finds a countermodel›
   lemma S5: "(cod y)⋅y ≅ y"  nitpick oops ― ‹Nitpick finds a countermodel›
   lemma S6: "x⋅(dom x) ≅ x"  nitpick oops ― ‹Nitpick finds a countermodel›
  end


subsection‹AxiomsSet8Strict (algebraic reading)›

 text‹The situation changes when strictness conditions are postulated. Note that in the algebraic
      framework of Freyd and Scedrov such conditions have to be assumed as given in the
      logic, while here we can explicitly encode them as axioms.›

 locale AxiomsSet8Strict = AxiomsSet8 +
  assumes
   B0a: "E(x⋅y) → (E x ∧ E y)" and
   B0b: "E(dom x) → E x" and
   B0c: "E(cod x) → E x"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end


 subsubsection‹AxiomsSet8Strict entails AxiomsSet5›

 context AxiomsSet8Strict
  begin
   lemma S1: "E(dom x) → E x"  using B0b by blast
   lemma S2: "E(cod y) → E y"  using B0c by blast
   lemma S3: "E(x⋅y) ↔ dom x ≃ cod y" by (metis B0a B0b B0c B1 B3a)
   lemma S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z" by (meson B0a B5)
   lemma S5: "(cod y)⋅y ≅ y" using B0a B3b by blast
   lemma S6: "x⋅(dom x) ≅ x" using B0a B3a by blast
  end


 subsubsection‹AxiomsSet5 entails AxiomsSet8Strict›

 context AxiomsSet5
  begin
   lemma B0a: "E(x⋅y) → (E x ∧ E y)" using S1 S2 S3 by blast
   lemma B0b: "E(dom x) → E x" using S1 by blast
   lemma B0c: "E(cod x) → E x" using S2 by blast
   lemma  B1: "∀x.∀y. E(x⋅y) ↔ dom x ≅ cod y" by (metis S3 S5)
   lemma B2a: "∀x. cod(dom x) ≅ dom x" using A2 by blast
   lemma B2b: "∀y. dom(cod y) ≅ cod y" using A2b by blast
   lemma B3a: "∀x. x⋅(dom x) ≅ x" using S6 by blast
   lemma B3b: "∀y. (cod y)⋅y ≅ y" using S5 by blast
   lemma B4a: "∀x.∀y. dom(x⋅y) ≅ dom((dom x)⋅y)" by (metis S1 S3 S4 S6)
   lemma B4b: "∀x.∀y. cod(x⋅y) ≅ cod(x⋅(cod y))" by (metis S1 S2 S3 S4 S5)
   lemma  B5: "∀x.∀y.∀z. x⋅(y⋅z) ≅ (x⋅y)⋅z" using S4 by blast
  end


  subsubsection‹AxiomsSet8Strict is Redundant›

  text‹AxiomsSet8Strict is redundant: either the B2-axioms can be omitted or the B4-axioms.›

 context AxiomsSet8Strict
  begin
   lemma B2aRedundant: "∀x. cod(dom x) ≅ dom x " by (metis B0a B1 B3a)
   lemma B2bRedundant: "∀y. dom(cod y) ≅ cod y" by (metis B0a B1 B3b)
   lemma B4aRedundant: "∀x.∀y. dom(x⋅y) ≅ dom((dom x)⋅y)" by (metis B0a B0b B1 B3a B5)
   lemma B4bRedundant: "∀x.∀y. cod(x⋅y) ≅ cod(x⋅(cod y))" by (metis B0a B0c B1 B3b B5)
  end





  section‹The Axioms Sets of Mac Lane \cite{MacLane48}›

  text‹We analyse the axioms set suggested by Mac Lane~\cite{MacLane48} already in 1948.
      As for the theory by
       Freyd and Scedrov above, which was developed much later, we need to assume
       strictness of composition to show equivalence to our previous axiom sets.
       Note that his complicated conditions on existence of compositions proved to be
       unnecessary, as we show. It shows it is hard to think about partial operations.›


 locale AxiomsSetMcL =
  assumes
   C0 : "E(x⋅y) → (E x ∧ E y)" and
   C1 : "∀γ β α. (E(γ⋅β) ∧ E((γ⋅β)⋅α)) → E(β⋅α)" and
   C1': "∀γ β α. (E(β⋅α) ∧ E(γ⋅(β⋅α))) → E(γ⋅β)" and
   C2 : "∀γ β α. (E(γ⋅β) ∧ E(β⋅α)) → (E((γ⋅β)⋅α) ∧ E(γ⋅(β⋅α)) ∧ ((γ⋅β)⋅α) = (γ⋅(β⋅α)))" and
   C3 : "∀γ. ∃eD. IDMcL(eD) ∧ E(γ⋅eD)" and
   C4 : "∀γ. ∃eR. IDMcL(eR) ∧ E(eR⋅γ)"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end

  text‹Remember that IDMcL  was defined on p.~\pageref{IDMcL} and proved
       equivalent to ID.›


 subsection‹AxiomsSetMcL entails AxiomsSet1›

 context AxiomsSetMcL
  begin
   lemma Si: "E(x⋅y) → (E x ∧ E y)"  using C0 by blast
   lemma Ei: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" by (metis C2)
   lemma Ai: "x⋅(y⋅z) ≅ (x⋅y)⋅z"       by (metis C1 C1' C2 C0)
   lemma Ci: "∀y.∃i. ID i ∧ i⋅y ≅ y" using C4 by fastforce
   lemma Di: "∀x.∃j. ID j ∧ x⋅j ≅ x" using C3 by fastforce
  end


 subsection‹AxiomsSet1 entails AxiomsSetMcL›

 context AxiomsSet1
  begin
   lemma C0 : "E(x⋅y) → (E x ∧ E y)" using Si by blast
   lemma C1 : "∀γ β α. (E(γ⋅β) ∧ E((γ⋅β)⋅α)) → E(β⋅α)" by (metis Ai Si)
   lemma C1': "∀γ β α. (E(β⋅α) ∧ E(γ⋅(β⋅α))) → E(γ⋅β)" by (metis Ai Si)
   lemma C2 : "∀γ β α. (E(γ⋅β) ∧ E(β⋅α)) → (E((γ⋅β)⋅α) ∧ E(γ⋅(β⋅α)) ∧ ((γ⋅β)⋅α) = (γ⋅(β⋅α)))" by (smt (verit) Ai Ci Ei Si)
   lemma C3 : "∀γ. ∃eD. IDMcL(eD) ∧ E(γ⋅eD)" using Di by force
   lemma C4 : "∀γ. ∃eR. IDMcL(eR) ∧ E(eR⋅γ)" using Ci by force
  end



 subsection‹Skolemization of the Axioms of Mac Lane›

 text‹Mac Lane employs diagrammatic composition instead of the set-theoretic
     definition as used in our axiom sets. As we have seen above,
      this is not a problem as long as composition is the only primitive.
      But when adding the Skolem terms $dom$ and $cod$ care must be taken and we should
      actually transform all axioms into a common form. Below we address this (in a minimal way) by
      using $dom$ in axiom @{term "C3s"} and $cod$ in axiom @{term "C4s"}, which is opposite of
      what Mac Lane proposed. For this axioms set we then show  equivalence to AxiomsSet1/2/5.›

 locale SkolemizedAxiomsSetMcL =
  assumes
   C0s : "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x) → E x) ∧ (E(cod y) → E y)" and
   C1s : "∀γ β α. (E(γ⋅β) ∧ E((γ⋅β)⋅α)) → E(β⋅α)" and
   C1's: "∀γ β α. (E(β⋅α) ∧ E(γ⋅(β⋅α))) → E(γ⋅β)" and
   C2s : "∀γ β α. (E(γ⋅β) ∧ E(β⋅α)) → (E((γ⋅β)⋅α) ∧ E(γ⋅(β⋅α)) ∧ ((γ⋅β)⋅α) = (γ⋅(β⋅α)))" and
   C3s : "∀γ. IDMcL(dom γ) ∧ E(γ⋅(dom γ))" and
   C4s : "∀γ. IDMcL(cod γ) ∧ E((cod γ)⋅γ)"
  begin
   lemma True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "∃x. ¬(E x)" shows True nitpick [satisfy] oops  ― ‹Consistency›
   lemma assumes "(∃x. ¬(E x)) ∧ (∃x. (E x))" shows True nitpick [satisfy] oops  ― ‹Consistency›
  end


 subsection‹SkolemizedAxiomsSetMcL entails AxiomsSetMcL and AxiomsSet1-5›

 context SkolemizedAxiomsSetMcL
  begin
   lemma C0 : "E(x⋅y) → (E x ∧ E y)" using C0s by blast
   lemma C1 : "∀γ β α. (E(γ⋅β) ∧ E((γ⋅β)⋅α)) → E(β⋅α)" using C1s by blast
   lemma C1': "∀γ β α. (E(β⋅α) ∧ E(γ⋅(β⋅α))) → E(γ⋅β)" using C1's by blast
   lemma C2 : "∀γ β α. (E(γ⋅β) ∧ E(β⋅α)) → (E((γ⋅β)⋅α) ∧ E(γ⋅(β⋅α)) ∧ ((γ⋅β)⋅α) = (γ⋅(β⋅α)))" using C2s by blast
   lemma C3 : "∀γ. ∃eD. IDMcL(eD) ∧ E(γ⋅eD)" by (metis C0s C3s)
   lemma C4 : "∀γ. ∃eR. IDMcL(eR) ∧ E(eR⋅γ)" by (metis C0s C4s)

   lemma Si: "E(x⋅y) → (E x ∧ E y)"   using C0s by blast
   lemma Ei: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))"  by (metis C2s)
   lemma Ai: "x⋅(y⋅z) ≅ (x⋅y)⋅z"        by (metis C1s C1's C2s C0s)
   lemma Ci: "∀y.∃i. ID i ∧ i⋅y ≅ y"  by (metis C0s C4s)
   lemma Di: "∀x.∃j. ID j ∧ x⋅j ≅ x"  by (metis C0s C3s)

   lemma Sii: "(E(x⋅y) → (E x ∧ E y)) ∧ (E(dom x ) → E x) ∧ (E(cod y) → E y)" using C0s by blast
   lemma Eii: "E(x⋅y) ← (E x ∧ E y ∧ (∃z. z⋅z ≅ z ∧ x⋅z ≅ x ∧ z⋅y ≅ y))" by (metis C2s)
   lemma Aii: "x⋅(y⋅z) ≅ (x⋅y)⋅z" by (metis C1s C1's C2s C0s)
   lemma Cii: "E y → (ID(cod y) ∧ (cod y)⋅y ≅ y)" using C4s by auto
   lemma Dii: "E x → (ID(dom x) ∧ x⋅(dom x) ≅ x)" using C3s by auto

   ― ‹AxiomsSets3/4 are omitted here; we already know they are equivalent.›

   lemma S1: "E(dom x) → E x"         using C0s by blast
   lemma S2: "E(cod y) → E y"         using C0s by blast
   lemma S3: "E(x⋅y) ↔ dom x ≃ cod y" by (metis (full_types) C0s C1s C1's C2s C3s C4s)
   lemma S4: "x⋅(y⋅z) ≅ (x⋅y)⋅z"        by (metis C0s C1s C1's C2s)
   lemma S5: "(cod y)⋅y ≅ y"           using C0s C4s by blast
   lemma S6: "x⋅(dom x) ≅ x"           using C0s C3s by blast
  end



(*<*)
end
(*>*)