diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 3021268..a5d986e 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -15,10 +15,10 @@ open import Cat.Categories.Fun
 -- The category of categories
 module _ (ℓ ℓ' : Level) where
   RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
-  RawCategory.Object RawCat = Category ℓ ℓ'
-  RawCategory.Arrow  RawCat = Functor
-  RawCategory.𝟙      RawCat = Functors.identity
-  RawCategory._∘_    RawCat = F[_∘_]
+  RawCategory.Object   RawCat = Category ℓ ℓ'
+  RawCategory.Arrow    RawCat = Functor
+  RawCategory.identity RawCat = Functors.identity
+  RawCategory._∘_      RawCat = F[_∘_]
 
   -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
   -- however, form a groupoid! Therefore there is no (1-)category of
@@ -48,8 +48,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
         Obj = ℂ.Object × 𝔻.Object
         Arr  : Obj → Obj → Set ℓ'
         Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ]
-        𝟙 : {o : Obj} → Arr o o
-        𝟙 = ℂ.𝟙 , 𝔻.𝟙
+        identity : {o : Obj} → Arr o o
+        identity = ℂ.identity , 𝔻.identity
         _∘_ :
           {a b c : Obj} →
           Arr b c →
@@ -58,16 +58,16 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
         _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
 
       rawProduct : RawCategory ℓ ℓ'
-      RawCategory.Object rawProduct = Obj
-      RawCategory.Arrow  rawProduct = Arr
-      RawCategory.𝟙      rawProduct = 𝟙
-      RawCategory._∘_    rawProduct = _∘_
+      RawCategory.Object   rawProduct = Obj
+      RawCategory.Arrow    rawProduct = Arr
+      RawCategory.identity rawProduct = identity
+      RawCategory._∘_      rawProduct = _∘_
 
     open RawCategory rawProduct
 
     arrowsAreSets : ArrowsAreSets
     arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets}
-    isIdentity : IsIdentity 𝟙
+    isIdentity : IsIdentity identity
     isIdentity
       = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity)
       , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity)
@@ -202,14 +202,14 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
   module _ {c : Functor ℂ 𝔻 × ℂ.Object} where
     open Σ c renaming (proj₁ to F ; proj₂ to C)
 
-    ident : fmap {c} {c} (identityNT F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙
+    ident : fmap {c} {c} (identityNT F , ℂ.identity {A = snd c}) ≡ 𝔻.identity
     ident = begin
-      fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c})        ≡⟨⟩
-      fmap {c} {c} (idN F , ℂ.𝟙)               ≡⟨⟩
-      𝔻 [ identityTrans F C ∘ F.fmap ℂ.𝟙 ]    ≡⟨⟩
-      𝔻 [ 𝔻.𝟙 ∘ F.fmap ℂ.𝟙 ]                  ≡⟨ 𝔻.leftIdentity ⟩
-      F.fmap ℂ.𝟙                               ≡⟨ F.isIdentity ⟩
-      𝔻.𝟙                                       ∎
+      fmap {c} {c} (Category.identity (object ⊗ ℂ) {c}) ≡⟨⟩
+      fmap {c} {c} (idN F , ℂ.identity)                 ≡⟨⟩
+      𝔻 [ identityTrans F C ∘ F.fmap ℂ.identity ]       ≡⟨⟩
+      𝔻 [ 𝔻.identity ∘ F.fmap ℂ.identity ]              ≡⟨ 𝔻.leftIdentity ⟩
+      F.fmap ℂ.identity                                 ≡⟨ F.isIdentity ⟩
+      𝔻.identity                                        ∎
       where
         module F = Functor F
 
@@ -278,16 +278,16 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
       transpose : Functor 𝔸 object
       eq : F[ eval ∘ (parallelProduct transpose (Functors.identity {ℂ = ℂ})) ] ≡ F
       -- eq : F[ :eval: ∘ {!!} ] ≡ F
-      -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F
+      -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (identity Catℓ {o = ℂ})) ] ≡ F
       -- eq' : (Catℓ [ :eval: ∘
       --   (record { product = product } HasProducts.|×| transpose)
-      --   (𝟙 Catℓ)
+      --   (identity Catℓ)
       --   ])
       --   ≡ F
 
     -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
     -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [
-    -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose =
+    -- :eval: ∘ (parallelProduct F~ (identity Catℓ {o = ℂ}))] ≡ F) catTranspose =
     -- transpose , eq
 
 -- We don't care about filling out the holes below since they are anyways hidden
diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda
index f338343..5322b16 100644
--- a/src/Cat/Categories/Cube.agda
+++ b/src/Cat/Categories/Cube.agda
@@ -67,7 +67,7 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
     Rawℂ : RawCategory ℓ ℓ -- ℓo (lsuc lzero ⊔ ℓo)
     Raw.Object Rawℂ = FiniteDecidableSubset
     Raw.Arrow Rawℂ = Hom
-    Raw.𝟙 Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
+    Raw.identity Rawℂ {o} = inj₁ , λ { (i , ii) (j , jj) eq → Σ≡ eq {!refl!} }
     Raw._∘_ Rawℂ = {!!}
 
     postulate IsCategoryℂ : IsCategory Rawℂ
diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda
index 5ffde56..ff4fafc 100644
--- a/src/Cat/Categories/Fam.agda
+++ b/src/Cat/Categories/Fam.agda
@@ -11,9 +11,9 @@ module _ (ℓa ℓb : Level) where
     Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb)
     Arr : Object → Object → Set (ℓa ⊔ ℓb)
     Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x)))
