From 8fdf459876b999dbe184196f9abd330a3c24d560 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 4 Dec 2025 17:14:46 +0100
Subject: implement derivable equality

---
 Nominal/Instances/Basic.lean | 15 +++++++++++++++
 Nominal/Permutations.lean    | 17 +++++++++++++++++
 2 files changed, 32 insertions(+)

(limited to 'Nominal')

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index dcca75b..64b6425 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -70,6 +70,21 @@ def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
     · intro π hπ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl
     · exact Set.finite_empty
 
+instance {X : Type} [NominalSet.Discrete 𝔸 X] [Finite X] : OrbitFinite 𝔸 X where
+  fin_orbits := Finite.of_equiv X
+    { toFun x := Quotient.mk _ x
+      invFun x := x.out
+      left_inv x := by
+        suffices ∀ (x y : X), MulAction.orbitRel (FPerm 𝔸) X x y → x = y by
+          apply this
+          rw [← Quotient.eq]
+          apply Quotient.out_eq
+        intro x y ⟨π, hπ⟩
+        simp only [NominalSet.Discrete.is_discrete] at hπ
+        exact hπ.symm
+      right_inv x := by simp
+    }
+
 @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 79a5042..0a4974a 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -187,12 +187,29 @@ class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
+/-- An (FPerm 𝔸)-set is orbit-finite if there are only finitely many different orbits. -/
+class OrbitFinite (X : Type) [PermSet 𝔸 X] where
+  fin_orbits : Finite (Quotient (MulAction.orbitRel (FPerm 𝔸) X))
+
 /-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 𝔸 where
   smul π a := π a
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
 
+instance : OrbitFinite 𝔸 𝔸 where
+  fin_orbits := Finite.of_equiv Unit
+    { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some
+      invFun _ := ()
+      right_inv := by
+        let chosen := (inferInstanceAs (Nonempty 𝔸)).some
+        apply Quotient.ind; intro a
+        rw [Quotient.eq]
+        show chosen ∈ MulAction.orbit (FPerm 𝔸) a
+        use ⸨chosen, a⸩
+        exact FPerm.swap_apply_right chosen a
+    }
+
 /-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 (FPerm 𝔸) where
   smul π τ := π * τ
-- 
cgit v1.3.1