diff --git a/Algebra/G-Set.agda b/Algebra/G-Set.agda
index 30ed6c8..c0e62bd 100644
--- a/Algebra/G-Set.agda
+++ b/Algebra/G-Set.agda
@@ -1,7 +1,7 @@
 open import Algebra.Group
 open import Level
 open import Data.Product
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 module Algebra.G-Set {ℓ : Level} where
   open Group using () renaming (Carrier to ∣_∣)
@@ -14,22 +14,35 @@ module Algebra.G-Set {ℓ : Level} where
       ε⊳ : ∀ {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 : X → Set ℓ
+    -- orb x = Σ[ y ∈ X ] Σ[ g ∈ ∣ G ∣ ] g ⊳ x ≡ y
 
-    Orb : Set ℓ
-    Orb = Σ[ x ∈ X ] orb x
+    -- Orb : Set ℓ
+    -- Orb = Σ[ x ∈ X ] orb x
 
-    -- record orb (x : X) : Set ℓ where
-    --   field
-    --     y : X
-    --     g : ∣ G ∣
-    --     .eq : g ⊳ x ≡ y
+    record orb (x : X) : Set ℓ where
+      constructor orb[_,_,_]
+      field
+        y : X
+        g : ∣ G ∣
+        .eq : g ⊳ x ≡ y
+
+    orb-intro : ∀ {x : X} {y z : X} {g h : ∣ G ∣} {eq₁ : g ⊳ x ≡ y} {eq₂ : h ⊳ x ≡ z} (p : y ≡ z) (q : g ≡ h)
+                → ≡.subst₂ (λ y g → g ⊳ x ≡ y) p q eq₁ ≡ eq₂
+                → orb[ y , g , eq₁ ] ≡ orb[ z , h , eq₂ ]
+    orb-intro ≡.refl ≡.refl ≡.refl = ≡.refl
+
+    record Orb : Set ℓ where
+      constructor Orb[_,_]
+      field
+        x : X
+        o : orb x
+
+    Orb-intro : ∀ {x y : X} {o₁ : orb x} {o₂ : orb y} (p : x ≡ y)
+                → ≡.subst (λ x → orb x) p o₁ ≡ o₂
+                → Orb[ x , o₁ ] ≡ Orb[ y , o₂ ]
+    Orb-intro ≡.refl ≡.refl = ≡.refl
 
-    -- record Orb : Set ℓ where
-    --   field
-    --     x : X
-    --     O : orb x
 
   open G-Set using () renaming (X to ∣_∣)
 
diff --git a/Category/G-Sets/Properties/A4.agda b/Category/G-Sets/Properties/A4.agda
index cc0a457..160c542 100644
--- a/Category/G-Sets/Properties/A4.agda
+++ b/Category/G-Sets/Properties/A4.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --irrelevant-projections #-}
 open import Algebra.G-Set
 open import Algebra.Group
 open import Category.G-Sets
@@ -5,13 +6,18 @@ 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.Properties
 open import Relation.Binary.PropositionalEquality.WithK
 open import Axiom.UniquenessOfIdentityProofs.WithK
 open import Data.Product
+open import Data.Product.Relation.Binary.Pointwise.Dependent.WithK
+open import Data.Product.Relation.Binary.Pointwise.Dependent
 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)
@@ -33,14 +39,32 @@ module Category.G-Sets.Properties.A4 {ℓ} (G : Group ℓ) where
   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))))
+  V .F₁ {A} {B} f O = Orb[ < f > O.x , G-Set.orb[ (< f > o.y) , o.g , (≡.trans (≡.sym f.equivariance) (≡.cong < f > o.eq)) ] ]
+  -- 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
+      open G-Set A using () renaming (Orb to OrbA; orb to orbA; Orb[_,_] to OrbA[_,_])
+      open G-Set B using (Orb[_,_]; orb[_,_,_]) renaming (Orb to OrbB; orb to orbB)
       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 , {!!})
+      module O = OrbA O
+      module o = orbA O.o
+  V .identity {GS} {O} = Orb-intro ≡.refl ≡.refl
     where
-      module f = G-Set-Morphism f
-      module g = G-Set-Morphism g
+    open G-Set GS
+
+  -- V .identity {GS} {(x , (y , (g , ≡.refl)))} = ≡.refl
+  V .homomorphism {X} {Y} {Z} {f} {g} {O} = Orb-intro ≡.refl ≡.refl
+    where
+    open G-Set Z
+  -- TODO needs something like subst-application, but for orb...
+  V .F-resp-≈ {A} {B} {f} {g} eq {O} = {!!}
+  -- V .F-resp-≈ {A} {B} {f} {g} eq {(x , (y , (h , ≡.refl)))} = peq ((eq {x}) , {!!})
+    where
+      module f = G-Set-Morphism f hiding (u)
+      module g = G-Set-Morphism g hiding (u)
       module A = G-Set A
+      open G-Set A using () renaming (Orb to OrbA; orb to orbA)
+      open G-Set B using () renaming (Orb[_,_] to OrbB[_,_]; orb[_,_,_] to orbB[_,_,_]; Orb-intro to Orb-introB; orb-intro to orb-introB)
+      module O = OrbA O
+      module o = orbA O.o
+      helper : (e : < f > O.x ≡ < g > O.x) → (≡.subst (G-Set.orb B) (eq {O.x}) orbB[ < f > o.y , o.g , _ ]) ≡ orbB[ < f > o.y , o.g , _ ]
+      helper e = {!!}