-    𝟙 : {A : Object} → Arr A A
-    proj₁ 𝟙 = λ x → x
-    proj₂ 𝟙 = λ b → b
+    identity : {A : Object} → Arr A A
+    proj₁ identity = λ x → x
+    proj₂ identity = λ b → b
     _∘_ : {a b c : Object} → Arr b c → Arr a b → Arr a c
     (g , g') ∘ (f , f') = g Function.∘ f , g' Function.∘ f'
 
@@ -21,16 +21,16 @@ module _ (ℓa ℓb : Level) where
     RawFam = record
       { Object = Object
       ; Arrow = Arr
-      ; 𝟙 = λ { {A} → 𝟙 {A = A}}
+      ; identity = λ { {A} → identity {A = A}}
       ; _∘_ = λ {a b c} → _∘_ {a} {b} {c}
       }
 
-    open RawCategory RawFam hiding (Object ; 𝟙)
+    open RawCategory RawFam hiding (Object ; identity)
 
     isAssociative : IsAssociative
     isAssociative = Σ≡ refl refl
 
-    isIdentity : IsIdentity λ { {A} → 𝟙 {A} }
+    isIdentity : IsIdentity λ { {A} → identity {A} }
     isIdentity = (Σ≡ refl refl) , Σ≡ refl refl
 
     open import Cubical.NType.Properties
diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 1d262dd..29d6bbe 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -27,10 +27,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     module ℂ = Category ℂ
 
     RawFree : RawCategory ℓa (ℓa ⊔ ℓb)
-    RawCategory.Object RawFree = ℂ.Object
-    RawCategory.Arrow  RawFree = Path ℂ.Arrow
-    RawCategory.𝟙      RawFree = empty
-    RawCategory._∘_    RawFree = concatenate
+    RawCategory.Object   RawFree = ℂ.Object
+    RawCategory.Arrow    RawFree = Path ℂ.Arrow
+    RawCategory.identity RawFree = empty
+    RawCategory._∘_      RawFree = concatenate
 
     open RawCategory RawFree
 
@@ -52,7 +52,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     ident-l : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate empty p ≡ p
     ident-l = refl
 
