commit 12e3092a1779d41507e1eb4a3fe867fc716673af
Author: Leon Vatthauer <leon.vatthauer@fau.de>
Date:   Sat May 4 14:15:13 2024 +0200

    initial

diff --git a/Algebra/GSet.agda b/Algebra/GSet.agda
new file mode 100644
index 0000000..14004a9
--- /dev/null
+++ b/Algebra/GSet.agda
@@ -0,0 +1,28 @@
+open import Algebra.Bundles
+open import Level
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+
+module GSet {c ℓ : Level} where
+  open Group using () renaming (Carrier to ∣_∣)
+  record G-Set (G : Group c ℓ) : Set (suc (c ⊔ ℓ)) where
+    open Group G using (ε; _∙_)
+    field
+      X : Set c
+      _⊳_ : ∣ G ∣ → X → X
+    field
+      ε⊳ : ∀ {x : X} → ε ⊳ x ≡ x
+      ∘⊳ : ∀ {g h : ∣ G ∣} {x : X} → (g ∙ h) ⊳ x ≡ (g ⊳ (h ⊳ x))
+
+  open G-Set using () renaming (X to ∣_∣)
+
+  isEquivariant : ∀ {G : Group c ℓ} (X Y : G-Set G) (f : ∣ X ∣ → ∣ Y ∣) → Set c
+  isEquivariant {G} X Y f = ∀ {g : ∣ G ∣} {x : ∣ X ∣} → f (g ⊳ˣ x) ≡ g ⊳ʸ (f x)
+    where
+      open G-Set X using () renaming (_⊳_ to _⊳ˣ_)
+      open G-Set Y using () renaming (_⊳_ to _⊳ʸ_)
+
+  record G-Set-Morphism (G : Group c ℓ) (X Y : G-Set G) : Set (suc (c ⊔ ℓ)) where
+    field
+      f : ∣ X ∣ → ∣ Y ∣
+      isEqui : isEquivariant X Y f
diff --git a/Category/GSets.agda b/Category/GSets.agda
new file mode 100644
index 0000000..4fcd00f
--- /dev/null
+++ b/Category/GSets.agda
@@ -0,0 +1,2 @@
+open import Algebra.Bundles
+open import Level
diff --git a/gset.agda-lib b/gset.agda-lib
new file mode 100644
index 0000000..f075a25
--- /dev/null
+++ b/gset.agda-lib
@@ -0,0 +1,3 @@
+name: gset
+include: .
+depend: agda-categories standard-library