From b3f26f306945ec9e391140f1645012ba11decb40 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Mon, 27 Oct 2025 21:58:56 +0100 Subject: quotient types as nominal sets --- Nominal/Equivariance.lean | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Nominal/Equivariance.lean') diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 189ca66..0fe9f91 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -31,6 +31,10 @@ def EquivariantSet (S : Set X) : Prop := def EquivariantRelation (R : Rel X Y) : Prop := ∀ (x : X) (y : Y) (π : FPerm 𝔸), R x y → R (π • x) (π • y) +/-- Extended setoid definition that also requires the relation to be equivariant. -/ +class EquivariantSetoid (X : Type) [PermSet 𝔸 X] extends Setoid X where + equivariant : EquivariantRelation 𝔸 r + /-- For equivariant sets, we even have "if and only if". -/ lemma equivariant_set_iff {S : Set X} : EquivariantSet 𝔸 S ↔ ∀ (x : X) (π : FPerm 𝔸), x ∈ S ↔ π • x ∈ S := by constructor -- cgit v1.3.1