-    isIdentity : IsIdentity 𝟙
+    isIdentity : IsIdentity identity
     isIdentity = ident-l , ident-r
 
     open Univalence isIdentity
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index 791ddc6..1cd2e0a 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -1,28 +1,28 @@
-{-# OPTIONS --allow-unsolved-metas --cubical #-}
+{-# OPTIONS --allow-unsolved-metas --cubical --caching #-}
 module Cat.Categories.Fun where
 
 open import Cat.Prelude
 
 open import Cat.Category
 open import Cat.Category.Functor
+import Cat.Category.NaturalTransformation
+  as NaturalTransformation
 
 module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
-  import Cat.Category.NaturalTransformation ℂ 𝔻
-    as NaturalTransformation
-  open NaturalTransformation public hiding (module Properties)
-  open NaturalTransformation.Properties
+  open NaturalTransformation ℂ 𝔻 public hiding (module Properties)
+  open NaturalTransformation.Properties ℂ 𝔻
   private
     module ℂ = Category ℂ
     module 𝔻 = Category 𝔻
 
     -- Functor categories. Objects are functors, arrows are natural transformations.
     raw : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd')
-    RawCategory.Object raw = Functor ℂ 𝔻
-    RawCategory.Arrow  raw = NaturalTransformation
-    RawCategory.𝟙      raw {F} = identity F
-    RawCategory._∘_    raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
+    RawCategory.Object   raw = Functor ℂ 𝔻
+    RawCategory.Arrow    raw = NaturalTransformation
+    RawCategory.identity raw {F} = identity F
+    RawCategory._∘_      raw {F} {G} {H} = NT[_∘_] {F} {G} {H}
 
-    open RawCategory raw
+    open RawCategory raw hiding (identity)
     open Univalence (λ {A} {B} {f} → isIdentity {F = A} {B} {f})
 
     module _ (F : Functor ℂ 𝔻) where
@@ -32,7 +32,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
       open Σ center renaming (proj₂ to isoF)
 
       module _ (cG : Σ[ G ∈ Object ] (F ≅ G)) where
-        open Σ cG     renaming (proj₁ to G   ; proj₂ to isoG)
+        open Σ cG renaming (proj₁ to G ; proj₂ to isoG)
         module G = Functor G
         open Σ isoG   renaming (proj₁ to θNT ; proj₂ to invθNT)
         open Σ invθNT renaming (proj₁ to ηNT ; proj₂ to areInv)
@@ -46,10 +46,10 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         -- g = T[ η ∘ θ ] {!!}
 
         ntF : NaturalTransformation F F
-        ntF = 𝟙 {A = F}
+        ntF = identity F
 
         ntG : NaturalTransformation G G
-        ntG = 𝟙 {A = G}
+        ntG = identity G
 
         idFunctor = Functors.identity
 
@@ -103,14 +103,14 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         -- The transformation will be the identity on 𝔻. Such an arrow has the
         -- type `A.omap A → A.omap A`. Which we can coerce to have the type
         -- `A.omap → B.omap` since `A` and `B` are equal.
-        coe𝟙 : Transformation A B
-        coe𝟙 X = coe coerceAB 𝔻.𝟙
+        coeidentity : Transformation A B
+        coeidentity X = coe coerceAB 𝔻.identity
 
         module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where
-          nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ]
+          nat' : 𝔻 [ coeidentity b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coeidentity a ]
           nat' = begin
-            (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
-            (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎
+            (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡⟨ {!!} ⟩
+            (𝔻 [ B.fmap f ∘ coeidentity a ]) ∎
 
         transs : (i : I) → Transformation A (p i)
         transs = {!!}
@@ -118,26 +118,26 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         natt : (i : I) → Natural A (p i) {!!}
         natt = {!!}
 
-        t : Natural A B coe𝟙
+        t : Natural A B coeidentity
         t = coe c (identityNatural A)
           where
-          c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙
+          c : Natural A A (identityTrans A) ≡ Natural A B coeidentity
           c = begin
             Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩
-            Natural A B coe𝟙 ∎
+            Natural A B coeidentity ∎
           -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!}
 
-        k : Natural A A (identityTrans A) → Natural A B coe𝟙
+        k : Natural A A (identityTrans A) → Natural A B coeidentity
         k n {a} {b} f = res
           where
-          res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ])
+          res : (𝔻 [ coeidentity b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coeidentity a ])
           res = {!!}
 
-        nat : Natural A B coe𝟙
+        nat : Natural A B coeidentity
         nat = nat'
 
         fromEq : NaturalTransformation A B
-        fromEq = coe𝟙 , nat
+        fromEq = coeidentity , nat
 
     module _ {A B : Functor ℂ 𝔻} where
       obverse : A ≡ B → A ≅ B
@@ -147,9 +147,9 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
         ob = fromEq p
         re : Arrow B A
         re = fromEq (sym p)
-        vr : _∘_ {A = A} {B} {A} re ob ≡ 𝟙 {A}
+        vr : _∘_ {A = A} {B} {A} re ob ≡ identity A
         vr = {!!}
-        rv : _∘_ {A = B} {A} {B} ob re ≡ 𝟙 {B}
+        rv : _∘_ {A = B} {A} {B} ob re ≡ identity B
         rv = {!!}
         isInverse : IsInverseOf {A} {B} ob re
         isInverse = vr , rv
@@ -183,23 +183,42 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
   Category.raw        Fun = raw
   Category.isCategory Fun = isCategory
 
--- module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
---   private
---     open import Cat.Categories.Sets
---     open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
+  private
+    open import Cat.Categories.Sets
+    open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+    module K = Fun (opposite ℂ) (𝓢𝓮𝓽 ℓ')
+    module F = Category K.Fun
 
---     -- Restrict the functors to Presheafs.
---     rawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
---     rawPresh = record
---       { Object = Presheaf ℂ
---       ; Arrow = NaturalTransformation
---       ; 𝟙 = λ {F} → identity F
---       ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
---       }
---     instance
---       isCategory : IsCategory rawPresh
---       isCategory = Fun.isCategory _ _
+    -- Restrict the functors to Presheafs.
+    raw : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+    raw = record
+      { Object = Presheaf ℂ
+      ; Arrow = NaturalTransformation
+      ; identity = λ {F} → identity F
+      ; _∘_ = λ {F G H} → NT[_∘_] {F = F} {G = G} {H = H}
+      }
 
---   Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
---   Category.raw        Presh = rawPresh
---   Category.isCategory Presh = isCategory
+    isCategory : IsCategory raw
+    isCategory = record
+      { isAssociative =
+        λ{ {A} {B} {C} {D} {f} {g} {h}
+        → F.isAssociative {A} {B} {C} {D} {f} {g} {h}
+        }
+      ; isIdentity =
+        λ{ {A} {B} {f}
+        → F.isIdentity {A} {B} {f}
+        }
+      ; arrowsAreSets =
+        λ{ {A} {B}
+        → F.arrowsAreSets {A} {B}
+        }
+      ; univalent =
+        λ{ {A} {B}
+        → F.univalent {A} {B}
+        }
+      }
+
+  Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
+  Category.raw        Presh = raw
+  Category.isCategory Presh = isCategory
diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda
index 5b44601..73d4bff 100644
--- a/src/Cat/Categories/Rel.agda
+++ b/src/Cat/Categories/Rel.agda
@@ -153,7 +153,7 @@ RawRel : RawCategory (lsuc lzero) (lsuc lzero)
 RawRel = record
   { Object = Set
   ; Arrow = λ S R → Subset (S × R)
-  ; 𝟙 = λ {S} → Diag S
+  ; identity = λ {S} → Diag S
   ; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
   }
 
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index f4c59fd..8536870 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -60,10 +60,10 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
 module _ (ℓ : Level) where
   private
     SetsRaw : RawCategory (lsuc ℓ) ℓ
-    RawCategory.Object SetsRaw = hSet ℓ
-    RawCategory.Arrow  SetsRaw (T , _) (U , _) = T → U
-    RawCategory.𝟙      SetsRaw = Function.id
-    RawCategory._∘_    SetsRaw = Function._∘′_
+    RawCategory.Object   SetsRaw = hSet ℓ
+    RawCategory.Arrow    SetsRaw (T , _) (U , _) = T → U
+    RawCategory.identity SetsRaw = Function.id
+    RawCategory._∘_      SetsRaw = Function._∘′_
 
     open RawCategory SetsRaw hiding (_∘_)
 
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 8408cf0..2576ee2 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -12,7 +12,7 @@
 --
 -- Data
 -- ----
--- 𝟙; the identity arrow
+-- identity; the identity arrow
 -- _∘_; function composition
 --
 -- Laws
@@ -48,10 +48,10 @@ import      Function
 record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   no-eta-equality
   field
-    Object : Set ℓa
-    Arrow  : Object → Object → Set ℓb
-    𝟙      : {A : Object} → Arrow A A
-    _∘_    : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
+    Object   : Set ℓa
+    Arrow    : Object → Object → Set ℓb
+    identity : {A : Object} → Arrow A A
+    _∘_      : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
 
   infixl 10 _∘_ _>>>_
 
@@ -82,7 +82,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B)
 
   IsInverseOf : ∀ {A B} → (Arrow A B) → (Arrow B A) → Set ℓb
-  IsInverseOf = λ f g → g ∘ f ≡ 𝟙 × f ∘ g ≡ 𝟙
+  IsInverseOf = λ f g → g ∘ f ≡ identity × f ∘ g ≡ identity
 
   Isomorphism : ∀ {A B} → (f : Arrow A B) → Set ℓb
   Isomorphism {A} {B} f = Σ[ g ∈ Arrow B A ] IsInverseOf f g
@@ -110,10 +110,10 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
   Terminal = Σ Object IsTerminal
 
   -- | Univalence is indexed by a raw category as well as an identity proof.
-  module Univalence (isIdentity : IsIdentity 𝟙) where
+  module Univalence (isIdentity : IsIdentity identity) where
     -- | The identity isomorphism
     idIso : (A : Object) → A ≅ A
-    idIso A = 𝟙 , 𝟙 , isIdentity
+    idIso A = identity , identity , isIdentity
 
     -- | Extract an isomorphism from an equality
     --
@@ -150,16 +150,16 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
   open RawCategory ℂ public
   field
     isAssociative : IsAssociative
-    isIdentity    : IsIdentity 𝟙
+    isIdentity    : IsIdentity identity
     arrowsAreSets : ArrowsAreSets
   open Univalence isIdentity public
   field
     univalent     : Univalent
 
-  leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f
+  leftIdentity : {A B : Object} {f : Arrow A B} → identity ∘ f ≡ f
   leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f})
 
