diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index b8f91ab..d78e4ca 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -22,7 +22,7 @@ eqpair eqa eqb i = eqa i , eqb i
 
 open Functor
 open IsFunctor
-open Category
+open Category hiding (_∘_)
 
 -- The category of categories
 module _ (ℓ ℓ' : Level) where
@@ -40,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
                    ((h ∘f (g ∘f f)) .isFunctor .ident)
                    (((h ∘f g) ∘f f) .isFunctor .ident)
         postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
-                          → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a))
+                          → eq→ i (A [ a' ∘ a ]) ≡ D [ eq→ i a' ∘ eq→ i a ])
                             ((h ∘f (g ∘f f)) .isFunctor .distrib) (((h ∘f g) ∘f f) .isFunctor .distrib)
 
       assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f
@@ -64,7 +64,7 @@ module _ (ℓ ℓ' : Level) where
             eqD-r : PathP
                         (λ i →
                         {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} →
-                        eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
+                        eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
                         ((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
         ident-r : F ∘f identity ≡ F
         ident-r = Functor≡ eq* eq→ eqI-r eqD-r
@@ -78,7 +78,7 @@ module _ (ℓ ℓ' : Level) where
             eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
                   ((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident)
             eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
-                 → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
+                 → eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
                  ((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
         ident-l : identity ∘f F ≡ F
         ident-l = Functor≡ eq* eq→ eqI eqD
@@ -89,7 +89,7 @@ module _ (ℓ ℓ' : Level) where
       { Object = Category ℓ ℓ'
       ; Arrow = Functor
       ; 𝟙 = identity
-      ; _⊕_ = _∘f_
+      ; _∘_ = _∘f_
       -- What gives here? Why can I not name the variables directly?
       ; isCategory = record
         { assoc = λ {_ _ _ _ f g h} → assc {f = f} {g = g} {h = h}
@@ -112,7 +112,7 @@ module _ {ℓ ℓ' : Level} where
         :Arrow: b c →
         :Arrow: a b →
         :Arrow: a c
-      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (ℂ ._⊕_) bc∈C ab∈C , 𝔻 ._⊕_ bc∈D ab∈D}
+      _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
 
       instance
         :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
@@ -131,7 +131,7 @@ module _ {ℓ ℓ' : Level} where
         { Object = :Object:
         ; Arrow = :Arrow:
         ; 𝟙 = :𝟙:
-        ; _⊕_ = _:⊕:_
+        ; _∘_ = _:⊕:_
         }
 
       proj₁ : Arrow Catt :product: ℂ
@@ -161,16 +161,16 @@ module _ {ℓ ℓ' : Level} where
 
         -- Need to "lift equality of functors"
         -- If I want to do this like I do it for pairs it's gonna be a pain.
-        postulate isUniqL : (Catt ⊕ proj₁) x ≡ x₁
+        postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
         -- isUniqL = Functor≡ refl refl {!!} {!!}
 
-        postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂
+        postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
         -- isUniqR = Functor≡ refl refl {!!} {!!}
 
-        isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂
+        isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
         isUniq = isUniqL , isUniqR
 
-        uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂)
+        uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂)
         uniq = x , isUniq
 
     instance
@@ -199,9 +199,6 @@ module _ (ℓ : Level) where
     Catℓ = Cat ℓ ℓ
     module _ (ℂ 𝔻 : Category ℓ ℓ) where
       private
-        _𝔻⊕_ = 𝔻 ._⊕_
-        _ℂ⊕_ = ℂ ._⊕_
-
         :obj: : Cat ℓ ℓ .Object
         :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
 
@@ -233,13 +230,13 @@ module _ (ℓ : Level) where
             G→f : 𝔻 .Arrow (G .func* A) (G .func* B)
             G→f = G .func→ f
             l : 𝔻 .Arrow (F .func* A) (G .func* B)
-            l = θB 𝔻⊕ F→f
+            l = 𝔻 [ θB ∘ F→f ]
             r : 𝔻 .Arrow (F .func* A) (G .func* B)
-            r = G→f 𝔻⊕ θA
+            r = 𝔻 [ G→f ∘ θA ]
             -- There are two choices at this point,
             -- but I suppose the whole point is that
             -- by `θNat f` we have `l ≡ r`
-            --     lem : θ B 𝔻⊕ F .func→ f ≡ G .func→ f 𝔻⊕ θ A
+            --     lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
             --     lem = θNat f
             result : 𝔻 .Arrow (F .func* A) (G .func* B)
             result = l
@@ -257,17 +254,16 @@ module _ (ℓ : Level) where
         -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
         -- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
         --   where
-        --     _𝔻⊕_ = 𝔻 ._⊕_
         --     open module 𝔻 = IsCategory (𝔻 .isCategory)
         -- Unfortunately the equational version has some ambigous arguments.
         :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙
         :ident: = begin
           :func→: {c} {c} ((:obj: ×p ℂ) .Product.obj .𝟙 {c}) ≡⟨⟩
           :func→: {c} {c} (identityNat F , ℂ .𝟙)             ≡⟨⟩
-          (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙))             ≡⟨⟩
-          𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙)                            ≡⟨ proj₂ 𝔻.ident ⟩
+          𝔻 [ identityTrans F C ∘ F .func→ (ℂ .𝟙)]           ≡⟨⟩
+          𝔻 [ 𝔻 .𝟙 ∘ F .func→ (ℂ .𝟙)]                        ≡⟨ proj₂ 𝔻.ident ⟩
           F .func→ (ℂ .𝟙)                                    ≡⟨ F.ident ⟩
-          𝔻 .𝟙 ∎
+          𝔻 .𝟙                                               ∎
           where
             open module 𝔻 = IsCategory (𝔻 .isCategory)
             open module F = IsFunctor (F .isFunctor)
@@ -280,7 +276,7 @@ module _ (ℓ : Level) where
         H = H×C .proj₁
         C = H×C .proj₂
         -- Not entirely clear what this is at this point:
-        _P⊕_ = (:obj: ×p ℂ) .Product.obj ._⊕_ {F×A} {G×B} {H×C}
+        _P⊕_ = (:obj: ×p ℂ) .Product.obj .Category._∘_ {F×A} {G×B} {H×C}
         module _
           -- NaturalTransformation F G × ℂ .Arrow A B
           {θ×f : NaturalTransformation F G × ℂ .Arrow A B}
@@ -300,26 +296,33 @@ module _ (ℓ : Level) where
             g = proj₂ η×g
 
             ηθNT : NaturalTransformation F H
-            ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
+            ηθNT = Fun .Category._∘_ {F} {G} {H} (η , ηNat) (θ , θNat)
 
             ηθ = proj₁ ηθNT
             ηθNat = proj₂ ηθNT
 
           :distrib: :
-              (η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f)
-            ≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
+              𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ]
+            ≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ]
           :distrib: = begin
-            (ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f)                ≡⟨ ηθNat (g ℂ⊕ f) ⟩
-            H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A)                ≡⟨ cong (λ φ → φ 𝔻⊕ ηθ A) (H.distrib) ⟩
-            (H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A)       ≡⟨ sym assoc ⟩
-            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨⟩
-            H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A))       ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) assoc ⟩
-            H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩
-            H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym assoc) ⟩
-            H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ assoc ⟩
-            (H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩
-            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩
-            (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) ∎
+            𝔻 [ (ηθ C) ∘ F .func→ (ℂ [ g ∘ f ]) ]
+              ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
+            𝔻 [ H .func→ (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.distrib) ⟩
+            𝔻 [ 𝔻 [ H .func→ g ∘ H .func→ f ] ∘ (ηθ A) ]
+              ≡⟨ sym assoc ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ H .func→ f ∘ ηθ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) assoc ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ H .func→ f ∘ η A ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ 𝔻 [ η B ∘ G .func→ f ] ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ H .func→ g ∘ φ ]) (sym assoc) ⟩
+            𝔻 [ H .func→ g ∘ 𝔻 [ η B ∘ 𝔻 [ G .func→ f ∘ θ A ] ] ] ≡⟨ assoc ⟩
+            𝔻 [ 𝔻 [ H .func→ g ∘ η B ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ G .func→ f ∘ θ A ] ]) (sym (ηNat g)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ G .func→ f ∘ θ A ] ]
+              ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ φ ]) (sym (θNat f)) ⟩
+            𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ] ∎
             where
               open IsCategory (𝔻 .isCategory)
               open module H = IsFunctor (H .isFunctor)
