implement derivable equality

1 files changed, 17 insertions, 0 deletions

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 π τ := π * τ