-  rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f
+  rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ identity ≡ f
   rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f})
 
   ------------
@@ -171,24 +171,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
     iso→epi : Isomorphism f → Epimorphism {X = X} f
     iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
       g₀              ≡⟨ sym rightIdentity ⟩
-      g₀ ∘ 𝟙          ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
+      g₀ ∘ identity   ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
       g₀ ∘ (f ∘ f-)   ≡⟨ isAssociative ⟩
       (g₀ ∘ f) ∘ f-   ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
       (g₁ ∘ f) ∘ f-   ≡⟨ sym isAssociative ⟩
       g₁ ∘ (f ∘ f-)   ≡⟨ cong (_∘_ g₁) right-inv ⟩
-      g₁ ∘ 𝟙          ≡⟨ rightIdentity ⟩
+      g₁ ∘ identity   ≡⟨ rightIdentity ⟩
       g₁              ∎
 
     iso→mono : Isomorphism f → Monomorphism {X = X} f
     iso→mono (f- , left-inv , right-inv) g₀ g₁ eq =
       begin
       g₀            ≡⟨ sym leftIdentity ⟩
-      𝟙 ∘ g₀        ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
+      identity ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
       (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩
       f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
       f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩
       (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
-      𝟙 ∘ g₁        ≡⟨ leftIdentity ⟩
+      identity ∘ g₁ ≡⟨ leftIdentity ⟩
       g₁            ∎
 
     iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f
@@ -228,12 +228,12 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
           where
             geq : g ≡ g'
             geq = begin
-              g            ≡⟨ sym rightIdentity ⟩
-              g ∘ 𝟙        ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
-              g ∘ (f ∘ g') ≡⟨ isAssociative ⟩
-              (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩
-              𝟙 ∘ g'       ≡⟨ leftIdentity ⟩
-              g'           ∎
+              g             ≡⟨ sym rightIdentity ⟩
+              g ∘ identity  ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩
+              g ∘ (f ∘ g')  ≡⟨ isAssociative ⟩
+              (g ∘ f) ∘ g'  ≡⟨ cong (λ φ → φ ∘ g') η ⟩
+              identity ∘ g' ≡⟨ leftIdentity ⟩
+              g'            ∎
 
     propUnivalent : isProp Univalent
     propUnivalent a b i = propPi (λ iso → propIsContr) a b i
@@ -274,9 +274,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       Xprop f g = trans (sym (snd Xit f)) (snd Xit g)
       Yprop : isProp (Arrow Y Y)
       Yprop f g = trans (sym (snd Yit f)) (snd Yit g)
-      left : Y→X ∘ X→Y ≡ 𝟙
+      left : Y→X ∘ X→Y ≡ identity
       left = Xprop _ _
-      right : X→Y ∘ Y→X ≡ 𝟙
+      right : X→Y ∘ Y→X ≡ identity
       right = Yprop _ _
       iso : X ≅ Y
       iso = X→Y , Y→X , left , right
@@ -321,9 +321,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc
       Xprop f g = trans (sym (snd Xii f)) (snd Xii g)
       Yprop : isProp (Arrow Y Y)
       Yprop f g = trans (sym (snd Yii f)) (snd Yii g)
-      left : Y→X ∘ X→Y ≡ 𝟙
+      left : Y→X ∘ X→Y ≡ identity
       left = Yprop _ _
-      right : X→Y ∘ Y→X ≡ 𝟙
+      right : X→Y ∘ Y→X ≡ identity
       right = Xprop _ _
       iso : X ≅ Y
       iso = Y→X , X→Y , right , left
@@ -351,18 +351,18 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       -- adverse effects this may have.
       module Prop = X.Propositionality
 
-      isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ]
+      isIdentity : (λ _ → IsIdentity identity) [ X.isIdentity ≡ Y.isIdentity ]
       isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity
 
-      U : ∀ {a : IsIdentity 𝟙}
-        → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ]
+      U : ∀ {a : IsIdentity identity}
+        → (λ _ → IsIdentity identity) [ X.isIdentity ≡ a ]
         → (b : Univalent a)
         → Set _
       U eqwal univ =
         (λ i → Univalent (eqwal i))
         [ X.univalent ≡ univ ]
-      P : (y : IsIdentity 𝟙)
-        → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _
+      P : (y : IsIdentity identity)
+        → (λ _ → IsIdentity identity) [ X.isIdentity ≡ y ] → Set _
       P y eq = ∀ (univ : Univalent y) → U eq univ
       p : ∀ (b' : Univalent X.isIdentity)
         → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ]
@@ -426,14 +426,14 @@ module Opposite {ℓa ℓb : Level} where
     private
       module ℂ = Category ℂ
       opRaw : RawCategory ℓa ℓb
-      RawCategory.Object opRaw = ℂ.Object
-      RawCategory.Arrow  opRaw = Function.flip ℂ.Arrow
-      RawCategory.𝟙      opRaw = ℂ.𝟙
-      RawCategory._∘_    opRaw = Function.flip ℂ._∘_
+      RawCategory.Object   opRaw = ℂ.Object
+      RawCategory.Arrow    opRaw = Function.flip ℂ.Arrow
+      RawCategory.identity opRaw = ℂ.identity
+      RawCategory._∘_      opRaw = Function.flip ℂ._∘_
 
       open RawCategory opRaw
 
-      isIdentity : IsIdentity 𝟙
+      isIdentity : IsIdentity identity
       isIdentity = swap ℂ.isIdentity
 
       open Univalence isIdentity
@@ -530,7 +530,7 @@ module Opposite {ℓa ℓb : Level} where
       rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
       RawCategory.Object   (rawInv _) = Object
       RawCategory.Arrow    (rawInv _) = Arrow
-      RawCategory.𝟙        (rawInv _) = 𝟙
+      RawCategory.identity (rawInv _) = identity
       RawCategory._∘_      (rawInv _) = _∘_
 
     oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda
index 76652d2..4b4f017 100644
--- a/src/Cat/Category/Exponential.agda
+++ b/src/Cat/Category/Exponential.agda
@@ -16,11 +16,11 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
       field
         uniq
           : ∀ (A : Object) (f : ℂ [ A × B , C ])
-          → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
+          → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f)
 
     IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ')
     IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ])