@@ -339,9 +342,9 @@ module _ (ℓ : Level) where
 
         postulate
           transpose : Functor 𝔸 :obj:
-          eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F
+          eq : Catℓ [ :eval: ∘ (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ] ≡ F
 
-        catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F)
+        catTranspose : ∃![ F~ ] (Catℓ [ :eval: ∘ (parallelProduct F~ (Catℓ .𝟙 {o = ℂ}))] ≡ F )
         catTranspose = transpose , eq
 
       :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index c818e76..e3d0c83 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -10,19 +10,19 @@ open import Cat.Category
 open import Cat.Functor
 
 module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
-  open Category
+  open Category hiding ( _∘_ ; Arrow )
   open Functor
 
   module _ (F G : Functor ℂ 𝔻) where
     -- What do you call a non-natural tranformation?
     Transformation : Set (ℓc ⊔ ℓd')
-    Transformation = (C : ℂ .Object) → 𝔻 .Arrow (F .func* C) (G .func* C)
+    Transformation = (C : ℂ .Object) → 𝔻 [ F .func* C , G .func* C ]
 
     Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
     Natural θ
       = {A B : ℂ .Object}
-      → (f : ℂ .Arrow A B)
-      → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
+      → (f : ℂ [ A , B ])
+      → 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
 
     NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
     NaturalTransformation = Σ Transformation Natural
@@ -30,18 +30,28 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
     -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
 
+  module _ {F G : Functor ℂ 𝔻} where
+    NaturalTransformation≡ : {α β : NaturalTransformation F G}
+      → (eq₁ : α .proj₁ ≡ β .proj₁)
+      → (eq₂ : PathP
+          (λ i → {A B : ℂ .Object} (f : ℂ [ A , B ])
+            → 𝔻 [ eq₁ i B ∘ F .func→ f ]
+            ≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
+        (α .proj₂) (β .proj₂))
+      → α ≡ β
+    NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
+
   identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
   identityTrans F C = 𝔻 .𝟙
 
   identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
   identityNatural F {A = A} {B = B} f = begin
-    identityTrans F B 𝔻⊕ F→ f                 ≡⟨⟩
-    𝔻 .𝟙              𝔻⊕ F→ f                 ≡⟨ proj₂ 𝔻.ident ⟩
-    F→ f                                       ≡⟨ sym (proj₁ 𝔻.ident) ⟩
-    F→ f              𝔻⊕ 𝔻 .𝟙                 ≡⟨⟩
-    F→ f              𝔻⊕ identityTrans F A     ∎
+    𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
+    𝔻 [ 𝔻 .𝟙 ∘  F→ f ]              ≡⟨ proj₂ 𝔻.ident ⟩
+    F→ f                            ≡⟨ sym (proj₁ 𝔻.ident) ⟩
+    𝔻 [ F→ f ∘ 𝔻 .𝟙 ]               ≡⟨⟩
+    𝔻 [ F→ f ∘ identityTrans F A ]  ∎
     where
-      _𝔻⊕_ = 𝔻 ._⊕_
       F→ = F .func→
       open module 𝔻 = IsCategory (𝔻 .isCategory)
 
@@ -50,21 +60,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
 
   module _ {F G H : Functor ℂ 𝔻} where
     private
-      _𝔻⊕_ = 𝔻 ._⊕_
       _∘nt_ : Transformation G H → Transformation F G → Transformation F H
-      (θ ∘nt η) C = θ C 𝔻⊕ η C
+      (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]
 
     NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
     proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
     proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
-      ((θ ∘nt η) B) 𝔻⊕ (F .func→ f)    ≡⟨⟩
-      (θ B 𝔻⊕ η B) 𝔻⊕ (F .func→ f)     ≡⟨ sym assoc ⟩
-      θ B 𝔻⊕ (η B 𝔻⊕ (F .func→ f))     ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩
-      θ B 𝔻⊕ ((G .func→ f) 𝔻⊕ η A)     ≡⟨ assoc ⟩
-      (θ B 𝔻⊕ (G .func→ f)) 𝔻⊕ η A     ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩
-      (((H .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A)   ≡⟨ sym assoc ⟩
-      ((H .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A))   ≡⟨⟩
-      ((H .func→ f)  𝔻⊕ ((θ ∘nt η) A)) ∎
+      𝔻 [ (θ ∘nt η) B ∘ F .func→ f ]     ≡⟨⟩
+      𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F .func→ f ] ≡⟨ sym assoc ⟩
+      𝔻 [ θ B ∘ 𝔻 [ η B ∘ F .func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
+      𝔻 [ θ B ∘ 𝔻 [ G .func→ f ∘ η A ] ] ≡⟨ assoc ⟩
+      𝔻 [ 𝔻 [ θ B ∘ G .func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
+      𝔻 [ 𝔻 [ H .func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
+      𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
+      𝔻 [ H .func→ f ∘ (θ ∘nt η) A ]     ∎
       where
         open IsCategory (𝔻 .isCategory)
     NatComp = _:⊕:_
@@ -100,7 +109,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
     { Object = Functor ℂ 𝔻
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → identityNat F
-    ; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H}
+    ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
     }
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
@@ -112,5 +121,5 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     { Object = Presheaf ℂ
     ; Arrow = NaturalTransformation
     ; 𝟙 = λ {F} → identityNat F
-    ; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
+    ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
     }
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 42d63ab..43f3409 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -159,6 +159,6 @@ Rel = record
   { Object = Set
   ; Arrow = λ S R → Subset (S × R)
   ; 𝟙 = λ {S} → Diag S
-  ; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
+  ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
   ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
   }
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 634a3a7..31a0b63 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -3,7 +3,6 @@ module Cat.Categories.Sets where
 open import Cubical
 open import Agda.Primitive
 open import Data.Product
-open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
 
 open import Cat.Category
 open import Cat.Functor
@@ -15,7 +14,7 @@ module _ {ℓ : Level} where
     { Object = Set ℓ
     ; Arrow = λ T U → T → U
     ; 𝟙 = id
-    ; _⊕_ = _∘′_
+    ; _∘_ = _∘′_
     ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
     }
     where
@@ -26,16 +25,15 @@ module _ {ℓ : Level} where
       _&&&_ : (X → A × B)
       _&&&_ x = f x , g x
     module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
-      _S⊕_ = Sets ._⊕_
-      lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g
+      lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
       proj₁ lem = refl
       proj₂ lem = refl
     instance
-      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd
+      isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂
       isProduct f g = f &&& g , lem f g
 
     product : (A B : Sets .Object) → Product {ℂ = Sets} A B
-    product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct }
+    product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
 
   instance
     SetsHasProducts : HasProducts Sets
@@ -49,9 +47,9 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
 representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
 representable {ℂ = ℂ} A = record
   { func* = λ B → ℂ .Arrow A B
-  ; func→ = ℂ ._⊕_
+  ; func→ = ℂ ._∘_
   ; isFunctor = record
-    { ident = funExt λ _ → snd ident
+    { ident = funExt λ _ → proj₂ ident
     ; distrib = funExt λ x → sym assoc
     }
   }
@@ -66,9 +64,9 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
 presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
 presheaf {ℂ = ℂ} B = record
   { func* = λ A → ℂ .Arrow A B
-  ; func→ = λ f g → ℂ ._⊕_ g f
+  ; func→ = λ f g → ℂ ._∘_ g f
   ; isFunctor = record
-    { ident = funExt λ x → fst ident
+    { ident = funExt λ x → proj₁ ident
     ; distrib = funExt λ x → assoc
     }
   }
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 99e4cd1..586e00f 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -10,7 +10,7 @@ open import Data.Product renaming
   ; ∃! to ∃!≈
   )
 open import Data.Empty
-open import Function
+import Function
 open import Cubical
 
 ∃! : ∀ {a b} {A : Set a}
@@ -43,9 +43,9 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
     Object : Set ℓ
     Arrow  : Object → Object → Set ℓ'
     𝟙      : {o : Object} → Arrow o o
-    _⊕_    : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c
-    {{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
-  infixl 45 _⊕_
+    _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
+    {{isCategory}} : IsCategory Object Arrow 𝟙 _∘_
+  infixl 10 _∘_
   domain : { a b : Object } → Arrow a b → Object
   domain {a = a} _ = a
   codomain : { a b : Object } → Arrow a b → Object
@@ -57,18 +57,18 @@ _[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : ℂ .Object) →
 _[_,_] = Arrow
 
 _[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
-_[_∘_] = _⊕_
+_[_∘_] = _∘_
 
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
   module _ { A B : ℂ .Object } where
     Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
-    Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙
+    Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ [ g ∘ f ] ≡ ℂ .𝟙 × ℂ [ f ∘ g ] ≡ ℂ .𝟙
 
     Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ'
-    Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁
+    Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ [ g₀ ∘ f ] ≡ ℂ [ g₁ ∘ f ] → g₀ ≡ g₁
 
     Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
-    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁
+    Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ [ f ∘ g₀ ] ≡ ℂ [ f ∘ g₁ ] → g₀ ≡ g₁
 
   -- Isomorphism of objects
   _≅_ : (A B : Object ℂ) → Set ℓ'
@@ -78,7 +78,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} whe
   IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
   IsProduct π₁ π₂
     = ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
-    → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂)
+    → ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)
 
 -- Tip from Andrea; Consider this style for efficiency:
 -- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
@@ -112,17 +112,17 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ 
   parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B'
     → ℂ .Arrow (objectProduct A B) (objectProduct A' B')
   parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
-    (ℂ ._⊕_ a ((product A B) .proj₁))
-    (ℂ ._⊕_ b ((product A B) .proj₂))
+    (ℂ [ a ∘ (product A B) .proj₁ ])
+    (ℂ [ b ∘ (product A B) .proj₂ ])
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   Opposite : Category ℓ ℓ'
   Opposite =
     record
       { Object = ℂ .Object
-      ; Arrow = flip (ℂ .Arrow)
+      ; Arrow = Function.flip (ℂ .Arrow)
       ; 𝟙 = ℂ .𝟙
-      ; _⊕_ = flip (ℂ ._⊕_)
+      ; _∘_ = Function.flip (ℂ ._∘_)
       ; isCategory = record { assoc = sym assoc ; ident = swap ident }
       }
       where
@@ -145,7 +145,7 @@ Hom ℂ A B = Arrow ℂ A B
 module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
   HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
     → Hom ℂ A B → Hom ℂ A B'
-  HomFromArrow _A = _⊕_ ℂ
+  HomFromArrow _A = ℂ ._∘_
 
 module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
   open HasProducts hasProducts
@@ -157,7 +157,7 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
   module _ (B C : ℂ .Category.Object) where
     IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ')
     IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C)
-      → ∃![ f~ ] (ℂ ._⊕_ eval (parallelProduct f~ (ℂ .𝟙)) ≡ f)
+      → ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (ℂ .𝟙)] ≡ f)
 
     record Exponential : Set (ℓ ⊔ ℓ') where
       field
diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda
index 5686356..1facb03 100644
--- a/src/Cat/Category/Free.agda
+++ b/src/Cat/Category/Free.agda
@@ -31,6 +31,6 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
     { Object = Obj
     ; Arrow = Path
     ; 𝟙 = λ {o} → emptyPath o
-    ; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
+    ; _∘_ = λ {a b c} → concatenate {a} {b} {c}
     ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
     }
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 2a540ba..c672a53 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -15,27 +15,26 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje
   open IsCategory (isCategory)
 
   iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f
-  iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq =
-    begin
+  iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
     g₀              ≡⟨ sym (proj₁ ident) ⟩
-    g₀ ⊕ 𝟙          ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩
-    g₀ ⊕ (f ⊕ f-)   ≡⟨ assoc ⟩
-    (g₀ ⊕ f) ⊕ f-   ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩
-    (g₁ ⊕ f) ⊕ f-   ≡⟨ sym assoc ⟩
-    g₁ ⊕ (f ⊕ f-)   ≡⟨ cong (_⊕_ g₁) right-inv ⟩
-    g₁ ⊕ 𝟙          ≡⟨ proj₁ ident ⟩
+    g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
+    g₀ ∘ (f ∘ f-)   ≡⟨ assoc ⟩
+    (g₀ ∘ f) ∘ f-   ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
+    (g₁ ∘ f) ∘ f-   ≡⟨ sym assoc ⟩
+    g₁ ∘ (f ∘ f-)   ≡⟨ cong (_∘_ g₁) right-inv ⟩
+    g₁ ∘ 𝟙          ≡⟨ proj₁ ident ⟩
     g₁              ∎
 
   iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f
   iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
     begin
     g₀            ≡⟨ sym (proj₂ ident) ⟩
-    𝟙 ⊕ g₀        ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩
-    (f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩
-    f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩
-    f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩
-    (f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩
-    𝟙 ⊕ g₁        ≡⟨ proj₂ ident ⟩
+    𝟙 ∘ g₀        ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
+    (f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩
+    f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
+    f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩
+    (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
+    𝟙 ∘ g₁        ≡⟨ proj₂ ident ⟩
     g₁            ∎
 
   iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f
@@ -71,17 +70,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
 
     module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
       :func→: : NaturalTransformation (prshf A) (prshf B)
-      :func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem
+      :func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ x → lem
         where
           lem = (ℂ .isCategory) .IsCategory.assoc
     module _ {c : ℂ .Object} where
       eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁
       eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂
-      eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i)
-      eqNat i f = {!!}
-
+      eqNat
+                 : PathP (λ i → {A B : ℂ .Object} (f : Opposite ℂ .Arrow A B)
+                   →   Sets [ eqTrans i B ∘ prshf c .Functor.func→ f ]
+                     ≡ Sets [ prshf c .Functor.func→ f ∘ eqTrans i A ])
+                   ((:func→: (ℂ .𝟙 {c})) .proj₂) ((Fun .𝟙 {o = prshf c}) .proj₂)
+      eqNat = λ i f i' x₁ → {!ℂ ._⊕_ ? ?!}
+      -- eqNat i f = {!!}
+      -- Sets ._⊕_ (eq₁ i B) (prshf A .func→ f) ≡ Sets ._⊕_ (prshf B .func→ f) (eq₁ i A)
       :ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
-      :ident: i = eqTrans i , eqNat i
+      :ident: = NaturalTransformation≡ eqTrans eqNat
 
   yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
   yoneda = record
diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda
index bc3baae..c92defe 100644
--- a/src/Cat/Cubical.agda
+++ b/src/Cat/Cubical.agda
@@ -18,7 +18,7 @@ open import Cat.Functor
 -- categorical version of CTT
 
 module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
-  open Category
+  open Category hiding (_∘_)
   open Functor
   open import Function
   open import Cubical
@@ -53,7 +53,7 @@ module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
       { Object = Obj
       ; Arrow = Arr
       ; 𝟙 = one
-      ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c}
+      ; _∘_ = λ {a b c} → _:⊕:_ {a} {b} {c}
       }
 
   Contexts = ℂ .Object
@@ -96,6 +96,6 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     { Object = Ns → Bool
     ; Arrow = Mor
     ; 𝟙 = {!!}
-    ; _⊕_ = {!!}
+    ; _∘_ = {!!}
     ; isCategory = {!!}
     }
diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda
index 8d97a08..056e142 100644
--- a/src/Cat/Functor.agda
+++ b/src/Cat/Functor.agda
@@ -6,7 +6,7 @@ open import Function
 
 open import Cat.Category
 
-open Category
+open Category hiding (_∘_)
 
 module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
   record IsFunctor