Rename One properties

1 files changed, 12 insertions, 12 deletions

diff --git a/Category/Instance/One/Properties.agda b/Category/Instance/One/Properties.agda
index 1452669..c6261bb 100644
--- a/Category/Instance/One/Properties.agda
+++ b/Category/Instance/One/Properties.agda
@@ -8,7 +8,7 @@ open import Categories.Category.Core using (Category)
 open import Categories.Category.Instance.One using () renaming (One to One′)
 
 One : Category o ℓ e
-One = One′
+One = One′ {o} {ℓ} {e}
 
 open import Categories.Category.Cocartesian One using (Cocartesian)
 open import Categories.Category.Cocomplete.Finitely One using (FinitelyCocomplete)
@@ -16,20 +16,20 @@ open import Categories.Object.Initial One using (Initial)
 open import Categories.Category.Cocartesian One using (BinaryCoproducts)
 
 
-One-Initial : Initial
-One-Initial = _
+initial : Initial
+initial = _
 
-One-BinaryCoproducts : BinaryCoproducts
-One-BinaryCoproducts = _
+coproducts : BinaryCoproducts
+coproducts = _
 
-One-Cocartesian : Cocartesian
-One-Cocartesian = record
-    { initial = One-Initial
-    ; coproducts = One-BinaryCoproducts
+cocartesian : Cocartesian
+cocartesian = record
+    { initial = initial
+    ; coproducts = coproducts
     }
 
-One-FinitelyCocomplete : FinitelyCocomplete
-One-FinitelyCocomplete = record
-    { cocartesian = One-Cocartesian
+finitelyCocomplete : FinitelyCocomplete
+finitelyCocomplete = record
+    { cocartesian = cocartesian
     ; coequalizer = _
     }