Theory MonadicEquationalTheory

(*
Author: Alexander Katovsky
*)

section "Monadic Equational Theory"

theory MonadicEquationalTheory
imports Category Universe
begin

record ('t,'f) Signature = 
  BaseTypes :: "'t set" (‹Tyı›)
  BaseFunctions :: "'f set" (‹Fnı›)
  SigDom :: "'f ⇒ 't" (‹sDomı›)
  SigCod :: "'f ⇒ 't" (‹sCodı›)

locale Signature = 
  fixes S :: "('t,'f) Signature" (structure)
  assumes Domt: "f ∈ Fn ⟹ sDom f ∈ Ty"
  and     Codt: "f ∈ Fn ⟹ sCod f ∈ Ty"

definition funsignature_abbrev (‹_ ∈ Sig _ : _ → _› ) where
  "f ∈ Sig S : A → B ≡ f ∈ (BaseFunctions S) ∧ A ∈ (BaseTypes S) ∧ B ∈ (BaseTypes S) ∧ 
                        (SigDom S f) = A ∧ (SigCod S f) = B ∧ Signature S"

lemma funsignature_abbrevE[elim]: 
"⟦f ∈ Sig S : A → B ; ⟦f ∈ (BaseFunctions S) ; A ∈ (BaseTypes S) ; B ∈ (BaseTypes S) ; 
                        (SigDom S f) = A ; (SigCod S f) = B ; Signature S⟧ ⟹ R⟧ ⟹ R"
by (simp add: funsignature_abbrev_def)

datatype ('t,'f) Expression = ExprVar (‹Vx›) | ExprApp 'f "('t,'f) Expression" (‹_ E@ _›)
datatype ('t,'f) Language = Type 't (‹⊢ _ Type›) | Term 't "('t,'f) Expression" 't (‹Vx : _ ⊢ _ : _›) | 
                            Equation 't "('t,'f) Expression" "('t,'f) Expression" 't (‹Vx : _ ⊢ _≡_ : _›)

inductive
  WellDefined :: "('t,'f) Signature ⇒ ('t,'f) Language ⇒ bool" (‹Sig _ ▹ _›) where
    WellDefinedTy: "A ∈ BaseTypes S ⟹ Sig S ▹ ⊢ A Type"
  | WellDefinedVar: "Sig S ▹ ⊢ A Type ⟹ Sig S ▹ (Vx : A  ⊢ Vx : A)" 
  | WellDefinedFn: "⟦Sig S ▹ (Vx : A  ⊢ e : B)  ; f ∈ Sig S : B → C⟧ ⟹ Sig S ▹ (Vx : A  ⊢ (f E@ e) : C)"
  | WellDefinedEq: "⟦Sig S ▹ (Vx : A  ⊢ e1 : B) ; Sig S ▹ (Vx : A  ⊢ e2 : B)⟧ ⟹ Sig S ▹ (Vx : A ⊢ e1 ≡ e2 : B)"

lemmas WellDefined.intros [intro]
inductive_cases WellDefinedTyE [elim!]: "Sig S ▹ ⊢ A Type"
inductive_cases WellDefinedVarE [elim!]: "Sig S ▹ (Vx : A  ⊢ Vx : A)"
inductive_cases WellDefinedFnE [elim!]: "Sig S ▹ (Vx : A  ⊢ (f E@ e) : C)"
inductive_cases WellDefinedEqE [elim!]: "Sig S ▹ (Vx : A ⊢ e1 ≡ e2 : B)"

lemma SigId: "Sig S ▹ (Vx : A  ⊢ Vx : B) ⟹ A = B"
apply(rule WellDefined.cases)
by simp+

lemma SigTyId: "Sig S ▹ (Vx : A  ⊢ Vx : A) ⟹ A ∈ BaseTypes S"
apply(rule WellDefined.cases)
by auto

lemma (in Signature) SigTy: "⋀ B . Sig S ▹ (Vx : A  ⊢ e : B) ⟹ (A ∈ BaseTypes S ∧ B ∈ BaseTypes S)"
proof(induct e)
  {
    fix B assume a: "Sig S ▹ Vx : A ⊢ Vx : B"
    have "A = B" using a SigId[of S] by simp
    thus "A ∈ Ty ∧ B ∈ Ty" using a by auto
  }
  {
    fix B f e assume ih: "⋀B'. Sig S ▹ (Vx : A ⊢ e : B') ⟹ A ∈ Ty ∧ B' ∈ Ty"
    and a: "Sig S ▹ (Vx : A ⊢ (f E@ e) : B)"
    from a obtain B' where f: "f ∈ Sig S : B' → B" and "Sig S ▹ (Vx : A ⊢ e : B')" by auto
    hence "A ∈ Ty" using ih by auto
    moreover have "B ∈ Ty" using f by (auto simp add: funsignature_abbrev_def Codt)
    ultimately show "A ∈ Ty ∧ B ∈ Ty" by simp
  }
qed

(*An interpretation is an object, a morphism or a boolean*)
datatype ('o,'m) IType = IObj 'o | IMor 'm | IBool bool

record ('t,'f,'o,'m) Interpretation = 
  ISignature :: "('t,'f) Signature" (‹iSı›)
  ICategory  :: "('o,'m) Category"  (‹iCı›)
  ITypes     :: "'t ⇒ 'o" (‹Ty⟦_⟧ı›)
  IFunctions :: "'f ⇒ 'm" (‹Fn⟦_⟧ı›)

locale Interpretation = 
  fixes I :: "('t,'f,'o,'m) Interpretation" (structure)
  assumes ICat: "Category  iC"
  and     ISig: "Signature iS" 
  and     It  : "A ∈ BaseTypes iS ⟹ Ty⟦A⟧ ∈ Obj iC"
  and     If  : "(f ∈ Sig iS : A → B) ⟹ Fn⟦f⟧ maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧"

inductive Interp  (‹L⟦_⟧ı → _›) where
    InterpTy: "Sig iS⇘I⇙ ▹ ⊢ A Type ⟹ 
                       L⟦⊢ A Type⟧⇘I⇙ → (IObj Ty⟦A⟧⇘I⇙)"
  | InterpVar: "L⟦⊢ A Type⟧⇘I⇙ → (IObj c) ⟹ 
                       L⟦Vx : A  ⊢ Vx : A⟧⇘I⇙ → (IMor (Id iC⇘I⇙ c))" 
  | InterpFn: "⟦Sig iS⇘I⇙ ▹ Vx : A  ⊢ e : B ; 
               f ∈ Sig iS⇘I⇙ : B → C ; 
               L⟦Vx : A  ⊢ e : B⟧⇘I⇙ → (IMor g)⟧ ⟹ 
               L⟦Vx : A  ⊢ (f E@ e) : C⟧⇘I⇙ → (IMor (g ;;⇘ICategory I⇙ Fn⟦f⟧⇘I⇙))"
  | InterpEq: "⟦L⟦Vx : A  ⊢ e1 : B⟧⇘I⇙ → (IMor g1) ; 
                L⟦Vx : A  ⊢ e2 : B⟧⇘I⇙ → (IMor g2)⟧ ⟹ 
                L⟦Vx : A  ⊢ e1 ≡ e2 : B⟧⇘I⇙ → (IBool (g1 = g2))"

lemmas  Interp.intros [intro]
inductive_cases  InterpTyE [elim!]: "L⟦⊢ A Type⟧⇘I⇙ → i"
inductive_cases  InterpVarE [elim!]: "L⟦Vx : A  ⊢ Vx : A⟧⇘I⇙ → i"
inductive_cases  InterpFnE [elim!]: "L⟦Vx : A  ⊢ (f E@ e) : C⟧⇘I⇙ → i"
inductive_cases  InterpEqE [elim!]: "L⟦Vx : A  ⊢ e1 ≡ e2 : B⟧⇘I⇙ → i"

lemma (in Interpretation) InterpEqEq[intro]: 
  "⟦L⟦Vx : A  ⊢ e1 : B⟧ → (IMor g) ; L⟦Vx : A  ⊢ e2 : B⟧ → (IMor g)⟧ ⟹ L⟦Vx : A  ⊢ e1 ≡ e2 : B⟧ → (IBool True)"
proof-
  assume a: "L⟦Vx : A  ⊢ e1 : B⟧ → (IMor g)" and b: "L⟦Vx : A  ⊢ e2 : B⟧ → (IMor g)"
  thus ?thesis using InterpEq[of I A e1 B g e2 g] by simp
qed

lemma (in Interpretation) InterpExprWellDefined:
"L⟦Vx : A ⊢ e : B⟧ → i ⟹ Sig iS ▹ Vx : A  ⊢ e : B"
apply (rule Interp.cases)
by auto

lemma (in Interpretation) WellDefined: "L⟦φ⟧ → i ⟹ Sig iS ▹ φ"
apply(rule Interp.cases)
by (auto simp add: InterpExprWellDefined)

lemma (in Interpretation) Bool: "L⟦φ⟧ → (IBool i) ⟹ ∃ A B e d . φ = (Vx : A ⊢ e ≡ d : B)"
apply(rule Interp.cases)
by auto

lemma (in Interpretation) FunctionalExpr:
"⋀i j A B.⟦L⟦Vx : A ⊢ e : B⟧ → i; L⟦Vx : A ⊢ e : B⟧ → j⟧ ⟹ i = j"
apply (induct e)
apply (rule Interp.cases)
apply auto
apply (auto simp add: funsignature_abbrev_def)
done

lemma (in Interpretation) Functional: "⟦L⟦φ⟧ → i1 ; L⟦φ⟧ → i2⟧ ⟹ i1 = i2"
proof(induct φ)
  {
    fix t show "⟦L⟦⊢ t Type⟧ → i1 ; L⟦⊢ t Type⟧ → i2⟧ ⟹ i1 = i2" by auto
  }
  {
    fix t1 t2 e 
    show "⟦L⟦Vx : t1 ⊢ e : t2⟧ → i1; L⟦Vx : t1 ⊢ e : t2⟧ → i2⟧ ⟹ i1 = i2" by (simp add: FunctionalExpr)
  }
  {
    fix t1 t2 e1 e2 show "⟦L⟦Vx : t1 ⊢ e1 ≡ e2 : t2⟧ → i1; L⟦Vx : t1 ⊢ e1 ≡ e2 : t2⟧ → i2⟧ ⟹ i1 = i2" 
    proof(auto)
      {
        fix f g h assume f1: "L⟦Vx : t1 ⊢ e1 : t2⟧ → (IMor f)" and f2: "L⟦Vx : t1 ⊢ e2 : t2⟧ → (IMor f)"
          and g1: "L⟦Vx : t1 ⊢ e1 : t2⟧ → (IMor g)" and g2: "L⟦Vx : t1 ⊢ e2 : t2⟧ → (IMor h)"
        have "f = g" using f1 g1 FunctionalExpr[of t1 e1 t2 "IMor f" "IMor g"] by simp
        moreover have "f = h" using f2 g2 FunctionalExpr[of t1 e2 t2 "IMor f" "IMor h"] by simp
        ultimately show "g = h" by simp
      }
      moreover 
      {
        fix f g h assume f1: "L⟦Vx : t1 ⊢ e1 : t2⟧ → (IMor f)" and f2: "L⟦Vx : t1 ⊢ e2 : t2⟧ → (IMor g)"
          and g1: "L⟦Vx : t1 ⊢ e1 : t2⟧ → (IMor h)" and g2: "L⟦Vx : t1 ⊢ e2 : t2⟧ → (IMor h)"
        have "f = h" using f1 g1 FunctionalExpr[of t1 e1 t2 "IMor f" "IMor h"] by simp
        moreover have "g = h" using f2 g2 FunctionalExpr[of t1 e2 t2 "IMor g" "IMor h"] by simp
        ultimately show "f = g" by simp
      }
    qed 
  }
qed

lemma (in Interpretation) MorphismsPreserved:
"⋀ B i . L⟦Vx : A  ⊢ e : B⟧ → i ⟹ ∃ g . i = (IMor g) ∧ (g maps⇘iC ⇙Ty⟦A⟧ to Ty⟦B⟧)"
proof(induct e)
  {
    fix B i assume a: "L⟦Vx : A ⊢ Vx : B⟧ → i" show "∃ g. i = IMor g ∧ g maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧"
    proof(rule exI[where ?x="Id iC Ty⟦A⟧"], rule conjI)
      have sig: "Sig iS ▹ Vx : A  ⊢ Vx : B" using a by (simp add: InterpExprWellDefined) 
      hence aEqb: "A = B" by (simp add: SigId)
      have ty: "A ∈ BaseTypes iS" using aEqb sig SigTyId by simp
      hence "L⟦Vx : A ⊢ Vx : A⟧ → (IMor (Id iC Ty⟦A⟧))" by auto
      thus "i = IMor (Category.Id iC Ty⟦A⟧)" using a aEqb Functional by simp
      show "(Id iC Ty⟦A⟧) maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧" using aEqb ICat It[of A] Category.Cidm[of iC "Ty⟦A⟧"] ty by simp
    qed
  }
  {
    fix f e B i assume a: "⋀ B i . L⟦Vx : A ⊢ e : B⟧ → i ⟹ ∃g. i = IMor g ∧ g maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧"
               and b: "L⟦Vx : A ⊢ f E@ e : B⟧ → i"
    show "∃g. i = IMor g ∧ g maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧" using a b 
    proof-
      from b obtain g B' where g: "(Sig iS ▹ Vx : A ⊢ e : B') ∧ (f ∈ Sig iS : B' → B) ∧ (L⟦Vx : A ⊢ e : B'⟧ → (IMor g))"
        by auto
      from a have gmaps: "g maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B'⟧" using g by auto
      have fmaps: "Fn⟦f⟧ maps⇘iC⇙ Ty⟦B'⟧ to Ty⟦B⟧" using g If by simp
      have "(g ;;⇘iC⇙ Fn⟦f⟧) maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧" using ICat fmaps gmaps Category.Ccompt[of "iC" g] by simp
      moreover have "L⟦Vx : A ⊢ f E@ e : B⟧ → (IMor (g ;;⇘iC⇙ Fn⟦f⟧))" using g by auto
      ultimately show ?thesis using b Functional exI[where ?x = "(g ;;⇘iC⇙ Fn⟦f⟧)"] by simp
    qed
  }