-      → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f)
+      → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.identity ℂ ] ≡ f)
 
     record Exponential : Set (ℓ ⊔ ℓ') where
       field
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index bbdda14..c4a7346 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -30,7 +30,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
       fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
 
     IsIdentity : Set _
-    IsIdentity = {A : ℂ.Object} → fmap (ℂ.𝟙 {A}) ≡ 𝔻.𝟙 {omap A}
+    IsIdentity = {A : ℂ.Object} → fmap (ℂ.identity {A}) ≡ 𝔻.identity {omap A}
 
     IsDistributive : Set _
     IsDistributive = {A B C : ℂ.Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
@@ -150,10 +150,10 @@ module _ {ℓ0 ℓ1 ℓ2 ℓ3 ℓ4 ℓ5 : Level}
     isFunctor : IsFunctor A C raw
     isFunctor = record
       { isIdentity = begin
-        (F.fmap ∘ G.fmap) A.𝟙   ≡⟨ refl ⟩
-        F.fmap (G.fmap A.𝟙)     ≡⟨ cong F.fmap (G.isIdentity)⟩
-        F.fmap B.𝟙              ≡⟨ F.isIdentity ⟩
-        C.𝟙                     ∎
+        (F.fmap ∘ G.fmap) A.identity   ≡⟨ refl ⟩
+        F.fmap (G.fmap A.identity)     ≡⟨ cong F.fmap (G.isIdentity)⟩
+        F.fmap B.identity              ≡⟨ F.isIdentity ⟩
+        C.identity                     ∎
       ; isDistributive = dist
       }
 
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 8fc6c56..6383ab0 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -33,10 +33,10 @@ module Kleisli = Cat.Category.Monad.Kleisli
 
 -- | The monoidal- and kleisli presentation of monads are equivalent.
 module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-  open Cat.Category.NaturalTransformation ℂ ℂ
+  open Cat.Category.NaturalTransformation ℂ ℂ using (NaturalTransformation ; propIsNatural)
   private
     module ℂ = Category ℂ
-    open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
+    open ℂ using (Object ; Arrow ; identity ; _∘_ ; _>>>_)
     module M = Monoidal ℂ
     module K = Kleisli  ℂ
 
@@ -84,11 +84,11 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         inv-l = begin
           joinT X ∘ pureT (R.omap X) ≡⟨⟩
           join ∘ pure                 ≡⟨ proj₁ isInverse ⟩
-          𝟙                           ∎
+          identity                    ∎
         inv-r = begin
           joinT X ∘ R.fmap (pureT X) ≡⟨⟩
           join ∘ fmap pure            ≡⟨ proj₂ isInverse ⟩
-          𝟙                           ∎
+          identity                    ∎
 
     back : K.Monad → M.Monad
     Monoidal.Monad.raw     (back m) = backRaw     m
@@ -103,21 +103,21 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         bindEq {X} {Y} = begin
           K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
           (λ f → join ∘ fmap f)                  ≡⟨⟩
-          (λ f → bind (f >>> pure) >>> bind 𝟙)   ≡⟨ funExt lem ⟩
+          (λ f → bind (f >>> pure) >>> bind identity)   ≡⟨ funExt lem ⟩
           (λ f → bind f)                         ≡⟨⟩
           bind                                   ∎
           where
           lem : (f : Arrow X (omap Y))
-            → bind (f >>> pure) >>> bind 𝟙
+            → bind (f >>> pure) >>> bind identity
             ≡ bind f
           lem f = begin
-            bind (f >>> pure) >>> bind 𝟙
+            bind (f >>> pure) >>> bind identity
               ≡⟨ isDistributive _ _ ⟩
-            bind ((f >>> pure) >>> bind 𝟙)
+            bind ((f >>> pure) >>> bind identity)
               ≡⟨ cong bind ℂ.isAssociative ⟩
-            bind (f >>> (pure >>> bind 𝟙))
+            bind (f >>> (pure >>> bind identity))
               ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩
-            bind (f >>> 𝟙)
+            bind (f >>> identity)
               ≡⟨ cong bind ℂ.leftIdentity ⟩
             bind f ∎
 
@@ -146,10 +146,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         joinEq : ∀ {X} → KM.join ≡ joinT X
         joinEq {X} = begin
           KM.join                ≡⟨⟩
-          KM.bind 𝟙              ≡⟨⟩
-          bind 𝟙                 ≡⟨⟩
-          joinT X ∘ Rfmap 𝟙      ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
-          joinT X ∘ 𝟙            ≡⟨ ℂ.rightIdentity ⟩
+          KM.bind identity              ≡⟨⟩
+          bind identity                 ≡⟨⟩
+          joinT X ∘ Rfmap identity      ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩
+          joinT X ∘ identity            ≡⟨ ℂ.rightIdentity ⟩
           joinT X                ∎
 
         fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap
@@ -161,7 +161,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
           Rfmap (f >>> pureT B) >>> joinT B        ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩
           Rfmap f >>> Rfmap (pureT B) >>> joinT B  ≡⟨ ℂ.isAssociative ⟩
           joinT B ∘ Rfmap (pureT B) ∘ Rfmap f      ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩
-          𝟙 ∘ Rfmap f                              ≡⟨ ℂ.leftIdentity ⟩
+          identity ∘ Rfmap f                       ≡⟨ ℂ.leftIdentity ⟩
           Rfmap f                                  ∎
           )
 
@@ -183,8 +183,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
       joinTEq = funExt (λ X → begin
         M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
         KM.join ≡⟨⟩
-        joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
-        joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩
+        joinT X ∘ Rfmap identity ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
+        joinT X ∘ identity ≡⟨ ℂ.rightIdentity ⟩
         joinT X ∎)
 
       joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))
diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda
index bf79a5f..dc40f1c 100644
--- a/src/Cat/Category/Monad/Kleisli.agda
+++ b/src/Cat/Category/Monad/Kleisli.agda
@@ -12,11 +12,13 @@ open import Cat.Categories.Fun
 
 -- "A monad in the Kleisli form" [voe]
 module Cat.Category.Monad.Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
-open import Cat.Category.NaturalTransformation ℂ ℂ hiding (propIsNatural)
+open import Cat.Category.NaturalTransformation ℂ ℂ
+  using (NaturalTransformation ; Transformation ; Natural)
+
 private
   ℓ = ℓa ⊔ ℓb
   module ℂ = Category ℂ
-  open ℂ using (Arrow ; 𝟙 ; Object ; _∘_ ; _>>>_)
+  open ℂ using (Arrow ; identity ; Object ; _∘_ ; _>>>_)
 
 -- | Data for a monad.
 --
@@ -40,7 +42,7 @@ record RawMonad : Set ℓ where
 
   -- | Flattening nested monads.
   join : {A : Object} → ℂ [ omap (omap A) , omap A ]
-  join = bind 𝟙
+  join = bind identity
 
   ------------------
   -- * Monad laws --
@@ -49,7 +51,7 @@ record RawMonad : Set ℓ where
   -- There may be better names than what I've chosen here.
 
   IsIdentity     = {X : Object}
-    → bind pure ≡ 𝟙 {omap X}
+    → bind pure ≡ identity {omap X}
   IsNatural      = {X Y : Object}   (f : ℂ [ X , omap Y ])
     → pure >>> (bind f) ≡ f
   IsDistributive = {X Y Z : Object} (g : ℂ [ Y , omap Z ]) (f : ℂ [ X , omap Y ])
@@ -67,7 +69,7 @@ record RawMonad : Set ℓ where
   IsNaturalForeign = {X : Object} → join {X} ∘ fmap join ≡ join ∘ join
 
   IsInverse : Set _
-  IsInverse = {X : Object} → join {X} ∘ pure ≡ 𝟙 × join {X} ∘ fmap pure ≡ 𝟙
+  IsInverse = {X : Object} → join {X} ∘ pure ≡ identity × join {X} ∘ fmap pure ≡ identity
 
 record IsMonad (raw : RawMonad) : Set ℓ where
   open RawMonad raw public
@@ -100,9 +102,9 @@ record IsMonad (raw : RawMonad) : Set ℓ where
 
     isFunctorR : IsFunctor ℂ ℂ rawR
     IsFunctor.isIdentity isFunctorR = begin
-      bind (pure ∘ 𝟙) ≡⟨ cong bind (ℂ.rightIdentity) ⟩
-      bind pure       ≡⟨ isIdentity ⟩
-      𝟙               ∎
+      bind (pure ∘ identity) ≡⟨ cong bind (ℂ.rightIdentity) ⟩
+      bind pure              ≡⟨ isIdentity ⟩
+      identity               ∎
 
     IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
       bind (pure ∘ (g ∘ f))             ≡⟨⟩
@@ -137,29 +139,29 @@ record IsMonad (raw : RawMonad) : Set ℓ where
     joinN : Natural R² R joinT
     joinN f = begin
       join       ∘ R².fmap f  ≡⟨⟩
