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/Permutations.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'Nominal/Permutations.lean')

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