qed

lemma (in Interpretation) Expr2Mor: "L⟦Vx : A  ⊢ e : B⟧ → (IMor g) ⟹ (g maps⇘iC ⇙Ty⟦A⟧ to Ty⟦B⟧)"
proof-
  assume a: "L⟦Vx : A  ⊢ e : B⟧ → (IMor g)"
  from MorphismsPreserved[of A e B "(IMor g)"] obtain g' where "(IMor g) = (IMor g') ∧ (g' maps⇘iC ⇙Ty⟦A⟧ to Ty⟦B⟧)"
    using a by auto
  thus ?thesis by simp
qed

lemma (in Interpretation) WellDefinedExprInterp: "⋀ B . (Sig iS ▹ Vx : A  ⊢ e : B) ⟹ (∃ i . L⟦Vx : A  ⊢ e : B⟧ → i)"
proof(induct e)
  {
    fix B assume sig: "(Sig iS ▹ Vx : A  ⊢ Vx : B)" show "∃i. L⟦Vx : A ⊢ Vx : B⟧ → i"
    proof-
      have aEqb: "A = B" using sig by (simp add: SigId)
      hence ty: "A ∈ BaseTypes iS" using sig SigTyId by simp
      hence "L⟦Vx : A ⊢ Vx : A⟧ → (IMor (Id iC Ty⟦A⟧))" by auto
      thus ?thesis using aEqb by auto
    qed
  }
  {
    fix f e B assume a: "⋀ B . (Sig iS ▹ Vx : A  ⊢ e : B) ⟹ (∃ i . L⟦Vx : A  ⊢ e : B⟧ → i)"
      and b: "(Sig iS ▹ Vx : A  ⊢ f E@ e : B)"
    show "∃ i . L⟦Vx : A  ⊢ f E@ e : B⟧ → i"
    proof-
      from b obtain B' where B': "(Sig iS ▹ (Vx : A  ⊢ e : B')) ∧ (f ∈ Sig iS : B' → B)" by auto
      from B' a obtain i where i: "L⟦Vx : A  ⊢ e : B'⟧ → i" by auto
      from MorphismsPreserved[of A e B' i] i obtain g where g: "i = (IMor g)" by auto
      thus ?thesis using B' i by auto
    qed
  }
qed

lemma (in Interpretation) Sig2Mor: assumes "(Sig iS ▹ Vx : A  ⊢ e : B)" shows "∃ g . L⟦Vx : A  ⊢ e : B⟧ → (IMor g)"
proof-
  from WellDefinedExprInterp[of A e B] assms obtain i where i: "L⟦Vx : A  ⊢ e : B⟧ → i" by auto
  thus ?thesis using MorphismsPreserved[of A e B i] i by auto
qed

record ('t,'f) Axioms = 
  aAxioms :: "('t,'f) Language set" 
  aSignature :: "('t,'f) Signature" (‹aSı›)

locale Axioms = 
  fixes Ax :: "('t,'f) Axioms" (structure)
  assumes AxT: "(aAxioms Ax) ⊆ {(Vx : A ⊢ e1 ≡ e2 : B) | A B e1 e2 . Sig (aSignature Ax) ▹ (Vx : A ⊢ e1 ≡ e2 : B)}"
  assumes AxSig: "Signature (aSignature Ax)"

primrec Subst :: "('t,'f) Expression ⇒ ('t,'f) Expression ⇒ ('t,'f) Expression" (‹sub _ in _› [81,81] 81) where
  "(sub e in Vx) = e" | "sub e in (f E@ d) = (f E@ (sub e in d))"

lemma SubstXinE: "(sub Vx in e) = e"
by(induct e, auto simp add: Subst_def)

lemma SubstAssoc: "sub a in (sub b in c) = sub (sub a in b) in c"
by(induct c, (simp add: Subst_def)+)

lemma SubstWellDefined: "⋀ C . ⟦Sig S ▹ (Vx : A ⊢ e : B); Sig S ▹ (Vx : B ⊢ d : C)⟧
       ⟹ Sig S ▹ (Vx : A ⊢ (sub e in d) : C)"
proof(induct d)
  {
    fix C assume a: "Sig S ▹ Vx : A ⊢ e : B" and b: "Sig S ▹ Vx : B ⊢ Vx : C"
    have BCeq: "B = C" using b SigId[of S] by simp
    thus "Sig S ▹ Vx : A ⊢ sub e in Vx : C" using a by simp
  }
  {
    fix f d C assume ih: "⋀B'. ⟦Sig S ▹ Vx : A ⊢ e : B; Sig S ▹ Vx : B ⊢ d : B'⟧
            ⟹ Sig S ▹ Vx : A ⊢ sub e in d : B'" and a: "Sig S ▹ Vx : A ⊢ e : B" 
    and b: "Sig S ▹ Vx : B ⊢ f E@ d : C"
    from b obtain B' where B': "f ∈ Sig S : B' → C" and d: "Sig S ▹ Vx : B ⊢ d : B'" by auto
    hence "Sig S ▹ Vx : A ⊢ sub e in d : B'" using ih a by simp
    hence "Sig S ▹ Vx : A ⊢ f E@ (sub e in d) : C" using B' by auto
    thus "Sig S ▹ Vx : A ⊢ (sub e in (f E@ d)) : C" by auto
  }
qed

inductive_set (in Axioms) Theory where
  Ax: "A ∈ (aAxioms Ax) ⟹ A ∈ Theory"
| Refl: "Sig (aSignature Ax) ▹ (Vx : A ⊢ e : B) ⟹ (Vx : A ⊢ e ≡ e : B) ∈ Theory"
| Symm: "(Vx : A ⊢ e1 ≡ e2 : B) ∈ Theory ⟹ (Vx : A ⊢ e2 ≡ e1 : B) ∈ Theory" 
| Trans: "⟦(Vx : A ⊢ e1 ≡ e2 : B) ∈ Theory ; (Vx : A ⊢ e2 ≡ e3 : B) ∈ Theory⟧ ⟹
           (Vx : A ⊢ e1 ≡ e3 : B) ∈ Theory"
| Congr: "⟦(Vx : A ⊢ e1 ≡ e2 : B) ∈ Theory ; f ∈ Sig (aSignature Ax) : B → C⟧ ⟹ 
           (Vx : A ⊢ (f E@ e1) ≡ (f E@ e2) : C) ∈ Theory"
| Subst: "⟦Sig (aSignature Ax) ▹ (Vx : A ⊢ e1 : B) ; (Vx : B ⊢ e2 ≡ e3 : C) ∈ Theory⟧ ⟹
           (Vx : A ⊢ (sub e1 in e2) ≡ (sub e1 in e3) : C) ∈ Theory"

lemma (in Axioms) Equiv2WellDefined: "φ ∈ Theory ⟹ Sig aS ▹ φ"
proof(rule Theory.induct,auto simp add: SubstWellDefined)
  {
    fix φ assume ax: "φ ∈ aAxioms Ax"
    from AxT obtain A e1 e2 B where "Sig aS ▹ Vx : A ⊢ e1 ≡ e2 : B" and "φ = Vx : A ⊢ e1 ≡ e2 : B" using ax by blast
    thus "Sig aS ▹ φ" by simp    
  }
qed

lemma (in Axioms) Subst':
  "⋀ C . ⟦Sig aS ▹ Vx : B ⊢ d : C ; (Vx : A ⊢ e1 ≡ e2 : B) ∈ Theory⟧ ⟹ 
  (Vx : A ⊢ (sub e1 in d) ≡ (sub e2 in d) : C) ∈ Theory"
proof(induct d)
  {
    fix C assume a: "Sig aS ▹ Vx : B ⊢ Vx : C" and b: "(Vx : A ⊢ e1≡e2 : B) ∈ Theory"
    have BCeq: "B = C" using a SigId[of aS B C] by simp
    thus "(Vx : A ⊢ (sub e1 in Vx) ≡ (sub e2 in Vx) : C) ∈ Theory" using b by (simp add: Subst_def)
  }
  {
    fix C f d assume ih: "⋀ B' . ⟦Sig aS ▹ Vx : B ⊢ d : B'; (Vx : A ⊢ e1≡e2 : B) ∈ Theory⟧
      ⟹ (Vx : A ⊢ (sub e1 in d) ≡ (sub e2 in d) : B') ∈ Theory" and wd: "Sig aS ▹ Vx : B ⊢ f E@ d : C" and
      eq: "(Vx : A ⊢ e1 ≡ e2 : B) ∈ Theory"
    from wd obtain B' where B': "f ∈ Sig aS : B' → C" and d: "Sig aS ▹ Vx : B ⊢ d : B'" by auto
    hence "(Vx : A ⊢ (sub e1 in d) ≡ (sub e2 in d) : B') ∈ Theory" using ih eq by simp
    hence "(Vx : A ⊢ f E@ (sub e1 in d) ≡ f E@ (sub e2 in d) : C) ∈ Theory" using B' by (simp add: Congr)
    thus "(Vx : A ⊢ (sub e1 in (f E@ d)) ≡ (sub e2 in (f E@ d)) : C) ∈ Theory" by (simp add: Subst_def)
  }
qed

(*This is the diamond problem in multiple inheritance -- both Interpretation and Axioms share a Signature*)
locale Model = Interpretation I + Axioms Ax
  for I :: "('t,'f,'o,'m) Interpretation" (structure)
  and Ax :: "('t,'f) Axioms" +
  assumes AxSound: "φ ∈ (aAxioms Ax) ⟹ L⟦φ⟧ → (IBool True)"
  and Seq[simp]: "(aSignature Ax) = iS"

lemma (in Interpretation) Equiv:
  assumes "L⟦Vx : A ⊢ e1 ≡ e2 : B⟧ → (IBool True)"
  shows "∃ g . (L⟦Vx : A ⊢ e1 : B⟧ → (IMor g)) ∧ (L⟦Vx : A ⊢ e2 : B⟧ → (IMor g))"
proof-
  from assms Sig2Mor[of A e1 B] obtain g1 where g1: "L⟦Vx : A ⊢ e1 : B⟧ → (IMor g1)" by auto
  from assms Sig2Mor[of A e2 B] obtain g2 where g2: "L⟦Vx : A ⊢ e2 : B⟧ → (IMor g2)" by auto
  have "L⟦Vx : A ⊢ e1≡e2 : B⟧ → (IBool (g1 = g2))" using g1 g2 by auto
  hence "g1 = g2" using assms Functional[of "Vx : A ⊢ e1≡e2 : B" "(IBool True)" "IBool (g1=g2)"] by simp
  thus ?thesis using g1 g2 by auto
qed

lemma (in Interpretation) SubstComp: "⋀ h C . ⟦(L⟦Vx : A ⊢ e : B⟧ → (IMor g)) ; (L⟦Vx : B ⊢ d : C⟧ → (IMor h))⟧ ⟹
  (L⟦Vx : A ⊢ (sub e in d) : C⟧ → (IMor (g ;;⇘iC⇙ h)))"
proof(induct d,auto)
  {
    fix h C assume a: "L⟦Vx : A ⊢ e : B⟧ → IMor g" and b: "L⟦Vx : B ⊢ Vx : C⟧ → (IMor h)"
    show "L⟦Vx : A ⊢ e : C⟧ → IMor (g ;;⇘iC⇙ h)"
    proof-
      have beqc: "B = C" using b SigId[of iS B C] InterpExprWellDefined by simp
      have "L⟦Vx : B ⊢ Vx : B⟧ → (IMor (Id iC Ty⟦B⟧))" using beqc b by auto
      hence h: "h = Id iC Ty⟦B⟧" using b beqc by (auto simp add: Functional)
      have "g maps⇘iC ⇙Ty⟦A⟧ to Ty⟦B⟧" using a MorphismsPreserved by auto
      hence "g ∈ Mor iC" and "cod⇘iC⇙ g = Ty⟦B⟧" by auto
      hence "(g ;;⇘iC⇙ h) = g" using h ICat Category.Cidr[of iC g] by simp
      thus ?thesis using beqc a by simp
    qed
  }
  {
    fix f d C' h C assume 
      i: "⋀ h C' . L⟦Vx : B ⊢ d : C'⟧ → IMor h ⟹ L⟦Vx : A ⊢ (sub e in d) : C'⟧ → (IMor (g ;;⇘iC⇙ h))" and
      a: "L⟦Vx : A ⊢ e : B⟧ → IMor g" "f ∈ Sig iS : C' → C" "L⟦Vx : B ⊢ d : C'⟧ → IMor h"
    show "L⟦Vx : A ⊢ f E@ (sub e in d) : C⟧ → (IMor (g ;;⇘iC⇙ (h ;;⇘iC⇙ Fn⟦f⟧)))"
    proof-
      have "L⟦Vx : A ⊢ (sub e in d) : C'⟧ → (IMor (g ;;⇘iC⇙ h))" using i a by auto
      moreover hence "Sig iS ▹ Vx : A ⊢ (sub e in d) : C'" using InterpExprWellDefined by simp
      ultimately have 1: "L⟦Vx : A ⊢ f E@ (sub e in d) : C⟧ → (IMor ((g ;;⇘iC⇙ h) ;;⇘iC⇙ Fn⟦f⟧))" using a(2) by auto
      have "g maps⇘iC⇙ Ty⟦A⟧ to Ty⟦B⟧" and "h maps⇘iC⇙ Ty⟦B⟧ to Ty⟦C'⟧" and "Fn⟦f⟧ maps⇘iC⇙ Ty⟦C'⟧ to Ty⟦C⟧"
        using a If Expr2Mor by simp+
      hence "g ≈>⇘iC⇙ h" and "h ≈>⇘iC⇙ (Fn⟦f⟧)" using MapsToCompDef[of iC] by simp+
      hence "(g ;;⇘iC⇙ h) ;;⇘iC⇙ Fn⟦f⟧ = g ;;⇘iC⇙ (h ;;⇘iC⇙ Fn⟦f⟧)" using ICat Category.Cassoc[of iC] by simp
      thus ?thesis using 1 by simp
    qed
  }
qed

lemma (in Model) Sound: "φ ∈ Theory ⟹  L⟦φ⟧ → (IBool True)"
proof(rule Theory.induct, (simp_all add: AxSound)+)
  {
    fix A e B assume sig: "Sig iS ▹ Vx : A ⊢ e : B" show "L⟦Vx : A ⊢ e≡e : B⟧ → (IBool True)"
    proof-
      from sig Sig2Mor[of A e B] obtain g where g: "L⟦Vx : A ⊢ e : B⟧ → (IMor g)" by auto
      thus ?thesis using InterpEq[of I A e B g e g] by simp
    qed
  }
  {
    fix A e1 e2 B assume a: "L⟦Vx : A ⊢ e1≡e2 : B⟧ → (IBool True)" show "L⟦Vx : A ⊢ e2≡e1 : B⟧ → (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A ⊢ e1 : B⟧ → (IMor g)" and g2: "L⟦Vx : A ⊢ e2 : B⟧ → (IMor g)"
        using Equiv by auto
      thus ?thesis by auto
    qed
  }
  {
    fix A e1 e2 B e3 assume a: "L⟦Vx : A ⊢ e1≡e2 : B⟧ → (IBool True)" and b: "L⟦Vx : A ⊢ e2≡e3 : B⟧ → (IBool True)"
    show "L⟦Vx : A ⊢ e1≡e3 : B⟧ → (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A ⊢ e1 : B⟧ → (IMor g)" and g2: "L⟦Vx : A ⊢ e2 : B⟧ → (IMor g)"
        using Equiv by auto
      from b obtain g' where g1': "L⟦Vx : A ⊢ e2 : B⟧ → (IMor g')" and g2': "L⟦Vx : A ⊢ e3 : B⟧ → (IMor g')"
        using Equiv by auto
      have eq: "g = g'" using g2 g1' using Functional by auto
      thus ?thesis using eq g1 g2' by auto
    qed
  }
  {
    fix A e1 e2 B f C assume a: "L⟦Vx : A ⊢ e1≡e2 : B⟧ → (IBool True)" and b: "f ∈ Sig iS : B → C"
    show "L⟦Vx : A ⊢ (f E@ e1) ≡ (f E@ e2) : C⟧ → (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A ⊢ e1 : B⟧ → (IMor g)" and g2: "L⟦Vx : A ⊢ e2 : B⟧ → (IMor g)"
        using Equiv by auto      
      have s1: "Sig iS ▹ Vx : A  ⊢ e1 : B" and s2: "Sig iS ▹ Vx : A  ⊢ e2 : B" using g1 g2 InterpExprWellDefined by simp+
      have "L⟦Vx : A  ⊢ (f E@ e1) : C⟧ → (IMor (g ;;⇘iC⇙ Fn⟦f⟧))"
        and "L⟦Vx : A  ⊢ (f E@ e2) : C⟧ → (IMor (g ;;⇘iC⇙ Fn⟦f⟧))" using b g1 s1 g2 s2 by auto
      thus ?thesis using InterpEqEq[of A "(f E@ e1)" C "(g ;;⇘iC⇙ Fn⟦f⟧)"] by simp
    qed
  }
  {
    fix A e1 B e2 e3 C assume a: "Sig iS ▹ (Vx : A ⊢ e1 : B)" and b: "L⟦Vx : B ⊢ e2≡e3 : C⟧ → (IBool True)"
    show "L⟦Vx : A ⊢ (sub e1 in e2) ≡ (sub e1 in e3) : C⟧ → (IBool True)"
    proof-
      from b obtain g where g1: "L⟦Vx : B ⊢ e2 : C⟧ → (IMor g)" and g2: "L⟦Vx : B ⊢ e3 : C⟧ → (IMor g)"
        using Equiv by auto
      from a Sig2Mor[of A e1 B] obtain f where f: "L⟦Vx : A ⊢ e1 : B⟧ → (IMor f)" by auto
      have "L⟦Vx : A ⊢ (sub e1 in e2) : C⟧ → (IMor (f ;;⇘iC⇙ g))" using SubstComp g1 f by simp
      moreover have "L⟦Vx : A ⊢ (sub e1 in e3) : C⟧ → (IMor (f ;;⇘iC⇙ g))" using SubstComp g2 f by simp
      ultimately show ?thesis using InterpEqEq by simp
    qed
  }
qed

record ('t,'f) TermEquivClT = 
  TDomain :: 't
  TExprSet :: "('t,'f) Expression set"
  TCodomain :: 't

locale ZFAxioms = Ax : Axioms Ax for Ax :: "(ZF,ZF) Axioms" (structure) +
  assumes     fnzf: "BaseFunctions (aSignature Ax) ∈ range explode"

lemma [simp]: "ZFAxioms T ⟹ Axioms T" by (simp add: ZFAxioms_def)

(*(tree depth, rule number, components)*)
primrec Expr2ZF :: "(ZF,ZF) Expression ⇒ ZF" where
    Expr2ZFVx: "Expr2ZF Vx = ZFTriple (nat2Nat 0) (nat2Nat 0) Empty" 
  | Expr2ZFfe: "Expr2ZF (f E@ e) = ZFTriple (SucNat (ZFTFst (Expr2ZF e)))
                                 (nat2Nat 1)
                                 (Opair f (Expr2ZF e))"

definition ZF2Expr :: "ZF ⇒ (ZF,ZF) Expression" where
  "ZF2Expr = inv Expr2ZF"

definition "ZFDepth = Nat2nat o ZFTFst"
definition "ZFType = Nat2nat o ZFTSnd"
definition "ZFData = ZFTThd"

lemma Expr2ZFType0: "ZFType (Expr2ZF e) = 0 ⟹ e = Vx"
by(cases e,auto simp add: ZFType_def ZFTSnd Elem_Empty_Nat Elem_SucNat_Nat ZFSucNeq0)

lemma ZFDepthInNat: "Elem (ZFTFst (Expr2ZF e)) Nat"
by(induct e, auto simp add:  ZFTFst HOLZF.Elem_Empty_Nat Elem_SucNat_Nat)

lemma Expr2ZFType1: "ZFType (Expr2ZF e) = 1 ⟹ 
  ∃ f e' . e = (f E@ e') ∧ (Suc (ZFDepth (Expr2ZF e'))) = (ZFDepth (Expr2ZF e))"
by(cases e,auto simp add: ZFType_def ZFTSnd ZFDepth_def ZFTFst ZFZero ZFDepthInNat Nat2nat_SucNat)

lemma Expr2ZFDepth0: "ZFDepth (Expr2ZF e) = 0 ⟹ ZFType (Expr2ZF e) = 0"
by(cases e, auto simp add: ZFDepth_def ZFTFst ZFType_def ZFTSnd ZFSucNeq0 ZFDepthInNat)

lemma Expr2ZFDepthSuc: "ZFDepth (Expr2ZF e) = Suc n ⟹ ZFType (Expr2ZF e) = 1"
by(cases e, auto simp add: ZFDepth_def ZFTFst ZFType_def ZFTSnd ZFSucZero ZFSucNeq0 ZFZero)

lemma Expr2Data: "ZFData (Expr2ZF (f E@ e)) = Opair f (Expr2ZF e)"
by(auto simp add: ZFData_def ZFTThd)

lemma Expr2ZFinj: "inj Expr2ZF"
proof(auto simp add: inj_on_def)
  have a: "⋀ n e d . ⟦n = ZFDepth (Expr2ZF e) ; Expr2ZF e = Expr2ZF d⟧ ⟹ e = d"
  proof-
    fix n show "⋀ e d . ⟦n = ZFDepth (Expr2ZF e) ; Expr2ZF e = Expr2ZF d⟧ ⟹ e = d"
    proof(induct n)
      {
        fix e d assume a: "0 = ZFDepth (Expr2ZF e)" and b: "Expr2ZF e = Expr2ZF d"
        have "0 = ZFDepth (Expr2ZF d)" using a b by simp 
        hence "e = Vx" and "d = Vx" using a by (simp add: Expr2ZFDepth0 Expr2ZFType0)+
        thus "e = d" by simp
      }
      {
        fix n e d assume ih: "⋀ e' d' . ⟦n = ZFDepth (Expr2ZF e') ; Expr2ZF e' = Expr2ZF d'⟧ ⟹ e' = d'"
          and a: "Suc n = ZFDepth (Expr2ZF e)" and b: "Expr2ZF e = Expr2ZF d"
        have "ZFType (Expr2ZF e) = 1" and "ZFType (Expr2ZF d) = 1" using a b Expr2ZFDepthSuc[of e n] by simp+
        from this Expr2ZFType1[of e] Expr2ZFType1[of d] obtain fe fd e' d' 
          where e: "e = (fe E@ e') ∧ (Suc (ZFDepth (Expr2ZF e'))) = (ZFDepth (Expr2ZF e))" and
          d: "d = (fd E@ d') ∧ (Suc (ZFDepth (Expr2ZF d'))) = (ZFDepth (Expr2ZF d))" by auto
        hence "Suc (ZFDepth (Expr2ZF e')) = Suc n" using a by simp
        hence ne: "(ZFDepth (Expr2ZF e')) = n" by (rule Suc_inject)
        have edat: "ZFData (Expr2ZF e) = Opair fe (Expr2ZF e')" using e Expr2Data by simp
        have ddat: "ZFData (Expr2ZF d) = Opair fd (Expr2ZF d')" using d Expr2Data by simp
        have fd_eq_fe: "fe = fd" and "(Expr2ZF e') = (Expr2ZF d')" using edat ddat Opair b by auto
        hence "e' = d'" using ne ih by auto
        thus "e = d" using e d fd_eq_fe by auto
      }
    qed
  qed
  fix e d show "Expr2ZF e = Expr2ZF d ⟹ e = d" using a by auto
qed

definition "TermEquivClGen T A e B ≡ {e' . (Vx : A ⊢ e' ≡ e : B) ∈ Axioms.Theory T}"
definition "TermEquivCl' T A e B ≡ ⦇ TDomain = A , TExprSet = TermEquivClGen T A e B , TCodomain = B⦈"

definition m2ZF :: "(ZF,ZF) TermEquivClT ⇒ ZF" where
  "m2ZF t ≡ ZFTriple (TDomain t) (implode (Expr2ZF ` (TExprSet t))) (TCodomain t)"

definition ZF2m :: "(ZF,ZF) Axioms ⇒ ZF ⇒ (ZF,ZF) TermEquivClT" where
  "ZF2m T ≡ inv_into {TermEquivCl' T A e B | A e B . True} m2ZF"

lemma TDomain: "TDomain (TermEquivCl' T A e B) = A" by (simp add: TermEquivCl'_def)
lemma TCodomain: "TCodomain (TermEquivCl' T A e B) = B" by (simp add: TermEquivCl'_def)

primrec WellFormedToSet :: "(ZF,ZF) Signature ⇒ nat ⇒ (ZF,ZF) Expression set" where
  WFS0: "WellFormedToSet S 0 = {Vx}"
| WFSS: "WellFormedToSet S (Suc n) = (WellFormedToSet S n) ∪
                { f E@ e | f e . f ∈ BaseFunctions S ∧ e ∈ (WellFormedToSet S n)}"

lemma WellFormedToSetInRangeExplode: "ZFAxioms T ⟹ (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n)) ∈ range explode"
proof((induct n),(simp add: WellFormedToSet_def SingletonInRangeExplode))
  fix n assume zfx: "ZFAxioms T" and ih: "ZFAxioms T ⟹ Expr2ZF ` WellFormedToSet aS⇘T⇙ n ∈ range explode"
  hence a: "Expr2ZF ` WellFormedToSet aS⇘T⇙ n ∈ range explode" by simp
  have "Expr2ZF ` { f E@ e | f e . f ∈ BaseFunctions aS⇘T⇙ ∧ e ∈ (WellFormedToSet aS⇘T⇙ n)}
    = (λ (f, ze) . Expr2ZF (f E@ (ZF2Expr ze))) ` ((BaseFunctions aS⇘T⇙) × Expr2ZF ` (WellFormedToSet aS⇘T⇙ n))"
  proof (auto simp add: image_Collect image_def ZF2Expr_def Expr2ZFinj)
    fix f e
    assume f: "f ∈ BaseFunctions aS⇘T⇙" and e: "e ∈ WellFormedToSet aS⇘T⇙ n"
    show "∃ x ∈ BaseFunctions aS⇘T⇙.∃y. (∃ x ∈ WellFormedToSet aS⇘T⇙ n. y = Expr2ZF x) ∧
      ZFTriple (SucNat (ZFTFst (Expr2ZF e))) (SucNat Empty) (Opair f (Expr2ZF e)) =
      ZFTriple (SucNat (ZFTFst (Expr2ZF (inv Expr2ZF y)))) (SucNat Empty) (Opair x (Expr2ZF (inv Expr2ZF y)))"
      apply(rule bexI[where ?x = f], rule exI[where ?x = "Expr2ZF e"])
      apply (auto simp add: Expr2ZFinj f e)
      done
    show "∃x. (∃f e. x = f E@ e ∧ f ∈ (BaseFunctions aS⇘T⇙) ∧ e ∈ WellFormedToSet aS⇘T⇙ n) ∧
              ZFTriple (SucNat (ZFTFst (Expr2ZF e))) (SucNat Empty) (Opair f (Expr2ZF e)) = Expr2ZF x"
      apply(rule exI[where ?x = "f E@ e"])
      apply (auto simp add: f e)
      done
  qed
  moreover have "(BaseFunctions aS⇘T⇙) ∈ range explode" using zfx ZFAxioms.fnzf by simp 
  ultimately have "Expr2ZF ` { f E@ e | f e . f ∈ BaseFunctions aS⇘T⇙ ∧ e ∈ (WellFormedToSet aS⇘T⇙ n)} ∈ range explode"
    using a ZFProdFnInRangeExplode by simp
  moreover have "Expr2ZF ` WellFormedToSet aS⇘T⇙ (Suc n) = (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n)) ∪
                (Expr2ZF  ` { f E@ e | f e . f ∈ BaseFunctions aS⇘T⇙ ∧ e ∈ (WellFormedToSet aS⇘T⇙ n)})" by auto
  ultimately show "Expr2ZF ` WellFormedToSet aS⇘T⇙ (Suc n) ∈ range explode" using ZFUnionInRangeExplode a by simp
qed

lemma WellDefinedToWellFormedSet: "⋀ B . (Sig S ▹ (Vx : A ⊢ e : B)) ⟹ ∃n. e ∈ WellFormedToSet S n"
proof(induct e)
  {
    fix B assume "Sig S ▹ Vx : A ⊢ Vx : B"
    show "∃n. Vx ∈ WellFormedToSet S n" by (rule exI[of _ 0], auto)
  }
  {
    fix f e B assume ih: "⋀B'. Sig S ▹ Vx : A ⊢ e : B' ⟹ ∃n. e ∈ WellFormedToSet S n"
      and "Sig S ▹ Vx : A ⊢ (f E@ e) : B"
    from this obtain B' where "Sig S ▹ (Vx : A ⊢ e : B')" and f: "f ∈ Sig S : B' → B" by auto
    from this obtain n where a: "e ∈ WellFormedToSet S n" using ih by auto
    have ff: "f ∈ BaseFunctions S" using f by auto
    show "∃n. (f E@ e) ∈ WellFormedToSet S n" by(rule exI[of _ "Suc n"], auto simp add: a ff)
  }
qed

lemma TermSetInSet: "ZFAxioms T ⟹ Expr2ZF ` (TermEquivClGen T A e B) ∈ range explode"
proof-
  assume zfax: "ZFAxioms T"
  have "(TermEquivClGen T A e B) ⊆ {e' . (Sig aS⇘T⇙ ▹ (Vx : A ⊢ e' : B))}"
  proof(auto simp add: TermEquivClGen_def)
    fix x assume "Vx : A ⊢ x≡e : B ∈ Axioms.Theory T" 
    hence "Sig aS⇘T⇙ ▹ Vx : A ⊢ x≡e : B" by (auto simp add: Axioms.Equiv2WellDefined zfax)
    thus "Sig aS⇘T⇙ ▹ Vx : A ⊢ x : B" by auto
  qed
  also have "... ⊆ (⋃ n . (WellFormedToSet aS⇘T⇙ n))" by (auto simp add: WellDefinedToWellFormedSet)
  finally have "Expr2ZF ` (TermEquivClGen T A e B) ⊆ Expr2ZF ` (⋃ n . (WellFormedToSet aS⇘T⇙ n))" by auto
  also have "... = (⋃ n . (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n)))" by auto
  finally have "Expr2ZF ` (TermEquivClGen T A e B) ⊆ (⋃ n . (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n)))" by auto
  moreover have "(⋃ n . (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n))) ∈ range explode" 
    using zfax ZFUnionNatInRangeExplode WellFormedToSetInRangeExplode by auto
  ultimately show ?thesis using  ZFSubsetRangeExplode[of 
    "(⋃ n . (Expr2ZF ` (WellFormedToSet aS⇘T⇙ n)))" "Expr2ZF ` (TermEquivClGen T A e B)"] by simp
qed

lemma m2ZFinj_on: "ZFAxioms T ⟹ inj_on m2ZF {TermEquivCl' T A e B | A e B . True}"
apply(auto simp only: inj_on_def m2ZF_def)
apply(drule ZFTriple)
apply(auto simp add: TDomain TCodomain implode_def)
apply(simp add: TermEquivCl'_def)
apply(drule inv_into_injective)
apply(auto simp add: TermSetInSet inj_image_eq_iff Expr2ZFinj)
done

lemma ZF2m: "ZFAxioms T ⟹ ZF2m T (m2ZF (TermEquivCl' T A e B)) = (TermEquivCl' T A e B)"
proof-
  assume zfax: "ZFAxioms T"
  let ?A = "{TermEquivCl' T A e B | A e B . True}" and ?x = "TermEquivCl' T A e B"
  have "?x ∈ ?A" by auto
  thus ?thesis using m2ZFinj_on[of T] inv_into_f_f zfax by (simp add:  ZF2m_def )
qed

definition TermEquivCl (‹[_,_,_]ı›) where "[A,e,B]⇘T⇙ ≡ m2ZF (TermEquivCl' T A e B)"

definition "CLDomain T ≡ TDomain o ZF2m T"
definition "CLCodomain T ≡ TCodomain o ZF2m T"

definition "CanonicalComp T f g ≡ 
  THE h . ∃ e e' . h = [CLDomain T f,sub e in e',CLCodomain T g]⇘T⇙ ∧  
  f = [CLDomain T f,e,CLCodomain T f]⇘T⇙ ∧ g = [CLDomain T g,e',CLCodomain T g]⇘T⇙"

lemma CLDomain: "ZFAxioms T ⟹ CLDomain T [A,e,B]⇘T⇙ = A"  by (simp add: TermEquivCl_def CLDomain_def ZF2m TDomain)
lemma CLCodomain: "ZFAxioms T ⟹ CLCodomain T [A,e,B]⇘T⇙ = B"  by (simp add: TermEquivCl_def CLCodomain_def ZF2m TCodomain)

lemma Equiv2Cl: assumes "Axioms T" and "(Vx : A ⊢ e ≡ d : B) ∈ Axioms.Theory T" shows  "[A,e,B]⇘T⇙ = [A,d,B]⇘T⇙"
proof-
  have "{e'. (Vx : A ⊢ e'≡e : B) ∈ Axioms.Theory T} = {e'. (Vx : A ⊢ e'≡d : B) ∈ Axioms.Theory T}"
    using assms by(blast intro: Axioms.Trans Axioms.Symm)
  thus ?thesis by(auto simp add: TermEquivCl_def TermEquivCl'_def TermEquivClGen_def)
qed

lemma Cl2Equiv: 
  assumes axt: "ZFAxioms T" and sa: "Sig aS⇘T⇙ ▹ (Vx : A ⊢ e : B)" and cl: "[A,e,B]⇘T⇙ = [A,d,B]⇘T⇙"
  shows "(Vx : A ⊢ e ≡ d : B) ∈ Axioms.Theory T"
proof-
  have "ZF2m T (m2ZF (TermEquivCl' T A e B)) = ZF2m T (m2ZF (TermEquivCl' T A d B))" using cl by (simp add: TermEquivCl_def)
  hence a:"TermEquivCl' T A e B = TermEquivCl' T A d B" using assms by (simp add: ZF2m)
  have "(Vx : A ⊢ e ≡ e : B) ∈ Axioms.Theory T" using axt sa Axioms.Refl[of T] by simp
  hence "e ∈ TermEquivClGen T A e B" by (simp add: TermEquivClGen_def)
  hence "e ∈ TermEquivClGen T A d B" using a by (simp add: TermEquivCl'_def)
  thus ?thesis by (simp add: TermEquivClGen_def)
qed 

lemma CanonicalCompWellDefined: 
  assumes zaxt: "ZFAxioms T" and "Sig aS⇘T⇙ ▹ (Vx : A ⊢ d : B)" and "Sig aS⇘T⇙ ▹ (Vx : B ⊢ d' : C)" 
  shows "CanonicalComp T [A,d,B]⇘T⇙ [B,d',C]⇘T⇙ = [A,sub d in d',C]⇘T⇙"
proof((simp only: zaxt CanonicalComp_def CLDomain CLCodomain),(rule the_equality),
    (rule exI[of _ d], rule exI[of _ d'], auto))
  fix e e' assume de: "[A,d,B]⇘T⇙ = [A,e,B]⇘T⇙" and de': "[B,d',C]⇘T⇙ = [B,e',C]⇘T⇙"
  have axt: "Axioms T" using assms by simp
  have a: "(Vx : A ⊢ d ≡ e : B) ∈ Axioms.Theory T" using assms de Cl2Equiv by simp
  hence sa: "(Vx : A ⊢ (sub d in d') ≡ (sub e in d') : C) ∈ Axioms.Theory T" 
    using assms Axioms.Subst'[of T] by simp
  have b: "(Vx : B ⊢ d'≡ e' : C) ∈ Axioms.Theory T" using assms de' Cl2Equiv by simp
  have "Sig aS⇘T⇙ ▹ (Vx : A ⊢ d ≡ e : B)" using a axt Axioms.Equiv2WellDefined[of T] by simp
  hence "Sig aS⇘T⇙ ▹ (Vx : A ⊢ e : B)" by auto
  hence "(Vx : A ⊢ (sub e in d') ≡ (sub e in e') : C) ∈ Axioms.Theory T" using b Axioms.Subst[of T] axt by simp
  hence "(Vx : A ⊢ (sub e in e') ≡ (sub d in d') : C) ∈ Axioms.Theory T" using sa axt
    by (blast intro: Axioms.Symm[of T] Axioms.Trans[of T])
  thus "[A,sub e in e',C]⇘T⇙ = [A,sub d in d',C]⇘T⇙" using zaxt Equiv2Cl by simp
qed

definition "CanonicalCat' T ≡ ⦇
  Obj = BaseTypes (aS⇘T⇙), 
  Mor = {[A,e,B]⇘T⇙ | A e B . Sig aS⇘T⇙ ▹ (Vx : A ⊢ e : B)}, 
  Dom = CLDomain T, 
  Cod = CLCodomain T, 
  Id  = (λ A . [A,Vx,A]⇘T⇙), 
  Comp = CanonicalComp T
  ⦈"

definition "CanonicalCat T ≡ MakeCat (CanonicalCat' T)"

lemma CanonicalCat'MapsTo: 
  assumes "f maps⇘CanonicalCat' T⇙ X to Y" and zx: "ZFAxioms T"
  shows "∃ ef . f = [X,ef,Y]⇘T⇙ ∧ Sig (aSignature T) ▹ (Vx : X ⊢ ef : Y)"
proof-
  have fm: "f ∈ Mor (CanonicalCat' T)" and fd: "Dom (CanonicalCat' T) f = X" and fc: "Cod (CanonicalCat' T) f = Y"
    using assms by auto
  from fm obtain ef A B where ef: "f = [A,ef,B]⇘T⇙" and efsig: "Sig (aSignature T) ▹ (Vx : A ⊢ ef : B)" 
    by (auto simp add: CanonicalCat'_def)
  have "A = X" and "B = Y" using fd fc ef zx CLDomain[of T] CLCodomain[of T]  by (simp add: CanonicalCat'_def)+
  thus ?thesis using ef efsig by auto
qed

lemma CanonicalCatCat': "ZFAxioms T ⟹ Category_axioms (CanonicalCat' T)"
proof(auto simp only: Category_axioms_def)
  have obj: "obj⇘CanonicalCat' T⇙ = BaseTypes (aSignature T)" by (simp add: CanonicalCat'_def)
  assume zx: "ZFAxioms T"
  hence axt: "Axioms T" by simp
  {
    fix f assume a: "f ∈ mor⇘CanonicalCat' T⇙" 
    from a obtain A e B where f: "f = [A,e,B]⇘T⇙" and fwd: "Sig (aSignature T) ▹ (Vx : A ⊢ e : B)"
      by (auto simp add: CanonicalCat'_def)
    have domf: "dom⇘CanonicalCat' T⇙ f = CLDomain T f" and codf: "cod⇘CanonicalCat' T⇙ f = CLCodomain T f" 
      by (simp add: CanonicalCat'_def)+
    have absig: "A ∈ Ty⇘aSignature T⇙ ∧ B ∈ Ty⇘aSignature T⇙" using fwd Signature.SigTy[of "(aSignature T)"] Axioms.AxSig axt
      by auto
    have Awd: "Sig (aSignature T) ▹ (Vx : A ⊢ Vx : A)" and Bwd: "Sig (aSignature T) ▹ (Vx : B ⊢ Vx : B)" 
      using absig by auto
    show "dom⇘CanonicalCat' T⇙ f ∈ obj⇘CanonicalCat' T⇙" using domf f obj CLDomain[of T A e B] absig zx
      by simp
    show "cod⇘CanonicalCat' T⇙ f ∈ obj⇘CanonicalCat' T⇙" using codf f obj CLCodomain[of T A e B] absig zx
      by simp
    have idA: "Id (CanonicalCat' T) A = [A,Vx,A]⇘T⇙" and idB: "Id (CanonicalCat' T) B = [B,Vx,B]⇘T⇙" 
      by (simp add: CanonicalCat'_def)+
    have "(Id (CanonicalCat' T) (dom⇘CanonicalCat' T⇙ f)) ;;⇘CanonicalCat' T⇙ f = [A, sub Vx in e, B]⇘T⇙" 
      using f domf CLDomain[of T A e B] idA axt CanonicalCompWellDefined[of T] Awd fwd zx
      by (simp add: CanonicalCat'_def)
    thus "(Id (CanonicalCat' T) (dom⇘CanonicalCat' T⇙ f)) ;;⇘CanonicalCat' T⇙ f = f" using f SubstXinE[of e] by simp
    have "f ;;⇘CanonicalCat' T⇙ (Id (CanonicalCat' T) (cod⇘CanonicalCat' T⇙ f)) = [A, sub e in Vx, B]⇘T⇙" 
      using f codf CLCodomain[of T A e B] idB axt CanonicalCompWellDefined[of T] Bwd fwd zx
      by (simp add: CanonicalCat'_def)
    thus "f ;;⇘CanonicalCat' T⇙ (Id (CanonicalCat' T) (cod⇘CanonicalCat' T⇙ f)) = f" using f Subst_def by simp
  }
  {
    fix X assume a: "X ∈ obj⇘CanonicalCat' T⇙"
    have "X ∈ BaseTypes (aSignature T)" using a by (simp add: CanonicalCat'_def)
    hence b: "Sig (aSignature T) ▹ (Vx : X ⊢ Vx : X)" by auto
    show "Id (CanonicalCat' T) X maps⇘CanonicalCat' T⇙ X to X"
      apply(rule MapsToI)
      apply(auto simp add: CanonicalCat'_def CLDomain CLCodomain zx)
      apply(rule exI)+
      apply(auto simp add: b)
      done
  }
  {
    fix f g h assume a: "f ≈>⇘CanonicalCat' T⇙ g" and b: "g ≈>⇘CanonicalCat' T⇙ h"
    from a b have fm: "f ∈ Mor (CanonicalCat' T)" and gm: "g ∈ Mor (CanonicalCat' T)" 
      and hm: "h ∈ Mor (CanonicalCat' T)" and fg: "Cod (CanonicalCat' T) f = Dom (CanonicalCat' T) g" 
      and gh: "Cod (CanonicalCat' T) g = Dom (CanonicalCat' T) h" by auto
    from fm obtain A ef B where f: "f = [A,ef,B]⇘T⇙" and fwd: "Sig (aSignature T) ▹ (Vx : A ⊢ ef : B)"
      by (auto simp add: CanonicalCat'_def)
    from gm obtain B' eg C where g: "g = [B',eg,C]⇘T⇙" and gwd: "Sig (aSignature T) ▹ (Vx : B' ⊢ eg : C)"
      by (auto simp add: CanonicalCat'_def)
    from hm obtain C' eh D where h: "h = [C',eh,D]⇘T⇙" and hwd: "Sig (aSignature T) ▹ (Vx : C' ⊢ eh : D)"
      by (auto simp add: CanonicalCat'_def)
    from fg have Beq: "B = B'" using f g zx CLCodomain[of T A ef B] CLDomain[of T B' eg C] by (simp add: CanonicalCat'_def)
    from gh have Ceq: "C = C'" using g h zx CLCodomain[of T B' eg C] CLDomain[of T C' eh D] by (simp add: CanonicalCat'_def)
    have "CanonicalComp T (CanonicalComp T f g) h = CanonicalComp T f (CanonicalComp T g h)"
    proof-
      have "(CanonicalComp T f g) = [A,sub ef in eg,C]⇘T⇙" 
        using axt fwd gwd Beq zx CanonicalCompWellDefined[of T A ef B eg C] f g by simp
      moreover have "Sig aS⇘T⇙ ▹ Vx : A ⊢ sub ef in eg : C" using fwd gwd SubstWellDefined Beq by simp
      ultimately have a: "CanonicalComp T (CanonicalComp T f g) h = [A,(sub (sub ef in eg) in eh),D]⇘T⇙"
        using CanonicalCompWellDefined[of T A "sub ef in eg" C eh D] axt hwd h Beq Ceq zx by simp
      have "(CanonicalComp T g h) = [B,sub eg in eh,D]⇘T⇙"
        using axt gwd hwd Ceq Beq CanonicalCompWellDefined[of T B eg C eh D] g h zx by simp
      moreover have "Sig aS⇘T⇙ ▹ Vx : B ⊢ sub eg in eh : D" using gwd hwd SubstWellDefined Beq Ceq by simp
      ultimately have b: "CanonicalComp T f (CanonicalComp T g h) = [A,(sub ef in (sub eg in eh)),D]⇘T⇙"
        using CanonicalCompWellDefined[of T A ef B "sub eg in eh" D] axt fwd f zx by simp
      show ?thesis using a b by (simp add: SubstAssoc)
    qed
    thus "(f ;;⇘CanonicalCat' T⇙ g) ;;⇘CanonicalCat' T⇙ h = f ;;⇘CanonicalCat' T⇙ (g ;;⇘CanonicalCat' T⇙ h)"
      by(simp add: CanonicalCat'_def)
  }
  {
    fix f X Y g Z assume a: "f maps⇘CanonicalCat' T⇙ X to Y" and b: "g maps⇘CanonicalCat' T⇙ Y to Z"
    from a CanonicalCat'MapsTo[of T f X Y] obtain ef 
      where f: "f = [X,ef,Y]⇘T⇙" and fwd: "Sig (aSignature T) ▹ (Vx : X ⊢ ef : Y)" using zx by auto
    from b CanonicalCat'MapsTo[of T g Y Z] obtain eg
      where g: "g = [Y,eg,Z]⇘T⇙" and gwd: "Sig (aSignature T) ▹ (Vx : Y ⊢ eg : Z)" using zx by auto
    have fg: "CanonicalComp T f g = [X,sub ef in eg,Z]⇘T⇙" 
      using CanonicalCompWellDefined[of T X ef Y eg Z] f g fwd gwd zx by simp
    have fgwd: "Sig (aSignature T) ▹ (Vx : X ⊢ sub ef in eg : Z)" 
      using fwd gwd SubstWellDefined[of "aS⇘T⇙"] by simp
    have "(CanonicalComp T f g) maps⇘CanonicalCat' T⇙ X to Z"
    proof(rule MapsToI)
      show "Dom (CanonicalCat' T) (CanonicalComp T f g) = X" 
        using fg CLDomain[of T] zx by (simp add: CanonicalCat'_def)
      show "CanonicalComp T f g ∈ Mor (CanonicalCat' T)" using fg fgwd by (auto simp add: CanonicalCat'_def)
      show "Cod (CanonicalCat' T) (CanonicalComp T f g) = Z" 
        using fg CLCodomain[of T] zx by (simp add: CanonicalCat'_def)
    qed
    thus "f ;;⇘CanonicalCat' T⇙ g maps⇘CanonicalCat' T⇙ X to Z" by (simp add: CanonicalCat'_def)
  }
qed

lemma CanonicalCatCat: "ZFAxioms T ⟹ Category (CanonicalCat T)"
by (simp add: CanonicalCat_def CanonicalCatCat' MakeCat)

definition CanonicalInterpretation where 
"CanonicalInterpretation T ≡ ⦇
  ISignature = aSignature T,
  ICategory  = CanonicalCat T,
  ITypes     = λ A . A,
  IFunctions = λ f . [SigDom (aSignature T) f, f E@ Vx, SigCod (aSignature T) f]⇘T⇙
⦈"

abbreviation "CI T ≡ CanonicalInterpretation T"

lemma CIObj: "Obj (CanonicalCat T) = BaseTypes (aSignature T)"
by (simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)

lemma CIMor: "ZFAxioms T ⟹ [A,e,B]⇘T⇙ ∈ Mor (CanonicalCat T) = Sig (aSignature T) ▹ (Vx : A ⊢ e : B)"
proof(auto simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)
  fix A' e' B' assume zx: "ZFAxioms T" and b: "[A,e,B]⇘T⇙ = [A',e',B']⇘T⇙" and c: "Sig aS⇘T⇙ ▹ Vx : A' ⊢ e' : B'"
  have "CLDomain T [A,e,B]⇘T⇙ = CLDomain T [A',e',B']⇘T⇙" 
    and "CLCodomain T [A,e,B]⇘T⇙ = CLCodomain T [A',e',B']⇘T⇙" using b by simp+
  hence "A = A'" and "B = B'" by (simp add: CLDomain CLCodomain zx)+
  hence "(Vx : A ⊢ e' ≡ e : B) ∈ Axioms.Theory T" using zx b c Cl2Equiv[of T A e' B e] by simp
  hence "Sig aS⇘T⇙ ▹ (Vx : A ⊢ e' ≡ e : B)" using Axioms.Equiv2WellDefined[of T] zx by simp
  thus "Sig aS⇘T⇙ ▹ Vx : A ⊢ e : B" by auto
qed

lemma CIDom: "⟦ZFAxioms T ; [A,e,B]⇘T⇙ ∈ Mor(CanonicalCat T)⟧ ⟹  Dom (CanonicalCat T) [A,e,B]⇘T⇙ = A"
proof-
  assume "[A,e,B]⇘T⇙ ∈ Mor(CanonicalCat T)" and "ZFAxioms T"
  thus "Dom (CanonicalCat T) [A,e,B]⇘T⇙ = A" 
    by (simp add: CLDomain MakeCatMor CanonicalCat_def MakeCat_def CanonicalCat'_def)
qed

lemma CICod: "⟦ZFAxioms T ; [A,e,B]⇘T⇙ ∈ Mor(CanonicalCat T)⟧ ⟹ Cod (CanonicalCat T) [A,e,B]⇘T⇙ = B"
proof-
  assume "[A,e,B]⇘T⇙ ∈ Mor(CanonicalCat T)" and "ZFAxioms T"
  thus "Cod (CanonicalCat T) [A,e,B]⇘T⇙ = B" 
    by (simp add: CLCodomain MakeCatMor CanonicalCat_def MakeCat_def CanonicalCat'_def)
qed

lemma CIId: "⟦A ∈ BaseTypes (aSignature T)⟧ ⟹ Id (CanonicalCat T) A = [A,Vx,A]⇘T⇙"
by(simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)

lemma CIComp: 
  assumes "ZFAxioms T" and "Sig (aSignature T) ▹ (Vx : A ⊢ e : B)" and "Sig (aSignature T) ▹ (Vx : B ⊢ d : C)"
  shows "[A,e,B]⇘T⇙ ;;⇘CanonicalCat T⇙ [B,d,C]⇘T⇙ = [A,sub e in d,C]⇘T⇙"
proof-
  have "[A,e,B]⇘T⇙ ≈>⇘CanonicalCat' T⇙ [B,d,C]⇘T⇙"
  proof(rule CompDefinedI)
    show "[A,e,B]⇘T⇙ ∈ Mor (CanonicalCat' T)" and "[B,d,C]⇘T⇙ ∈ Mor (CanonicalCat' T)"
      using assms by (auto simp add:  CanonicalCat'_def)
    have "cod⇘CanonicalCat' T⇙ [A,e,B]⇘T⇙ = B" using assms by (simp add: CanonicalCat'_def CLCodomain)
    moreover have "dom⇘CanonicalCat' T⇙ [B,d,C]⇘T⇙ = B" using assms by (simp add: CanonicalCat'_def CLDomain)
    ultimately show "cod⇘CanonicalCat' T⇙ [A,e,B]⇘T⇙ = dom⇘CanonicalCat' T⇙ [B,d,C]⇘T⇙" by simp
  qed
  hence "[A,e,B]⇘T⇙ ;;⇘CanonicalCat T⇙ [B,d,C]⇘T⇙ = [A,e,B]⇘T⇙ ;;⇘CanonicalCat' T⇙ [B,d,C]⇘T⇙"
    by (auto simp add: MakeCatComp CanonicalCat_def)
  thus "[A,e,B]⇘T⇙ ;;⇘CanonicalCat T⇙ [B,d,C]⇘T⇙ = [A, sub e in d, C]⇘T⇙" 
    using CanonicalCompWellDefined[of T] assms by (simp add: CanonicalCat'_def)
qed

lemma [simp]: "ZFAxioms T ⟹ Category iC⇘CI T⇙" by(simp add: CanonicalInterpretation_def CanonicalCatCat[of T])
lemma [simp]: "ZFAxioms T ⟹ Signature iS⇘CI T⇙" by(simp add: CanonicalInterpretation_def Axioms.AxSig)

lemma CIInterpretation: "ZFAxioms T ⟹ Interpretation (CI T)"
proof(auto simp only: Interpretation_def)
  assume xt: "ZFAxioms T"
  show "Category iC⇘CI T⇙" and "Signature iS⇘CI T⇙" using xt by simp+
  {
    fix A assume "A ∈ BaseTypes (iS⇘CI T⇙)" thus "Ty⟦A⟧⇘CI T⇙ ∈ Obj (iC⇘CI T⇙)"
      by(simp add: CanonicalInterpretation_def CIObj[of T])
  }
  {
    fix f A B assume a: "f ∈ Sig iS⇘CI T⇙ : A → B"
    hence "[sDom⇘ISignature (CI T)⇙ f,f E@ Vx,sCod⇘ISignature (CI T)⇙ f]⇘T⇙ ∈ mor⇘CanonicalCat T⇙"
      using xt by(auto simp add: CanonicalInterpretation_def CIMor)
    thus "Fn⟦f⟧⇘CI T⇙ maps⇘ICategory (CI T) ⇙Ty⟦A⟧⇘CI T⇙ to Ty⟦B⟧⇘CI T⇙" using a xt
      by(auto simp add: CanonicalInterpretation_def MapsTo_def funsignature_abbrev_def CIDom CICod)
  }
qed

lemma CIInterp2Mor: "ZFAxioms T ⟹ (⋀ B . Sig iS⇘CI T⇙ ▹ (Vx : A ⊢ e : B) ⟹  L⟦Vx : A ⊢ e : B⟧⇘CI T⇙ → (IMor [A, e, B]⇘T⇙))"
proof(induct e)
  assume xt: "ZFAxioms T"
  {
    fix B assume a: "Sig iS⇘CI T⇙ ▹ Vx : A ⊢ Vx : B" 
    have aeqb: "A = B" using a SigId[of "iS⇘CI T⇙" A B] Interpretation.InterpExprWellDefined[of "CI T"] by simp
    moreover have bt: "A ∈ BaseTypes iS⇘CI T⇙" using a SigTyId aeqb by simp
    ultimately have b: "L⟦Vx : A ⊢ Vx : B⟧⇘CI T⇙ → (IMor (Id iC⇘CI T⇙ Ty⟦A⟧⇘CI T⇙))" by auto
    have "Ty⟦A⟧⇘CI T⇙ = A" by (simp add: CanonicalInterpretation_def)
    hence "(Id iC⇘CI T⇙ Ty⟦A⟧⇘CI T⇙) = [A,Vx,A]⇘T⇙" using bt CIId by(simp add: CanonicalInterpretation_def)
    thus "L⟦Vx : A ⊢ Vx : B⟧⇘CI T⇙ → (IMor [A,Vx,B]⇘T⇙)" using aeqb b by simp
  }
  {
    fix f e B assume ih: "⋀B'. ⟦ZFAxioms T ; Sig iS⇘CI T⇙ ▹ (Vx : A ⊢ e : B')⟧ ⟹ (L⟦Vx : A ⊢ e : B'⟧⇘CI T⇙ → (IMor [A,e,B']⇘T⇙))"
    and a: "Sig iS⇘CI T⇙ ▹ Vx : A ⊢ f E@ e : B"
    from a obtain B' where sig: "Sig iS⇘CI T⇙ ▹ (Vx : A ⊢ e : B')" and f: "f ∈ Sig iS⇘CI T⇙ : B' → B" by auto 
    hence "L⟦Vx : A ⊢ e : B'⟧⇘CI T⇙ → (IMor [A,e,B']⇘T⇙)" using ih xt by auto
    hence b: "L⟦Vx : A ⊢ f E@ e : B⟧⇘CI T⇙ → (IMor ([A,e,B']⇘T⇙ ;;⇘ICategory (CI T)⇙ Fn⟦f⟧⇘CI T⇙))" using sig f by auto
    have "[A,e,B']⇘T⇙ ;;⇘ICategory (CI T)⇙ Fn⟦f⟧⇘CI T⇙ = [A,f E@ e,B]⇘T⇙" 
    proof-
      have aa: "Fn⟦f⟧⇘CI T⇙ = [B', f E@ Vx, B]⇘T⇙" using f by (simp add: CanonicalInterpretation_def funsignature_abbrev_def)
      have "Sig iS⇘CI T⇙ ▹ Vx : A ⊢ e : B'" and "Sig iS⇘CI T⇙ ▹ Vx : B' ⊢ f E@ Vx : B"  using sig f by auto
      hence "[A,e,B']⇘T⇙ ;;⇘ICategory (CI T)⇙ [B', f E@ Vx, B]⇘T⇙ = [A, sub e in (f E@ Vx), B]⇘T⇙" 
        using CIComp[of T] xt by (simp add: CanonicalInterpretation_def)
      moreover have "sub e in (f E@ Vx) = f E@ e" by (auto simp add: Subst_def)
      ultimately show ?thesis using aa by simp
    qed
    thus "L⟦Vx : A ⊢ f E@ e : B⟧⇘CI T⇙ → (IMor [A,f E@ e,B]⇘T⇙)" using b by simp
  }
qed

lemma CIModel: "ZFAxioms T ⟹ Model (CI T) T"
proof(auto simp add: Model_def Model_axioms_def )
  assume xt: "ZFAxioms T"
  have axt: "Axioms T" using xt by simp
  show ii: "Interpretation (CI T)" using xt by (simp add: CIInterpretation)
  show aeq: "aS⇘T⇙ = iS⇘CI T⇙" by (simp add: CanonicalInterpretation_def)
  {
    fix φ assume a: "φ ∈ aAxioms T"
    from a Axioms.AxT obtain A B e d where φ: "φ = Vx : A ⊢ e ≡ d : B" and sig: "Sig aS⇘T⇙ ▹ Vx : A ⊢ e ≡ d : B" 
      using axt by blast
    have "Sig aS⇘T⇙ ▹ Vx : A ⊢ e : B" using sig by auto
    hence e: "L⟦Vx : A ⊢ e : B⟧⇘CI T⇙ → (IMor [A, e, B]⇘T⇙)" using aeq CIInterp2Mor xt by simp
    have "Sig aS⇘T⇙ ▹ Vx : A ⊢ d : B" using sig by auto
    hence d: "L⟦Vx : A ⊢ d : B⟧⇘CI T⇙ → (IMor [A, d, B]⇘T⇙)" using aeq CIInterp2Mor xt by simp
    have "φ ∈ Axioms.Theory T" using a axt by (simp add: Axioms.Theory.Ax)
    hence "[A, e, B]⇘T⇙ = [A, d, B]⇘T⇙" using φ Equiv2Cl axt by simp
    thus "L⟦φ⟧⇘CI T⇙ → (IBool True)" using e d φ ii InterpEq[of "CI T" A e B "[A, e, B]⇘T⇙" d "[A, d, B]⇘T⇙"] by simp
  }
qed

lemma CIComplete: assumes "ZFAxioms T" and "L⟦φ⟧⇘CI T⇙ → (IBool True)" shows "φ ∈ Axioms.Theory T"
proof-
  have ii: "Interpretation (CI T)" using assms by (simp add: CIInterpretation)
  hence aeq: "aS⇘T⇙ = iS⇘CI T⇙" by (simp add: CanonicalInterpretation_def)
  from Interpretation.Bool[of "CI T" φ True] obtain A B e d where φ: "φ = (Vx : A ⊢ e ≡ d : B)" using ii assms by auto
  from Interpretation.Equiv[of "CI T" A e d B] obtain g 
    where g1: "L⟦Vx : A ⊢ e : B⟧⇘CI T⇙ → (IMor g)" 
    and   g2: "L⟦Vx : A ⊢ d : B⟧⇘CI T⇙ → (IMor g)" using ii φ assms by auto
  have ewd: "Sig iS⇘CI T⇙ ▹ (Vx : A ⊢ e : B)" and dwd: "Sig iS⇘CI T⇙ ▹ (Vx : A ⊢ d : B)" 
    using g1 g2 Interpretation.InterpExprWellDefined[of "CI T"] ii by simp+
  have ie: "L⟦Vx : A ⊢ e : B⟧⇘CI T⇙ → (IMor [A, e, B]⇘T⇙)" using ewd CIInterp2Mor assms by simp
  have id: "L⟦Vx : A ⊢ d : B⟧⇘CI T⇙ → (IMor [A, d, B]⇘T⇙)" using dwd CIInterp2Mor assms by simp
  have "[A, e, B]⇘T⇙ = g" 
    using g1 ie ii Interpretation.Functional[of "CI T" "Vx : A ⊢ e : B" "IMor [A, e, B]⇘T⇙" "IMor g"] by simp
  moreover have "[A, d, B]⇘T⇙ = g" 
    using g2 id ii Interpretation.Functional[of "CI T" "Vx : A ⊢ d : B" "IMor [A, d, B]⇘T⇙" "IMor g"] by simp
  ultimately have "[A, e, B]⇘T⇙ = [A, d, B]⇘T⇙" by simp
  thus ?thesis using φ ewd Cl2Equiv aeq assms by simp
qed

lemma Complete: 
  assumes "ZFAxioms T" 
  and "⋀ (I :: (ZF,ZF,ZF,ZF) Interpretation) . Model I T ⟹ (L⟦φ⟧⇘I⇙ → (IBool True))" 
  shows "φ ∈ Axioms.Theory T"
proof-
  have "Model (CI T) T" using assms CIModel by simp
  thus ?thesis using CIComplete[of T φ] assms by auto
qed

end