-      bind 𝟙     ∘ R².fmap f  ≡⟨⟩
-      R².fmap f >>> bind 𝟙    ≡⟨⟩
-      fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
-      fmap (bind (f >>> pure)) >>> bind 𝟙          ≡⟨⟩
-      bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
+      bind identity     ∘ R².fmap f  ≡⟨⟩
+      R².fmap f >>> bind identity    ≡⟨⟩
+      fmap (fmap f) >>> bind identity ≡⟨⟩
+      fmap (bind (f >>> pure)) >>> bind identity          ≡⟨⟩
+      bind (bind (f >>> pure) >>> pure) >>> bind identity
         ≡⟨ isDistributive _ _ ⟩
-      bind ((bind (f >>> pure) >>> pure) >=> 𝟙)
+      bind ((bind (f >>> pure) >>> pure) >=> identity)
         ≡⟨⟩
-      bind ((bind (f >>> pure) >>> pure) >>> bind 𝟙)
+      bind ((bind (f >>> pure) >>> pure) >>> bind identity)
         ≡⟨ cong bind ℂ.isAssociative ⟩
-      bind (bind (f >>> pure) >>> (pure >>> bind 𝟙))
+      bind (bind (f >>> pure) >>> (pure >>> bind identity))
         ≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩
-      bind (bind (f >>> pure) >>> 𝟙)
+      bind (bind (f >>> pure) >>> identity)
         ≡⟨ cong bind ℂ.leftIdentity ⟩
       bind (bind (f >>> pure))
         ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩
-      bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩
-      bind (𝟙 >=> (f >>> pure))
+      bind (identity >>> bind (f >>> pure)) ≡⟨⟩
+      bind (identity >=> (f >>> pure))
         ≡⟨ sym (isDistributive _ _) ⟩
-      bind 𝟙     >>> bind (f >>> pure)    ≡⟨⟩
-      bind 𝟙     >>> fmap f    ≡⟨⟩
-      bind 𝟙     >>> R.fmap f ≡⟨⟩
-      R.fmap f  ∘ bind 𝟙      ≡⟨⟩
+      bind identity     >>> bind (f >>> pure)    ≡⟨⟩
+      bind identity     >>> fmap f    ≡⟨⟩
+      bind identity     >>> R.fmap f ≡⟨⟩
+      R.fmap f  ∘ bind identity      ≡⟨⟩
       R.fmap f  ∘ join        ∎
 
   pureNT : NaturalTransformation R⁰ R
@@ -173,20 +175,20 @@ record IsMonad (raw : RawMonad) : Set ℓ where
   isNaturalForeign : IsNaturalForeign
   isNaturalForeign = begin
     fmap join >>> join ≡⟨⟩
-    bind (join >>> pure) >>> bind 𝟙
+    bind (join >>> pure) >>> bind identity
       ≡⟨ isDistributive _ _ ⟩
-    bind ((join >>> pure) >>> bind 𝟙)
+    bind ((join >>> pure) >>> bind identity)
       ≡⟨ cong bind ℂ.isAssociative ⟩
-    bind (join >>> (pure >>> bind 𝟙))
+    bind (join >>> (pure >>> bind identity))
       ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩
-    bind (join >>> 𝟙)
+    bind (join >>> identity)
       ≡⟨ cong bind ℂ.leftIdentity ⟩
     bind join           ≡⟨⟩
-    bind (bind 𝟙)
+    bind (bind identity)
       ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩
-    bind (𝟙 >>> bind 𝟙) ≡⟨⟩
-    bind (𝟙 >=> 𝟙)      ≡⟨ sym (isDistributive _ _) ⟩
-    bind 𝟙 >>> bind 𝟙   ≡⟨⟩
+    bind (identity >>> bind identity) ≡⟨⟩
+    bind (identity >=> identity)      ≡⟨ sym (isDistributive _ _) ⟩
+    bind identity >>> bind identity   ≡⟨⟩
     join >>> join       ∎
 
   isInverse : IsInverse
@@ -194,21 +196,21 @@ record IsMonad (raw : RawMonad) : Set ℓ where
     where
     inv-l = begin
       pure >>> join   ≡⟨⟩
-      pure >>> bind 𝟙 ≡⟨ isNatural _ ⟩
-      𝟙 ∎
+      pure >>> bind identity ≡⟨ isNatural _ ⟩
+      identity ∎
     inv-r = begin
       fmap pure >>> join ≡⟨⟩
-      bind (pure >>> pure) >>> bind 𝟙
+      bind (pure >>> pure) >>> bind identity
         ≡⟨ isDistributive _ _ ⟩
-      bind ((pure >>> pure) >=> 𝟙) ≡⟨⟩
-      bind ((pure >>> pure) >>> bind 𝟙)
+      bind ((pure >>> pure) >=> identity) ≡⟨⟩
+      bind ((pure >>> pure) >>> bind identity)
         ≡⟨ cong bind ℂ.isAssociative ⟩
-      bind (pure >>> (pure >>> bind 𝟙))
+      bind (pure >>> (pure >>> bind identity))
         ≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩
-      bind (pure >>> 𝟙)
+      bind (pure >>> identity)
         ≡⟨ cong bind ℂ.leftIdentity ⟩
       bind pure ≡⟨ isIdentity ⟩
-      𝟙 ∎
+      identity ∎
 
 record Monad : Set ℓ where
   field
diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda
index 69f3865..56319c2 100644
--- a/src/Cat/Category/Monad/Monoidal.agda
+++ b/src/Cat/Category/Monad/Monoidal.agda
@@ -16,8 +16,10 @@ module Cat.Category.Monad.Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb
 private
   ℓ = ℓa ⊔ ℓb
 
-open Category ℂ using (Object ; Arrow ; 𝟙 ; _∘_)
+open Category ℂ using (Object ; Arrow ; identity ; _∘_)
 open import Cat.Category.NaturalTransformation ℂ ℂ
