Update structure

.gitignore

@@ -3,4 +3,4 @@
 \#*.agda#
 .#*.agda
 .DS_Store
-
+_build

Groups/Core.agda

@@ -1,16 +0,0 @@
-module Groups.Core where
-
-open import Relation.Binary.PropositionalEquality
-open import Level
-
-private
-  variable
-    ℓ : Level
-
-record Group (G : Set ℓ) (𝑒 : G) (_∙_ : G → G → G) : Set ℓ where
-  field
-    assoc : ∀ {f g h} → (f ∙ g) ∙ h ≡ f ∙ (g ∙ h)
-    id    : ∀ {g} → g ∙ 𝑒 ≡ 𝑒 ∙ g
-    invₗ  : ∀ {g h} → g ∙ h ≡ 𝑒
-    invᵣ  : ∀ {g h} → 𝑒 ≡ h ∙ g
-

category-research.agda-lib

@@ -0,0 +1,4 @@
+name: category-research
+depend: standard-library
+include: src
+

CategoricalRelation/Heterogeneous.agda → src/CategoricalRelation/Heterogeneous.agda

@@ -1,7 +1,6 @@
-open import Level
-
 module CategoricalRelation.Heterogeneous where
 
+open import Level
 open import Categories.Core using (Category; Obj; _[_,_])
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
 

src/Groups/Core.agda

@@ -0,0 +1,39 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+module Groups.Core where
+
+open import Relation.Binary.PropositionalEquality using (refl; _≡_; sym; cong)
+open import Level
+
+private
+  variable
+    ℓ : Level
+
+record Group (G : Set ℓ) : Set ℓ where
+  infixr 9 _∙_
+  field
+    𝑒   : G
+    _∙_ : G → G → G
+    _⁻¹ : G → G
+  field
+    assocₗ : ∀ 𝑥 𝑦 𝑧 → (𝑥 ∙ 𝑦) ∙ 𝑧 ≡ 𝑥 ∙ (𝑦 ∙ 𝑧)
+    assocᵣ : ∀ 𝑥 𝑦 𝑧 → 𝑥 ∙ (𝑦 ∙ 𝑧) ≡ (𝑥 ∙ 𝑦) ∙ 𝑧
+    idₗ   : ∀ 𝑥 → 𝑥 ∙ 𝑒 ≡ 𝑥
+    idᵣ   : ∀ 𝑥 → 𝑒 ∙ 𝑥 ≡ 𝑥
+    invₗ  : ∀ 𝑥 → 𝑥 ∙ (𝑥 ⁻¹) ≡ 𝑒
+    invᵣ  : ∀ 𝑥 → (𝑥 ⁻¹) ∙ 𝑥 ≡ 𝑒
+
+record CommutativeGroup (G : Set ℓ) {𝐺 : Group G} : Set ℓ where
+  open Group 𝐺 using (_∙_)
+  field
+    comm : ∀ 𝑥 𝑦 → 𝑥 ∙ 𝑦 ≡ 𝑦 ∙ 𝑥
+
+module GroupProp {G : Set ℓ} {𝐺 : Group G} where
+
+  open Group 𝐺
+  
+  -- Cancellation
+  cancelₗ : (a g h : G) → g ∙ a ≡ h ∙ a → g ≡ h
+  cancelₗ a g h p = {!!}
+  
+  cancelᵣ : (a g h : G) → a ∙ g ≡ a ∙ h → g ≡ h
+  cancelᵣ a g h p = {!!}