From b3f26f306945ec9e391140f1645012ba11decb40 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Mon, 27 Oct 2025 21:58:56 +0100
Subject: quotient types as nominal sets

---
 Nominal/Instances/Basic.lean | 70 ++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 67 insertions(+), 3 deletions(-)

(limited to 'Nominal/Instances/Basic.lean')

diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index 2bb389d..2ebe9b1 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -59,7 +59,7 @@ Every set can be made into a discrete nominal set, where supp x = ∅.
 -/
 section Discrete
 
-def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
+def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
   smul π x := x
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
@@ -81,10 +81,10 @@ def NominalSet.discrete (X : Type) : NominalSet.Discrete 𝔸 X where
   simp [IsFresh]
 
 /-- We consider Unit a discrete nominal set. -/
-instance : NominalSet.Discrete 𝔸 Unit := NominalSet.discrete 𝔸 Unit
+instance : NominalSet.Discrete 𝔸 Unit := NominalSet.mkDiscrete 𝔸 Unit
 
 /-- We consider Bool a discrete nominal set. -/
-instance : NominalSet.Discrete 𝔸 Bool := NominalSet.discrete 𝔸 Bool
+instance : NominalSet.Discrete 𝔸 Bool := NominalSet.mkDiscrete 𝔸 Bool
 
 end Discrete
 
@@ -221,3 +221,67 @@ lemma inr_equivariant : Equivariant 𝔸 (Sum.inr : Y → X ⊕ Y) := by
 end Sum
 
 end Coproducts
+
+/-!
+## Quotient Types
+
+If ≈ is an equivariant relation on X × X, then X/≈ is a nominal set with `supp [x] = ⋂₀ {supp y | y ∈ [x]}`.
+-/
+section Quotient
+
+namespace Quotient
+
+variable {X : Type} [PermSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+
+instance : SMul (FPerm 𝔸) (Quotient setoid.toSetoid) where
+  smul π := Quotient.lift (fun x => ⟦π • x⟧) (by
+    intro x y hxy
+    simp only [Quotient.eq]
+    apply setoid.equivariant x y π hxy)
+
+@[simp] lemma smul_quotient (π : FPerm 𝔸) (x : X) : (π • Quotient.mk setoid.toSetoid x) = ⟦π • x⟧ := rfl
+
+instance : PermSet 𝔸 (Quotient setoid.toSetoid) where
+  one_smul := by
+    apply Quotient.ind
+    intro x
+    simp
+  mul_smul := by
+    intro π τ
+    apply Quotient.ind
+    simp [mul_smul]
+
+lemma mk_equivariant : Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by
+  simp [Equivariant]
+
+variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X}
+
+instance : NominalSet 𝔸 (Quotient setoid.toSetoid) :=
+  NominalSet.fromEquivariantSurjective 𝔸 (Quotient.mk setoid.toSetoid) (mk_equivariant 𝔸) mk_surjective
+
+lemma supp {x : X} : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x) = {a | ∀ (x' : X), x' ≈ x → a ∈ NominalSet.supp 𝔸 x'} := by
+  ext a
+  constructor
+  · intro ha x' hx'
+    rw [← Quotient.sound hx'] at ha
+    have hsub : NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x') ⊆ NominalSet.supp 𝔸 x' :=
+      Equivariant.supp_subset 𝔸 (mk_equivariant 𝔸)
+    exact hsub ha
+  · contrapose; intro ha
+    simp only [Set.mem_setOf_eq, Classical.not_imp, not_forall]
+    have hfin₁ : (NominalSet.supp 𝔸 (Quotient.mk setoid.toSetoid x)).Finite := NominalSet.supp_finite 𝔸
+    have hfin₂ : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸
+    -- Show that we can find a fresh c for which (a c) • ⟦x⟧ = ⟦x⟧
+    obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin₁.toFinset ∪ hfin₂.toFinset)
+    simp only [Finset.mem_union, Set.Finite.mem_toFinset, not_or] at hc
+    use ⸨a, c⸩ • x; constructor
+    · apply Quotient.exact
+      rw [← smul_quotient]
+      exact NominalSet.fresh_swap_fix 𝔸 ha hc.left
+    · rw [NominalSet.supp_equivariant, Set.mem_smul_set_iff_inv_smul_mem]
+      simp only [FPerm.swap_inv, PermSet.atom_swap, Equiv.swap_apply_left]
+      exact hc.right
+
+end Quotient
+
+end Quotient
-- 
cgit v1.3.1