+  using (NaturalTransformation ; Transformation ; Natural)
+
 record RawMonad : Set ℓ where
   field
     R      : EndoFunctor ℂ
@@ -47,8 +49,8 @@ record RawMonad : Set ℓ where
     → joinT X ∘ Rfmap (joinT X) ≡ joinT X ∘ joinT (Romap X)
   IsInverse : Set _
   IsInverse = {X : Object}
-    → joinT X ∘ pureT (Romap X) ≡ 𝟙
-    × joinT X ∘ Rfmap (pureT X) ≡ 𝟙
+    → joinT X ∘ pureT (Romap X) ≡ identity
+    × joinT X ∘ Rfmap (pureT X) ≡ identity
   IsNatural = ∀ {X Y} f → joinT Y ∘ Rfmap f ∘ pureT X ≡ f
   IsDistributive = ∀ {X Y Z} (g : Arrow Y (Romap Z)) (f : Arrow X (Romap Y))
     → joinT Z ∘ Rfmap g ∘ (joinT Y ∘ Rfmap f)
@@ -70,7 +72,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where
     joinT Y ∘ (R.fmap f ∘ pureT X)   ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
     joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
     joinT Y ∘ pureT (R.omap Y) ∘ f   ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
-    𝟙 ∘ f                            ≡⟨ ℂ.leftIdentity ⟩
+    identity ∘ f                     ≡⟨ ℂ.leftIdentity ⟩
     f                                ∎
 
   isDistributive : IsDistributive
diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda
index a478aee..0b4d784 100644
--- a/src/Cat/Category/NaturalTransformation.agda
+++ b/src/Cat/Category/NaturalTransformation.agda
@@ -31,7 +31,7 @@ module Cat.Category.NaturalTransformation
   {ℓc ℓc' ℓd ℓd' : Level}
   (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
 
-open Category using (Object ; 𝟙)
+open Category using (Object)
 private
   module ℂ = Category ℂ
   module 𝔻 = Category 𝔻
@@ -63,14 +63,14 @@ module _ (F G : Functor ℂ 𝔻) where
   NaturalTransformation≡ eq = lemSig propIsNatural _ _ eq
 
 identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
-identityTrans F C = 𝟙 𝔻
+identityTrans F C = 𝔻.identity
 
 identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
 identityNatural F {A = A} {B = B} f = begin
   𝔻 [ identityTrans F B ∘ F→ f ]  ≡⟨⟩
-  𝔻 [ 𝟙 𝔻 ∘  F→ f ]              ≡⟨ 𝔻.leftIdentity ⟩
+  𝔻 [ 𝔻.identity ∘  F→ f ]       ≡⟨ 𝔻.leftIdentity ⟩
   F→ f                            ≡⟨ sym 𝔻.rightIdentity ⟩
-  𝔻 [ F→ f ∘ 𝟙 𝔻 ]               ≡⟨⟩
+  𝔻 [ F→ f ∘ 𝔻.identity ]        ≡⟨⟩
   𝔻 [ F→ f ∘ identityTrans F A ]  ∎
   where
     module F = Functor F
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 03f6c4a..e956377 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -134,7 +134,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           ( ℂ [ ya ∘ xy ] ≡ xa)
           × ℂ [ yb ∘ xy ] ≡ xb
           }
-      ; 𝟙 = λ{ {A , f , g} → ℂ.𝟙 {A} , ℂ.rightIdentity , ℂ.rightIdentity}
+      ; identity = λ{ {A , f , g} → ℂ.identity {A} , ℂ.rightIdentity , ℂ.rightIdentity}
       ; _∘_ = λ { {A , a0 , a1} {B , b0 , b1} {C , c0 , c1} (f , f0 , f1) (g , g0 , g1)
         → (f ℂ.∘ g)
           , (begin
@@ -169,24 +169,24 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
       s0 = ℂ.isAssociative {f = f} {g} {h}
 
 
-    isIdentity : IsIdentity 𝟙
+    isIdentity : IsIdentity identity
     isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = leftIdentity , rightIdentity
       where
-      leftIdentity : 𝟙 ∘ (f , f0 , f1) ≡ (f , f0 , f1)
+      leftIdentity : identity ∘ (f , f0 , f1) ≡ (f , f0 , f1)
       leftIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
         where
-        L = 𝟙 ∘ (f , f0 , f1)
+        L = identity ∘ (f , f0 , f1)
         R : Arrow AA BB
         R = f , f0 , f1
         l : proj₁ L ≡ proj₁ R
         l = ℂ.leftIdentity
-      rightIdentity : (f , f0 , f1) ∘ 𝟙 ≡ (f , f0 , f1)
+      rightIdentity : (f , f0 , f1) ∘ identity ≡ (f , f0 , f1)
       rightIdentity i = l i , lemPropF propEqs l {proj₂ L} {proj₂ R} i
         where
-        L = (f , f0 , f1) ∘ 𝟙
+        L = (f , f0 , f1) ∘ identity
         R : Arrow AA BB
         R = (f , f0 , f1)
-        l : ℂ [ f ∘ ℂ.𝟙 ] ≡ f
+        l : ℂ [ f ∘ ℂ.identity ] ≡ f
         l = ℂ.rightIdentity
 
     arrowsAreSets : ArrowsAreSets
diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index 1efc90e..afea823 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -52,7 +52,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
     isIdentity : IsIdentity
     isIdentity {c} = lemSig prp _ _ eq
       where
-      eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c)
+      eq : (λ C x → ℂ [ ℂ.identity ∘ x ]) ≡ identityTrans (presheaf c)
       eq = funExt λ A → funExt λ B → ℂ.leftIdentity
       prp = F.naturalIsProp _ _ {F = presheaf c} {presheaf c}