diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..491bb09
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.agdai
+_build/
diff --git a/Algebra/G-Set.agda b/Algebra/G-Set.agda
new file mode 100644
index 0000000..30ed6c8
--- /dev/null
+++ b/Algebra/G-Set.agda
@@ -0,0 +1,45 @@
+open import Algebra.Group
+open import Level
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+
+module Algebra.G-Set {ℓ : Level} where
+  open Group using () renaming (Carrier to ∣_∣)
+  record G-Set (G : Group ℓ) : Set (suc ℓ) where
+    open Group G using (ε; _∙_)
+    field
+      X : Set ℓ
+      _⊳_ : ∣ G ∣ → X → X
+    field
+      ε⊳ : ∀ {x : X} → ε ⊳ x ≡ x
+      ∘⊳ : ∀ {g h : ∣ G ∣} {x : X} → (g ∙ h) ⊳ x ≡ (g ⊳ (h ⊳ x))
+
+    orb : X → Set ℓ
+    orb x = Σ[ y ∈ X ] Σ[ g ∈ ∣ G ∣ ] g ⊳ x ≡ y
+
+    Orb : Set ℓ
+    Orb = Σ[ x ∈ X ] orb x
+
+    -- record orb (x : X) : Set ℓ where
+    --   field
+    --     y : X
+    --     g : ∣ G ∣
+    --     .eq : g ⊳ x ≡ y
+
+    -- record Orb : Set ℓ where
+    --   field
+    --     x : X
+    --     O : orb x
+
+  open G-Set using () renaming (X to ∣_∣)
+
+  IsEquivariant : ∀ {G : Group ℓ} (X Y : G-Set G) (f : ∣ X ∣ → ∣ Y ∣) → Set ℓ
+  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 ℓ) (X Y : G-Set G) : Set (suc ℓ) where
+    field
+      u : ∣ X ∣ → ∣ Y ∣ -- u for underlying
+      equivariance : IsEquivariant X Y u
diff --git a/Algebra/GSet.agda b/Algebra/GSet.agda
deleted file mode 100644
index 629c2e6..0000000
--- a/Algebra/GSet.agda
+++ /dev/null
@@ -1,28 +0,0 @@
-open import Algebra.Bundles
-open import Level
-open import Data.Product
-open import Relation.Binary.PropositionalEquality
-
-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 (ε; _∙_)
-    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
-      u : ∣ X ∣ → ∣ Y ∣ -- u for underlying
-      isEqui : isEquivariant X Y u
diff --git a/Algebra/Group.agda b/Algebra/Group.agda
new file mode 100644
index 0000000..e9af653
--- /dev/null
+++ b/Algebra/Group.agda
@@ -0,0 +1,27 @@
+open import Level
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+module Algebra.Group where
+  record IsGroup {ℓ} (A : Set ℓ) (_∙_ : A → A → A) (ε : A) (_⁻¹ : A → A) : Set (suc ℓ) where
+    field
+      assoc : ∀ {f g h : A} → (f ∙ g) ∙ h ≡ f ∙ (g ∙ h)
+      idˡ : ∀ {g : A} → ε ∙ g ≡ g
+      idʳ : ∀ {g : A} → g ∙ ε ≡ g
+      invˡ : ∀ {g : A} → g ∙ (g ⁻¹) ≡ ε
+      invʳ : ∀ {g : A} → (g ⁻¹) ∙ g ≡ ε
+
+  record Group (ℓ : Level) : Set (suc ℓ) where
+    infix 8 _⁻¹
+    infixl 7 _∙_
+    field
+      Carrier : Set ℓ
+      _∙_ : Carrier → Carrier → Carrier
+      ε : Carrier
+      _⁻¹ : Carrier → Carrier
+
+    field
+      isGroup : IsGroup Carrier _∙_ ε _⁻¹
+    open IsGroup isGroup public
+
+    ∙-resp : ∀ {f h g i : Carrier} → f ≡ h → g ≡ i → f ∙ g ≡ h ∙ i
+    ∙-resp {f} {h} {g} {i} f≡h g≡i = ≡.trans (≡.cong (f ∙_) g≡i) (≡.cong (_∙ i) f≡h)
diff --git a/Category/Construction/GroupAsCategory.agda b/Category/Construction/GroupAsCategory.agda
new file mode 100644
index 0000000..76b34b4
--- /dev/null
+++ b/Category/Construction/GroupAsCategory.agda
@@ -0,0 +1,27 @@
+open import Categories.Category.Core
+open import Algebra.Group
+open import Data.Unit.Polymorphic
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+module Category.Construction.GroupAsCategory {ℓ} (G : Group ℓ) where
+  open Group G
+
+  GroupAsCategory : Category ℓ ℓ ℓ
+  GroupAsCategory = record
+                     { Obj = ⊤
+                     ; _⇒_ = λ _ _ → Carrier
+                     ; _≈_ = _≡_
+                     ; id = ε
+                     ; _∘_ = _∙_
+                     ; assoc = assoc
+                     ; sym-assoc = ≡.sym assoc
+                     ; identityˡ = idˡ
+                     ; identityʳ = idʳ
+                     ; identity² = idˡ
+                     ; equiv = record
+                       { refl = ≡.refl
+                       ; sym = ≡.sym
+                       ; trans = ≡.trans
+                       }
+                     ; ∘-resp-≈ = ∙-resp
+                     }
diff --git a/Category/G-Sets.agda b/Category/G-Sets.agda
new file mode 100644
index 0000000..8ab736e
--- /dev/null
+++ b/Category/G-Sets.agda
@@ -0,0 +1,38 @@
+open import Algebra.Group
+open import Algebra.G-Set
+open import Categories.Category.Core
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Level
+
+module Category.G-Sets {ℓ : Level} where
+  open Category
+  open G-Set-Morphism using () renaming (u to <_>)
+  G-Sets : Group ℓ → Category (suc ℓ) (suc ℓ) ℓ
+  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
+    ; equivariance = ≡.refl
+    }
+  G-Sets G ._∘_ f g = record
+    { u = λ x → f.u (g.u x)
+    ; equivariance = ≡.trans (≡.cong < f > g.equivariance) f.equivariance
+    }
+    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)
diff --git a/Category/G-Sets/Properties/A4.agda b/Category/G-Sets/Properties/A4.agda
new file mode 100644
index 0000000..cc0a457
--- /dev/null
+++ b/Category/G-Sets/Properties/A4.agda
@@ -0,0 +1,46 @@
+open import Algebra.G-Set
+open import Algebra.Group
+open import Category.G-Sets
+open import Categories.Category.Instance.Sets
+open import Categories.Functor.Core
+open import Categories.Category.Core
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Relation.Binary.PropositionalEquality.WithK
+open import Axiom.UniquenessOfIdentityProofs.WithK
+open import Data.Product
+open import Data.Product.Properties renaming (Σ-≡,≡→≡ to peq)
+open import Level
+
+module Category.G-Sets.Properties.A4 {ℓ} (G : Group ℓ) where
+  open Functor
+  open G-Set-Morphism using () renaming (u to <_>)
+  D : Functor (Sets ℓ) (G-Sets G)
+  D .F₀ S = record
+    { X = S
+    ; _⊳_ = λ _ s → s
+    ; ε⊳ = ≡.refl
+    ; ∘⊳ = ≡.refl
+    }
+  D .F₁ {A} {B} f = record
+    { u = f
+    ; equivariance = ≡.refl
+    }
+  D .identity = ≡.refl
+  D .homomorphism = ≡.refl
+  D .F-resp-≈ f≡g = f≡g
+
+  V : Functor (G-Sets G) (Sets ℓ)
+  V .F₀ GS = Orb
+    where
+      open G-Set GS
+  V .F₁ {A} {B} f (x , (y , (g , eq))) = (< f > x , (< f > y , (g , ≡.trans (≡.sym f.equivariance) (≡.cong < f > eq))))
+    where
+      open G-Set A
+      module f = G-Set-Morphism f
+  V .identity {GS} {(x , (y , (g , ≡.refl)))} = ≡.refl
+  V .homomorphism {X} {Y} {Z} {f} {g} = {!!}
+  V .F-resp-≈ {A} {B} {f} {g} eq {(x , (y , (h , ≡.refl)))} = peq (eq , {!!})
+    where
+      module f = G-Set-Morphism f
+      module g = G-Set-Morphism g
+      module A = G-Set A
diff --git a/Category/G-Sets/Properties/Equivalence.agda b/Category/G-Sets/Properties/Equivalence.agda
new file mode 100644
index 0000000..a3ba62e
--- /dev/null
+++ b/Category/G-Sets/Properties/Equivalence.agda
@@ -0,0 +1,90 @@
+open import Category.G-Sets
+open import Algebra.Group
+open import Algebra.G-Set
+open import Category.Construction.GroupAsCategory
+open import Categories.Category.Construction.Functors renaming (Functors to [_,_])
+open import Categories.Category.Equivalence
+open import Categories.Category.Instance.Sets
+open import Categories.NaturalTransformation renaming (id to idN)
+open import Categories.NaturalTransformation.NaturalIsomorphism
+open import Categories.Functor.Core
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.Unit.Polymorphic
+
+-- The category 'G-Sets' is equivalent to the category [ G , Sets ]
+
+module Category.G-Sets.Properties.Equivalence {ℓ} (G : Group ℓ) where
+  open StrongEquivalence renaming (G to H)
+  open WeakInverse renaming (F∘G≈id to F∘H≅id; G∘F≈id to H∘F≅id)
+  open Functor
+  open NaturalIsomorphism
+  G-Sets≅[G,Sets] : StrongEquivalence (G-Sets G) [ GroupAsCategory G , Sets ℓ ]
+
+  -- F : G-Sets → [ G , Sets ]
+  G-Sets≅[G,Sets] .F .F₀ GS = record
+                               { F₀ = λ _ → X
+                               ; F₁ = λ f x → f ⊳ x
+                               ; identity = ε⊳
+                               ; homomorphism = ∘⊳
+                               ; F-resp-≈ = λ f≡g {x} → ≡.cong (_⊳ x) f≡g
+                               }
+    where open G-Set GS
+  G-Sets≅[G,Sets] .F .F₁ {A} {B} f = ntHelper (record { η = λ X x → f.u x ; commute = λ g → f.equivariance })
+    where
+      module f = G-Set-Morphism f
+  G-Sets≅[G,Sets] .F .identity = ≡.refl
+  G-Sets≅[G,Sets] .F .homomorphism = ≡.refl
+  G-Sets≅[G,Sets] .F .F-resp-≈ = λ x → x
+
+  -- H : [ G , Sets ] → G-Sets
+  G-Sets≅[G,Sets] .H .F₀ M = record
+    { X = M.₀ tt 
+    ; _⊳_ = λ g x → (M.₁ g) x
+    ; ε⊳ = M.identity
+    ; ∘⊳ = M.homomorphism
+    }
+    where
+      module M = Functor M
+  G-Sets≅[G,Sets] .H .F₁ {M} {N} α = record
+    { u = α.η tt
+    ; equivariance = λ {g} {x} → α.commute g
+    }
+    where
+      module α = NaturalTransformation α
+  G-Sets≅[G,Sets] .H .identity = ≡.refl
+  G-Sets≅[G,Sets] .H .homomorphism = ≡.refl
+  G-Sets≅[G,Sets] .H .F-resp-≈ = λ x → x
+
+  -- F∘H = Id
+  G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .F⇒G = ntHelper (record
+    { η = λ M → ntHelper (record
+      { η = λ _ x → x
+      ; commute = λ f {x} → ≡.refl
+      })
+    ; commute = λ {M} {N} α {x} → ≡.refl
+    })
+  G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .F⇐G = ntHelper (record
+    { η = λ M → ntHelper (record
+      { η = λ _ x → x
+      ; commute = λ f {x} → ≡.refl
+      })
+    ; commute = λ {M} {N} α {x} → ≡.refl
+    })
+  G-Sets≅[G,Sets] .weak-inverse .F∘H≅id .iso M = record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
+
+  -- H∘F = Id
+  G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .F⇒G = ntHelper (record
+    { η = λ GS → record
+      { u = λ x → x
+      ; equivariance = ≡.refl
+      }
+    ; commute = λ {GS} {GM} f {x} → ≡.refl
+    })
+  G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .F⇐G = ntHelper (record
+    { η = λ GS → record
+      { u = λ x → x
+      ; equivariance = ≡.refl
+      }
+    ; commute = λ {GS} {GM} f {x} → ≡.refl
+    })
+  G-Sets≅[G,Sets] .weak-inverse .H∘F≅id .iso GS = record { isoˡ = ≡.refl ; isoʳ = ≡.refl }
diff --git a/Category/G-Sets/Properties/FreeObject.agda b/Category/G-Sets/Properties/FreeObject.agda
new file mode 100644
index 0000000..a553a01
--- /dev/null
+++ b/Category/G-Sets/Properties/FreeObject.agda
@@ -0,0 +1,48 @@
+open import Algebra.G-Set
+open import Algebra.Group
+open import Category.G-Sets
+open import Categories.FreeObjects.Free
+open import Categories.Functor.Core
+open import Categories.Category.Instance.Sets
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.Product
+
+-- The category G-Sets has free objects
+
+module Category.G-Sets.Properties.FreeObject {ℓ} (G : Group ℓ) where
+  open Group using () renaming (Carrier to ∣_∣)
+  open G-Set using () renaming (X to ∣_∣)
+  open G-Set-Morphism using () renaming (u to <_>)
+  open FreeObject
+  open Group G hiding (Carrier)
+
+  forgetfulF : Functor (G-Sets G) (Sets ℓ)
+  forgetfulF = record
+                { F₀ = λ GS → ∣ GS ∣
+                ; F₁ = λ f → < f >
+                ; identity = ≡.refl
+                ; homomorphism = ≡.refl
+                ; F-resp-≈ = λ x → x
+                }
+
+  free-G-Set : ∀ {X : Set ℓ} → FreeObject forgetfulF X
+  free-G-Set {X} .FX = record
+    { X = ∣ G ∣ × X
+    ; _⊳_ = λ g (h , x) → (g ∙ h , x)
+    ; ε⊳ = λ {(g , x)} → ≡.cong (_, x) idˡ
+    ; ∘⊳ = λ {g} {h} {(f , x)} → ≡.cong (_, x) assoc
+    }
+  free-G-Set .η x = (ε , x)
+  free-G-Set {X} ._* {GS} f = record
+    { u = λ (g , x) → g ⊳ f x
+    ; equivariance = λ {g} {x} → ∘⊳
+    }
+    where open G-Set GS
+  free-G-Set {X} .*-lift {GS} f {x} = ε⊳
+    where open G-Set GS
+  free-G-Set {X} .*-uniq {GS} f f' g-prop {(h , y)} = ≡.trans (≡.cong < f' > (≡.cong (_, y) (≡.sym idʳ)) )
+                                                     (≡.trans (f'.equivariance)
+                                                              (≡.cong (h ⊳_) g-prop))
+    where
+      open G-Set GS
+      module f' = G-Set-Morphism f'
diff --git a/Category/GSets.agda b/Category/GSets.agda
deleted file mode 100644
index c8460e0..0000000
--- a/Category/GSets.agda
+++ /dev/null
@@ -1,33 +0,0 @@
-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 <_>)
diff --git a/Preliminaries.agda b/Preliminaries.agda
new file mode 100644
index 0000000..fa9e5a7
--- /dev/null
+++ b/Preliminaries.agda
@@ -0,0 +1,4 @@
+module Preliminaries where
+  open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) public
+  postulate
+    FunExt : ∀ {ℓ} {X Y : Set ℓ} {f g : X → Y} → (∀ (x : X) → f x ≡ g x) → f ≡ g