work on gsets category

Algebra/GSet.agda

@@ -3,7 +3,7 @@ open import Level
 open import Data.Product
 open import Relation.Binary.PropositionalEquality
 
-module GSet {c ℓ : Level} where
+module Algebra.GSet {c ℓ : Level} where
   open Group using () renaming (Carrier to ∣_∣)
   record G-Set (G : Group c ℓ) : Set (suc (c ⊔ ℓ)) where
     open Group G using (ε; _∙_)
@@ -24,5 +24,5 @@ module GSet {c ℓ : Level} where
 
   record G-Set-Morphism (G : Group c ℓ) (X Y : G-Set G) : Set (suc (c ⊔ ℓ)) where
     field
-      f : ∣ X ∣ → ∣ Y ∣
+      u : ∣ X ∣ → ∣ Y ∣ -- u for underlying
-      isEqui : isEquivariant X Y f
+      isEqui : isEquivariant X Y u

Category/GSets.agda

@@ -1,2 +1,33 @@
 open import Algebra.Bundles
+open import Algebra.GSet
+open import Categories.Category.Core
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Level
+
+module Category.GSets {c ℓ : Level} where
+  open Category
+  G-Sets : Group c ℓ → Category (suc (c ⊔ ℓ)) (suc c ⊔ suc ℓ) c
+  G-Sets G .Obj = G-Set G
+  G-Sets G ._⇒_ = G-Set-Morphism G
+  G-Sets G ._≈_ f g = ∀ {x} → f.u x ≡ g.u x
+    where
+      module f = G-Set-Morphism f
+      module g = G-Set-Morphism g
+  G-Sets G .id = record { u = λ x → x ; isEqui = ≡.refl }
+  G-Sets G ._∘_ f g .G-Set-Morphism.u x = f.u (g.u x)
+    where
+      module f = G-Set-Morphism f
+      module g = G-Set-Morphism g
+  -- TODO without rewrite
+  G-Sets G ._∘_ {X} {Y} {Z} f g .G-Set-Morphism.isEqui {h} {x} rewrite G-Set-Morphism.isEqui g {h} {x} | G-Set-Morphism.isEqui f {h} {G-Set-Morphism.u g x} = ≡.refl
+    where
+      module f = G-Set-Morphism f
+      module g = G-Set-Morphism g
+  G-Sets G .assoc = ≡.refl
+  G-Sets G .sym-assoc = ≡.refl
+  G-Sets G .identityˡ = ≡.refl
+  G-Sets G .identityʳ = ≡.refl
+  G-Sets G .identity² = ≡.refl
+  G-Sets G .equiv = record { refl = ≡.refl ; sym = λ eq → ≡.sym eq ; trans = λ eq₁ eq₂ → ≡.trans eq₁ eq₂ }
+  G-Sets G .∘-resp-≈ {X} {Y} {Z} {f} {h} {g} {i} f≈h g≈i = ≡.trans f≈h (≡.cong < h > g≈i)
+    where open G-Set-Morphism using () renaming (u to <_>)