From 27ff9d5b7a21ae54aed1c7a23a23723903ab2fa9 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <contact@haschu.me>
Date: Wed, 15 Apr 2026 15:17:51 +0200
Subject: Revert "move wip"

This reverts commit 37f7c86a7591da1233cdf1d293bf851f43c65ba1.
---
 Algebra/Derivations.lean | 237 +++++++++++++++++++++++++++++++++++
 Algebra/Semantics.lean   |  79 ++++++++++++
 Algebra/Terms.lean       | 312 +++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 628 insertions(+)
 create mode 100644 Algebra/Derivations.lean
 create mode 100644 Algebra/Semantics.lean
 create mode 100644 Algebra/Terms.lean

(limited to 'Algebra')

diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean
new file mode 100644
index 0000000..b6e5cb5
--- /dev/null
+++ b/Algebra/Derivations.lean
@@ -0,0 +1,237 @@
+import Mathlib
+import Algebra.Terms
+
+namespace NominalAlgebra
+
+section Theories
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable (sig : Signature)
+
+@[ext]
+structure Equation where
+  vars : Type
+  [vars_nominal : NominalSet 𝔸 vars]
+  left : Term 𝔸 sig vars
+  right : Term 𝔸 sig vars
+
+namespace Equation
+
+instance (eq : Equation 𝔸 sig) : NominalSet 𝔸 eq.vars :=
+  eq.vars_nominal
+
+def HasDepth
+    {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {sig : Signature}
+    (eq : Equation 𝔸 sig) (n : ℕ) : Prop :=
+  eq.left.HasDepth n ∧ eq.right.HasDepth n
+
+end Equation
+
+def UniformEquation :=
+  { eq : Equation 𝔸 sig // ∃ n, eq.HasDepth n }
+
+structure Theory where
+  sig : Signature
+  axioms : Set (UniformEquation 𝔸 sig)
+  axioms_orbitFinite : ∀ eq ∈ axioms, OrbitFinite 𝔸 eq.val.vars
+
+end Theories
+
+variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable {sig : Signature}
+
+section Helpers
+
+def UniformEquation.mk
+    (X : Type) [NominalSet 𝔸 X] {n : ℕ} (t u : TermAtDepth 𝔸 sig X n) :
+    UniformEquation 𝔸 sig :=
+  ⟨⟨X, t.val, u.val⟩, ⟨n, t.prop, u.prop⟩⟩
+
+notation:50 X " ⊢ " lhs " ≣ " rhs => UniformEquation.mk X lhs rhs
+
+end Helpers
+
+section DerivableEquations
+
+inductive Derivable (T : Theory 𝔸) : (eq : UniformEquation 𝔸 T.sig) → Prop
+  | refl {X : Type} [NominalSet 𝔸 X] {x : X} :
+      Derivable T (X ⊢ .var x ≣ .var x)
+  | symm {X : Type} [NominalSet 𝔸 X]
+      {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
+      Derivable T (X ⊢ u ≣ t) →
+      Derivable T (X ⊢ t ≣ u)
+  | trans {X : Type} [NominalSet 𝔸 X]
+      {m : ℕ} {t u v : TermAtDepth 𝔸 T.sig X m} :
+      Derivable T (X ⊢ t ≣ v) →
+      Derivable T (X ⊢ v ≣ u) →
+      Derivable T (X ⊢ t ≣ u)
+  | cong_pure {X : Type} [NominalSet 𝔸 X]
+      {f : T.sig.pure} {m : ℕ} {ts us : T.sig.pureArgs f → TermAtDepth 𝔸 T.sig X m} :
+      (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
+      Derivable T (X ⊢ .pure f ts ≣ .pure f us)
+  | cong_free {X : Type} [NominalSet 𝔸 X]
+      {a : 𝔸} {f : T.sig.free} {m : ℕ} {ts us : T.sig.freeArgs f → TermAtDepth 𝔸 T.sig X m} :
+      (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
+      Derivable T (X ⊢ .free a f ts ≣ .free a f us)
+  | cong_bound {X : Type} [NominalSet 𝔸 X]
+      {a : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} :
+      (∀ x, Derivable T (X ⊢ ts x ≣ us x)) →
+      Derivable T (X ⊢ .bound a f ts ≣ .bound a f us)
+  | ax' {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
+      {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m}
+      {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} :
+      ((Y ⊢ r ≣ s) ∈ T.axioms) →
+      (∀ (y : Y) (π : FPerm 𝔸), Derivable T (X ⊢ σ (π • y) ≣ π • (σ y))) →
+      Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s))
+  | perm {X : Type} [NominalSet 𝔸 X]
+      {a b : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} :
+      a ≠ b →
+      (∀ x, a # us x) →
+      (∀ x, Derivable T (X ⊢ ts x ≣ ⸨a, b⸩ • us x)) →
+      Derivable T (X ⊢ .bound a f ts ≣ .bound b f us)
+
+def DerivableEq (T : Theory 𝔸) (X : Type) [NominalSet 𝔸 X] (n : ℕ) :
+    Rel (TermAtDepth 𝔸 T.sig X n) (TermAtDepth 𝔸 T.sig X n) :=
+  fun t u => Derivable T (X ⊢ t ≣ u)
+
+variable {X Y : Type} [NominalSet 𝔸 X] [NominalSet 𝔸 Y]
+
+def UniformSubstitution.DerivablyEquivariant
+    (T : Theory 𝔸) {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig X Y l) : Prop :=
+  (∀ (x : X) (π : FPerm 𝔸), Derivable T (Y ⊢ σ (π • x) ≣ π • σ x))
+
+variable {T : Theory 𝔸} {n : ℕ}
+
+/-- Restated ax' rule using DerivablyEquivariant in the premiss. -/
+lemma Derivable.ax
+    {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} :
+    ((Y ⊢ r ≣ s) ∈ T.axioms) →
+    σ.DerivablyEquivariant T →
+    Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s)) := .ax'
+
+lemma Derivable.of_eq
+    {m : ℕ} {eq : UniformEquation 𝔸 T.sig} (t u : TermAtDepth 𝔸 T.sig eq.val.vars m)
+    (ht : t.val = eq.val.left := by rfl)
+    (hu : u.val = eq.val.right := by rfl) :
+    Derivable T (eq.val.vars ⊢ t ≣ u) →
+    Derivable T eq := by
+  intro hderiv
+  have heq : (eq.val.vars ⊢ t ≣ u) = eq := by
+    apply Subtype.ext; ext
+    · rfl
+    · rfl
+    · exact heq_of_eq ht
+    · exact heq_of_eq hu
+  rw [← heq]; exact hderiv
+
+lemma Derivable.equivariant_substitution
+    {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig Y X l) :
+    σ.DerivablyEquivariant T →
+    ∀ {n : ℕ} (t : TermAtDepth 𝔸 T.sig Y n) (π : FPerm 𝔸),
+      Derivable T (X ⊢ σ.apply (π • t) ≣ π • (σ.apply t)) := by
+  intro hequi n t π
+  induction' t using TermAtDepth.induction <;> expose_names
+  · apply of_eq (σ (π • x)) (π • σ x)
+    exact hequi x π
+  · apply of_eq (.pure f (σ.apply ∘ (π • ·) ∘ args)) (.pure f ((π • ·) ∘ σ.apply ∘ args))
+    apply Derivable.cong_pure
+    exact h
+  · apply of_eq (.free (π • a) f (σ.apply ∘ (π • ·) ∘ args)) (.free (π • a) f ((π • ·) ∘ σ.apply ∘ args))
+    apply Derivable.cong_free
+    exact h
+  · apply of_eq (.bound (π • a) f (σ.apply ∘ (π • ·) ∘ args)) (.bound (π • a) f ((π • ·) ∘ σ.apply ∘ args))
+    apply Derivable.cong_bound
+    exact h
+
+lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
+    ∀ (π : FPerm 𝔸), Derivable T (X ⊢ t ≣ u) → Derivable T (X ⊢ π • t ≣ π • u) := by
+  intro π
+  let rename (π : FPerm 𝔸) (eq : UniformEquation 𝔸 T.sig) : UniformEquation 𝔸 T.sig :=
+    ⟨⟨eq.val.vars, π • eq.val.left, π • eq.val.right⟩, by
+      obtain ⟨n, ⟨hn₁, hn₂⟩⟩ := eq.prop
+      let left : TermAtDepth 𝔸 T.sig eq.val.vars n := ⟨eq.val.left, hn₁⟩
+      let right : TermAtDepth 𝔸 T.sig eq.val.vars n := ⟨eq.val.right, hn₂⟩
+      use n; exact ⟨(π • left).prop, (π • right).prop⟩⟩
+  have rename_eq
+      {Y : Type} [NominalSet 𝔸 Y] {π : FPerm 𝔸} {k : ℕ}
+      {r s : TermAtDepth 𝔸 T.sig Y k} : rename π (Y ⊢ r ≣ s) = (Y ⊢ π • r ≣ π • s) := rfl
+  suffices ∀ eq, Derivable T eq → Derivable T (rename π eq) by
+    exact this (X ⊢ t ≣ u)
+  intro eq hderiv
+  induction' hderiv <;> expose_names
+  · exact .refl
+  · rw [rename_eq]
+    apply Derivable.symm
+    exact a_ih
+  · rw [rename_eq] at *
+    apply Derivable.trans
+    · exact a_ih
+    · exact a_ih_1
+  · apply of_eq (TermAtDepth.pure f ((π • ·) ∘ ts)) (TermAtDepth.pure f ((π • ·) ∘ us))
+    apply Derivable.cong_pure
+    exact a_ih
+  · apply of_eq (TermAtDepth.free (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.free (π • a) f ((π • ·) ∘ us))
+    apply Derivable.cong_free
+    exact a_ih
+  · apply of_eq (TermAtDepth.bound (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.bound (π • a) f ((π • ·) ∘ us))
+    apply Derivable.cong_bound
+    exact a_ih
+  · rw [rename_eq]
+    apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _
+    apply Derivable.trans _ (by apply equivariant_substitution; exact h_1)
+    rw [← SemigroupAction.mul_smul, ← SemigroupAction.mul_smul]
+    apply Derivable.ax
+    · exact h
+    · exact h_1
+  · apply of_eq (TermAtDepth.bound (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.bound (π • b) f ((π • ·) ∘ us))
+    apply Derivable.perm
+    · intro hcontra
+      apply π.val.injective at hcontra
+      contradiction
+    · intro x
+      show π • a # π • (us x)
+      rw [← Rel.equivariant 𝔸 NominalSet.IsFresh]
+      exact h_1 x
+    · intro x
+      show Derivable T (X_1 ⊢ π • ts x ≣ ⸨π a, π b⸩ • π • us x)
+      rw [← SemigroupAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, SemigroupAction.mul_smul]
+      exact a_ih x
+
+instance DerivableEq.instEquivariant : Rel.Equivariant 𝔸 (DerivableEq T X n) := by
+  constructor; intro t u
+  exact Derivable.equivariant
+
+@[refl]
+lemma DerivableEq.refl (t : TermAtDepth 𝔸 T.sig X n) : DerivableEq T X n t t := by
+  induction' t using TermAtDepth.induction <;> expose_names
+  · apply Derivable.refl
+  · apply Derivable.cong_pure; assumption
+  · apply Derivable.cong_free; assumption
+  · apply Derivable.cong_bound; assumption
+
+@[symm]
+lemma DerivableEq.symm {t u : TermAtDepth 𝔸 T.sig X n} :
+    DerivableEq T X n u t → DerivableEq T X n t u := by
+  intro h
+  apply Derivable.symm
+  exact h
+
+@[trans]
+lemma DerivableEq.trans {t u v : TermAtDepth 𝔸 T.sig X n} :
+    DerivableEq T X n t v → DerivableEq T X n v u → DerivableEq T X n t u := by
+  intro htv hvu
+  apply Derivable.trans
+  · exact htv
+  · exact hvu
+
+instance TermAtDepth.setoid : Setoid (TermAtDepth 𝔸 T.sig X n) where
+  r := DerivableEq T X n
+  iseqv :=
+    { refl := DerivableEq.refl
+      symm := DerivableEq.symm
+      trans := DerivableEq.trans }
+
+end DerivableEquations
+
+end NominalAlgebra
diff --git a/Algebra/Semantics.lean b/Algebra/Semantics.lean
new file mode 100644
index 0000000..13b54a0
--- /dev/null
+++ b/Algebra/Semantics.lean
@@ -0,0 +1,79 @@
+import Mathlib
+import Algebra.Terms
+import Algebra.Derivations
+
+open CategoryTheory
+
+namespace NominalAlgebra
+
+section AlgebraDefinition
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable (sig : Signature)
+
+structure Algebra where
+  carrier : ℕ → Nom 𝔸
+  pure (f : sig.pure) {m : ℕ} :
+    (sig.pureArgs f → carrier m) →ₑ[𝔸] carrier (m + sig.pureDepth f)
+  free (f : sig.free) {m : ℕ} :
+    (𝔸 × (sig.freeArgs f → carrier m)) →ₑ[𝔸] carrier (m + sig.freeDepth f)
+  bound (f : sig.bound) {m : ℕ} :
+    NameAbstraction 𝔸 (sig.boundArgs f → carrier m) →ₑ[𝔸] carrier (m + sig.boundDepth f)
+
+instance : CoeFun (Algebra 𝔸 sig) (fun _ => ℕ → Nom 𝔸) where
+  coe A := A.carrier
+
+@[ext]
+structure Algebra.Hom (A B : Algebra 𝔸 sig) where
+  toFun : (n : ℕ) → (A n →ₑ[𝔸] B n)
+  preserve_pure : ∀ (f : sig.pure) {m : ℕ} (args : sig.pureArgs f → A m),
+    toFun (m + sig.pureDepth f) (A.pure f args) = B.pure f (toFun m ∘ args)
+  preserve_free : ∀ (a : 𝔸) (f : sig.free) {m : ℕ} (args : sig.freeArgs f → A m),
+    toFun (m + sig.freeDepth f) (A.free f ⟨a, args⟩) = B.free f ⟨a, toFun m ∘ args⟩
+  preserve_bound : ∀ (a : 𝔸) (f : sig.bound) {m : ℕ} (args : sig.boundArgs f → A m),
+    toFun (m + sig.boundDepth f) (A.bound f (⟪a⟫ args)) = B.bound f (⟪a⟫ toFun m ∘ args)
+
+instance {A B : Algebra 𝔸 sig} : CoeFun (Algebra.Hom 𝔸 sig A B) (fun _ => (n : ℕ) → (A n →ₑ[𝔸] B n)) where
+  coe h := h.toFun
+
+end AlgebraDefinition
+
+section Algebra
+
+variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable {sig : Signature}
+
+namespace Algebra
+
+def Hom.id (A : Algebra 𝔸 sig) : Hom 𝔸 sig A A where
+  toFun _ := EquivariantMap.id 𝔸
+  preserve_pure _ _ _ := rfl
+  preserve_free _ _ _ _ := rfl
+  preserve_bound _ _ _ _ := rfl
+
+def Hom.comp {A B C : Algebra 𝔸 sig} (h : Hom 𝔸 sig B C) (g : Hom 𝔸 sig A B) : Hom 𝔸 sig A C where
+  toFun n := EquivariantMap.comp 𝔸 (h n) (g n)
+  preserve_pure f m args := by
+    rw [EquivariantMap.comp_app, g.preserve_pure, h.preserve_pure]
+    rfl
+  preserve_free a f m args := by
+    rw [EquivariantMap.comp_app, g.preserve_free, h.preserve_free]
+    rfl
+  preserve_bound a f m args := by
+    rw [EquivariantMap.comp_app, g.preserve_bound, h.preserve_bound]
+    rfl
+
+instance : Category (Algebra 𝔸 sig) where
+  Hom := Hom 𝔸 sig
+  id := Hom.id
+  comp h g := Hom.comp g h
+
+def forgetfulFunctor : Algebra 𝔸 sig ⥤ Nom 𝔸 where
+  obj X := X 0
+  map f := f.toFun 0
+
+end Algebra
+
+end Algebra
+
+end NominalAlgebra
diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean
new file mode 100644
index 0000000..568f5cb
--- /dev/null
+++ b/Algebra/Terms.lean
@@ -0,0 +1,312 @@
+import Mathlib
+import Nominal
+
+namespace NominalAlgebra
+
+section Definitions
+
+/-- A graded signature. -/
+structure Signature where
+  pure : Type
+  free : Type
+  bound : Type
+  /-- Type representing the arguments required for an operation. -/
+  args : pure ⊕ free ⊕ bound → Type
+  args_fintype : ∀ f, Fintype (args f) := by intro; infer_instance
+  /-- Depth of an operation. -/
+  depth : pure ⊕ free ⊕ bound → ℕ
+
+def Signature.pureArgs (sig : Signature) (f : sig.pure) : Type := sig.args (.inl f)
+def Signature.freeArgs (sig : Signature) (f : sig.free) : Type := sig.args (.inr (.inl f))
+def Signature.boundArgs (sig : Signature) (f : sig.bound) : Type := sig.args (.inr (.inr f))
+
+instance Signature.instPureArgsFintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f)
+instance Signature.instFreeArgsFintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f))
+instance Signature.instBoundArgsFintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f))
+
+def Signature.arity (sig : Signature) (f : sig.pure ⊕ sig.free ⊕ sig.bound) : ℕ := (sig.args_fintype f).card
+def Signature.pureArity (sig : Signature) (f : sig.pure) : ℕ := sig.arity (.inl f)
+def Signature.freeArity (sig : Signature) (f : sig.free) : ℕ := sig.arity (.inr (.inl f))
+def Signature.boundArity (sig : Signature) (f : sig.bound) : ℕ := sig.arity (.inr (.inr f))
+
+def Signature.pureDepth (sig : Signature) (f : sig.pure) : ℕ := sig.depth (.inl f)
+def Signature.freeDepth (sig : Signature) (f : sig.free) : ℕ := sig.depth (.inr (.inl f))
+def Signature.boundDepth (sig : Signature) (f : sig.bound) : ℕ := sig.depth (.inr (.inr f))
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable (sig : Signature)
+
+inductive Term (X : Type) [NominalSet 𝔸 X]
+  | var (x : X) : Term X
+  | pure (f : sig.pure) (args : sig.pureArgs f → Term X) : Term X
+  | free (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → Term X) : Term X
+  | bound (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → Term X) : Term X
+
+inductive Term.HasDepth
+    {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+    {sig : Signature}
+    {X : Type} [NominalSet 𝔸 X]
+    : Term 𝔸 sig X → ℕ → Prop
+  | var (x : X) : HasDepth (.var x) 0
+  | pure (f : sig.pure) (args : sig.pureArgs f → Term 𝔸 sig X) (k : ℕ) :
+      (∀ arg : sig.pureArgs f, HasDepth (args arg) k) → HasDepth (.pure f args) (k + sig.pureDepth f)
+  | free (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → Term 𝔸 sig X) (k : ℕ) :
+      (∀ arg : sig.freeArgs f, HasDepth (args arg) k) → HasDepth (.free a f args) (k + sig.freeDepth f)
+  | bound (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → Term 𝔸 sig X) (k : ℕ) :
+      (∀ arg : sig.boundArgs f, HasDepth (args arg) k) → HasDepth (.bound a f args) (k + sig.boundDepth f)
+
+def TermAtDepth (X : Type) [NominalSet 𝔸 X] (n : ℕ) :=
+  { t : Term 𝔸 sig X // t.HasDepth n }
+
+def Substitution (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] :=
+  X → Term 𝔸 sig Y
+
+def UniformSubstitution (X : Type) [NominalSet 𝔸 X] (Y : Type) [NominalSet 𝔸 Y] (l : ℕ) :=
+  X → TermAtDepth 𝔸 sig Y l
+
+end Definitions
+
+variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable {sig : Signature}
+variable {X : Type} [NominalSet 𝔸 X]
+variable {Y : Type} [NominalSet 𝔸 Y]
+
+section ConvenienceConstructors
+
+def TermAtDepth.var (x : X) : TermAtDepth 𝔸 sig X 0 := ⟨.var x, by constructor⟩
+
+def TermAtDepth.pure {n : ℕ} (f : sig.pure) (args : sig.pureArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.pureDepth f) :=
+  ⟨.pure f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
+def TermAtDepth.free {n : ℕ} (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.freeDepth f) :=
+  ⟨.free a f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
+def TermAtDepth.bound {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig X (n + sig.boundDepth f) :=
+  ⟨.bound a f (Subtype.val ∘ args), by constructor; intro arg; exact (args arg).prop⟩
+
+theorem TermAtDepth.induction
+  {motive : {n : ℕ} → TermAtDepth 𝔸 sig X n → Prop}
+  (var : ∀ (x : X), motive (.var x))
+  (pure : ∀ {n : ℕ} (f : sig.pure) (args : sig.pureArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.pure f args))
+  (free : ∀ {n : ℕ} (a : 𝔸) (f : sig.free) (args : sig.freeArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.free a f args))
+  (bound : ∀ {n : ℕ} (a : 𝔸) (f : sig.bound) (args : sig.boundArgs f → TermAtDepth 𝔸 sig X n),
+    (∀ x, motive (args x)) → motive (.bound a f args))
+  : ∀ {n : ℕ} (t : TermAtDepth 𝔸 sig X n), motive t := by
+  intro n ⟨t, ht⟩
+  induction' t generalizing n <;> cases ht <;> expose_names
+  · exact var x
+  · let args' : sig.pureArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact pure f args' args_ih'
+  · let args' : sig.freeArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact free a f args' args_ih'
+  · let args' : sig.boundArgs f → TermAtDepth 𝔸 sig X k := fun x => ⟨args x, h x⟩
+    have args_ih' : ∀ x, motive (args' x) := fun x => args_ih x (h x)
+    exact bound a f args' args_ih'
+
+end ConvenienceConstructors
+
+section Substitution
+
+def Substitution.apply (σ : Substitution 𝔸 sig X Y) : Term 𝔸 sig X → Term 𝔸 sig Y
+  | .var x => σ x
+  | .pure f args => .pure f (fun x => σ.apply (args x))
+  | .free a f args => .free a f (fun x => σ.apply (args x))
+  | .bound a f args => .bound a f (fun x => σ.apply (args x))
+
+@[simp] lemma Substitution.apply_var {x : X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply (.var x) = (σ x) := rfl
+
+@[simp] lemma Substitution.apply_pure
+    {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply (.pure f args) = .pure f (σ.apply ∘ args) := rfl
+
+@[simp] lemma Substitution.apply_free
+    {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply (.free a f args) = .free a f (σ.apply ∘ args) := rfl
+
+@[simp] lemma Substitution.apply_bound
+    {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → Term 𝔸 sig X} {σ : Substitution 𝔸 sig X Y} :
+    σ.apply (.bound a f args) = .bound a f (σ.apply ∘ args) := rfl
+
+def UniformSubstitution.toSubstitution {l : ℕ} (σ : UniformSubstitution 𝔸 sig X Y l) : Substitution 𝔸 sig X Y :=
+  fun x => (σ x).val
+
+def UniformSubstitution.apply {n l : ℕ} (σ : UniformSubstitution 𝔸 sig X Y l) (t : TermAtDepth 𝔸 sig X n) :
+    TermAtDepth 𝔸 sig Y (n + l) :=
+  ⟨σ.toSubstitution.apply t.val, by
+    suffices ∀ t n, t.HasDepth n → (σ.toSubstitution.apply t).HasDepth (n + l) by
+      exact this t.val n t.prop
+    intro t; fun_induction Substitution.apply
+    · intro n h; cases h
+      rw [Nat.zero_add]
+      exact (σ _).prop
+    all_goals
+      intro n h; cases h; expose_names
+      rw [Nat.add_right_comm]
+      constructor; intro arg
+      apply ih1; exact h arg⟩
+
+@[simp] lemma UniformSubstitution.apply_var
+    {x : X} {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply (.var x)).val = (σ x).val := rfl
+
+@[simp] lemma UniformSubstitution.apply_pure
+    {n : ℕ} {f : sig.pure} {args : sig.pureArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply (.pure f args)).val = (TermAtDepth.pure f (σ.apply ∘ args)).val := rfl
+
+@[simp] lemma UniformSubstitution.apply_free
+    {n : ℕ} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply (.free a f args)).val = (TermAtDepth.free a f (σ.apply ∘ args)).val := rfl
+
+@[simp] lemma UniformSubstitution.apply_bound
+    {n : ℕ} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → TermAtDepth 𝔸 sig X n}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 sig X Y l} :
+    (σ.apply (.bound a f args)).val = (TermAtDepth.bound a f (σ.apply ∘ args)).val := rfl
+
+end Substitution
+
+section NominalSet
+
+namespace Term
+
+private def rename (π : FPerm 𝔸) : Term 𝔸 sig X → Term 𝔸 sig X
+  | .var x => .var (π • x)
+  | .pure f args => .pure f (fun x => rename π (args x))
+  | .free a f args => .free (π • a) f (fun x => rename π (args x))
+  | .bound a f args => .bound (π • a) f (fun x => rename π (args x))
+
+private lemma one_rename (t : Term 𝔸 sig X) : t.rename 1 = t := by
+  induction' t <;> all_goals simp [rename, *]
+
+private lemma mul_rename (π τ : FPerm 𝔸) (t : Term 𝔸 sig X) :
+    t.rename (π * τ) = (t.rename τ).rename π := by
+  induction' t <;> all_goals simp [rename, mul_smul, *]
+
+instance : PermSet 𝔸 (Term 𝔸 sig X) where
+  smul := rename
+  one_smul := one_rename
+  mul_smul := mul_rename
+
+@[simp] lemma smul_var {π : FPerm 𝔸} {x : X} :
+    π • (.var x : Term 𝔸 sig X) = .var (π • x) := rfl
+
+@[simp] lemma smul_pure {π : FPerm 𝔸} {f : sig.pure} {args : sig.pureArgs f → Term 𝔸 sig X} :
+    π • Term.pure f args = .pure f ((π • ·) ∘ args) := rfl
+
+@[simp] lemma smul_free {π : FPerm 𝔸} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → Term 𝔸 sig X} :
+    π • Term.free a f args = .free (π • a) f ((π • ·) ∘ args) := rfl
+
+@[simp] lemma smul_bound {π : FPerm 𝔸} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → Term 𝔸 sig X} :
+    π • Term.bound a f args = .bound (π • a) f ((π • ·) ∘ args) := rfl
+
+private def atoms : Term 𝔸 sig X → Set 𝔸
+  | .var x => NominalSet.supp 𝔸 x
+  | .pure f args => ⋃₀ {(args x).atoms | x : sig.pureArgs f}
+  | .free a f args => {a} ∪ ⋃₀ {(args x).atoms | x : sig.freeArgs f}
+  | .bound a f args => {a} ∪ ⋃₀ {(args x).atoms | x : sig.boundArgs f}
+
+private lemma atoms_finite (t : Term 𝔸 sig X) : t.atoms.Finite := by
+  fun_induction atoms <;> all_goals expose_names
+  · exact NominalSet.supp_finite 𝔸
+  · apply Set.Finite.sUnion
+    · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+      apply Set.finite_range
+    · intro S ⟨x, hS⟩
+      rw [← hS]
+      exact ih1 x
+  all_goals
+    apply Set.Finite.union
+    · exact Set.finite_singleton a
+    · apply Set.Finite.sUnion
+      · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range]
+        apply Set.finite_range
+      · intro S ⟨x, hS⟩
+        rw [← hS]
+        exact ih1 x
+
+private lemma atoms_support (t : Term 𝔸 sig X) : PermSet.HasSupport 𝔸 t t.atoms := by
+  intro π
+  fun_induction atoms <;> all_goals expose_names
+  · have hsupp : PermSet.HasSupport 𝔸 x (NominalSet.supp 𝔸 x) := NominalSet.supp_is_support 𝔸
+    intro hπ
+    simp only [PermSet.fix', smul_var, Term.var.injEq, Set.mem_setOf_eq]
+    exact hsupp hπ
+  · intro hπ
+    simp only [PermSet.fix', smul_pure, Term.pure.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq]
+    ext x
+    rw [Function.comp_apply]
+    apply ih1
+    apply PermSet.fix_antitone_mem 𝔸 hπ
+    apply Set.subset_sUnion_of_mem
+    use x
+  all_goals
+    intro hπ
+    simp only [PermSet.fix', smul_free, smul_bound, Term.free.injEq, Term.bound.injEq, heq_eq_eq,
+      true_and, Set.mem_setOf_eq]
+    constructor
+    · apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_left
+      rfl
+    · ext x
+      rw [Function.comp_apply]
+      apply ih1
+      apply PermSet.fix_antitone_mem 𝔸 hπ
+      apply Set.subset_union_of_subset_right
+      apply Set.subset_sUnion_of_mem
+      use x
+
+instance : NominalSet 𝔸 (Term 𝔸 sig X) where
+  fin_supp t := by
+    use t.atoms
+    exact ⟨t.atoms_support, t.atoms_finite⟩
+
+instance instHasDepthEquivariant {n : ℕ} :
+    Set.Equivariant 𝔸 {t : Term 𝔸 sig X | t.HasDepth n} := by
+  constructor; intro t π ht
+  suffices ∀ (t : Term 𝔸 sig X) n, t.HasDepth n → (t.rename π).HasDepth n by
+    exact this t n ht
+  intro t; fun_induction rename
+  · intro n h; cases h; constructor
+  all_goals
+      intro n h; cases h
+      expose_names
+      constructor; intro arg
+      apply ih1; exact h arg
+
+end Term
+
+namespace TermAtDepth
+
+instance {n : ℕ} : NominalSet 𝔸 (TermAtDepth 𝔸 sig X n) :=
+  (Subtype.instNominalSetElem 𝔸 : NominalSet 𝔸 {t : Term 𝔸 sig X | t.HasDepth n})
+
+@[simp] lemma smul_var
+    {π : FPerm 𝔸} {x : X} :
+    (π • (.var x : TermAtDepth 𝔸 sig X 0)).val = (TermAtDepth.var (π • x)).val := rfl
+
+@[simp] lemma smul_pure
+    {π : FPerm 𝔸} {n : ℕ} {f : sig.pure} {args : sig.pureArgs f → TermAtDepth 𝔸 sig X n} :
+    (π • TermAtDepth.pure f args).val = (TermAtDepth.pure f ((π • ·) ∘ args)).val := rfl
+
+@[simp] lemma smul_free
+    {π : FPerm 𝔸} {n : ℕ} {a : 𝔸} {f : sig.free} {args : sig.freeArgs f → TermAtDepth 𝔸 sig X n} :
+    (π • TermAtDepth.free a f args).val = (TermAtDepth.free (π • a) f ((π • ·) ∘ args)).val := rfl
+
+@[simp] lemma smul_bound
+    {π : FPerm 𝔸} {n : ℕ} {a : 𝔸} {f : sig.bound} {args : sig.boundArgs f → TermAtDepth 𝔸 sig X n} :
+    (π • TermAtDepth.bound a f args).val = (TermAtDepth.bound (π • a) f ((π • ·) ∘ args)).val := rfl
+
+end TermAtDepth
+
+end NominalSet
+
+end NominalAlgebra
-- 
cgit v1.3.1