diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index dea5bcf..7f461ac 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -254,6 +254,13 @@ instance : PermSet 𝔸 (Quotient setoid.toSetoid) where lemma mk_equivariant : Function.Equivariant 𝔸 (Quotient.mk setoid.toSetoid) := by simp [Function.Equivariant] +lemma lift_equivariant + {Y : Type} [PermSet 𝔸 Y] (f : X → Y) (h : ∀ (a b : X), a ≈ b → f a = f b) : + Function.Equivariant 𝔸 f → Function.Equivariant 𝔸 (Quotient.lift f h) := by + intro hequi x π + obtain ⟨x', hx'⟩ := x.exists_rep + simp [← hx', hequi x' π] + variable {X : Type} [NominalSet 𝔸 X] {setoid : EquivariantSetoid 𝔸 X} instance : NominalSet 𝔸 (Quotient setoid.toSetoid) := |