From b0c2da630e8a2496ae7c550d6f479ea936d404aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Fri, 19 Nov 2021 13:10:09 +0100
Subject: [PATCH] Clean category theory (#624)

* delete redundant file

* lots of cleaning (in particular make argument to id implicit)

* remove duplicate yoneda code
---
 Cubical/Categories/Adjoint.agda               | 38 ++++----
 Cubical/Categories/Category.agda              |  4 -
 Cubical/Categories/Category/Base.agda         | 40 +++-----
 Cubical/Categories/Category/Properties.agda   | 29 +++---
 .../Categories/Constructions/Elements.agda    | 20 ++--
 Cubical/Categories/Constructions/Slice.agda   | 44 ++++-----
 Cubical/Categories/Functor/Base.agda          | 48 ++++------
 Cubical/Categories/Functor/Properties.agda    |  8 +-
 Cubical/Categories/Instances/CommRings.agda   |  2 +-
 Cubical/Categories/Instances/Cospan.agda      |  7 +-
 Cubical/Categories/Instances/Functors.agda    |  3 +-
 Cubical/Categories/Instances/Rings.agda       |  2 +-
 Cubical/Categories/Instances/Sets.agda        | 23 ++---
 Cubical/Categories/Limits.agda                |  1 -
 Cubical/Categories/Limits/Base.agda           |  6 +-
 Cubical/Categories/Limits/Pullback.agda       |  6 +-
 Cubical/Categories/Limits/Terminal.agda       |  8 +-
 Cubical/Categories/Morphism.agda              | 49 +++++-----
 .../NaturalTransformation/Base.agda           |  9 +-
 .../NaturalTransformation/Properties.agda     |  1 +
 Cubical/Categories/Presheaf/Base.agda         | 63 +------------
 Cubical/Categories/Presheaf/KanExtension.agda | 28 +++---
 Cubical/Categories/Presheaf/Properties.agda   | 14 +--
 Cubical/Categories/Sets.agda                  | 93 -------------------
 Cubical/Categories/Yoneda.agda                | 26 +++---
 25 files changed, 202 insertions(+), 370 deletions(-)
 delete mode 100644 Cubical/Categories/Sets.agda

diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda
index 70ee182799..cbe7dd6afe 100644
--- a/Cubical/Categories/Adjoint.agda
+++ b/Cubical/Categories/Adjoint.agda
@@ -68,8 +68,8 @@ module UnitCounit where
     ⦃ isCatC : isCategory C ⦄ ⦃ isCatD : isCategory D ⦄
     (η : 𝟙⟨ C ⟩ ⇒ (funcComp G F))
     (ε : (funcComp F G) ⇒ 𝟙⟨ D ⟩)
-    (Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id (F ⟅ c ⟆))
-    (Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id (G ⟅ d ⟆))
+    (Δ₁ : ∀ c → F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ≡ D .id)
+    (Δ₂ : ∀ d → η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫ ≡ C .id)
     where
 
     make⊣ : F ⊣ G
@@ -170,27 +170,27 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
         -- ETA
 
         -- trivial commutative diagram between identities in D
-        commInD : ∀ {x y} (f : C [ x , y ]) → (D .id _) ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _)
+        commInD : ∀ {x y} (f : C [ x , y ]) → D .id ⋆⟨ D ⟩ F ⟪ f ⟫ ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id
         commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _)
 
-        sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ (D .id _) ♭ ♯
+        sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯
         sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _))
 
         η' : 𝟙⟨ C ⟩ ⇒ G ∘F F
-        η' .N-ob x = (D .id _) ♭
+        η' .N-ob x = D .id ♭
         η' .N-hom f = sym (fst (adjNat') (commInD f ∙ sharpen1 f))
 
         -- EPSILON
 
         -- trivial commutative diagram between identities in C
-        commInC : ∀ {x y} (g : D [ x , y ]) → (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ (C .id _)
+        commInC : ∀ {x y} (g : D [ x , y ]) → C .id ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ G ⟪ g ⟫ ⋆⟨ C ⟩ C .id
         commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _)
 
-        sharpen2 : ∀ {x y} (g : D [ x , y ]) → (C .id _ ♯ ♭) ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ (C .id _) ⋆⟨ C ⟩ G ⟪ g ⟫
+        sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫
         sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _)
 
         ε' : F ∘F G ⇒ 𝟙⟨ D ⟩
-        ε' .N-ob x = (C .id _) ♯
+        ε' .N-ob x  = C .id ♯
         ε' .N-hom g = sym (snd adjNat' (sharpen2 g ∙ commInC g))
 
         -- DELTA 1
@@ -209,9 +209,9 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
             → (idTrans F) ⟦ c ⟧ ≡ (seqTransP F-assoc (F ∘ʳ η') (ε' ∘ˡ F) .N-ob c)
         body c = (idTrans F) ⟦ c ⟧
               ≡⟨ refl ⟩
-                D .id _
+                D .id
               ≡⟨ sym (D .⋆IdL _) ⟩
-                D .id _ ⋆⟨ D ⟩ D .id _
+                D .id ⋆⟨ D ⟩ D .id
               ≡⟨ snd adjNat' (cong (λ v → (η' ⟦ c ⟧) ⋆⟨ C ⟩ v) (G .F-id)) ⟩
                 F ⟪ η' ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε' ⟦ F ⟅ c ⟆ ⟧
               ≡⟨ sym (expL c) ⟩
@@ -226,16 +226,16 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
         -- DELTA 2
 
         body2 : ∀ (d)
-            →  seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧) ≡ C .id (G .F-ob d)
+            →  seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧) ≡ C .id
         body2 d = seqP {C = C} {p = refl} ((η' ∘ˡ G) ⟦ d ⟧) ((G ∘ʳ ε') ⟦ d ⟧)
                 ≡⟨ seqP≡seq {C = C} _ _ ⟩
                   ((η' ∘ˡ G) ⟦ d ⟧) ⋆⟨ C ⟩ ((G ∘ʳ ε') ⟦ d ⟧)
                 ≡⟨ refl ⟩
                   (η' ⟦ G ⟅ d ⟆ ⟧) ⋆⟨ C ⟩ (G ⟪ ε' ⟦ d ⟧ ⟫)
                 ≡⟨ fst adjNat' (cong (λ v → v ⋆⟨ D ⟩ (ε' ⟦ d ⟧)) (sym (F .F-id))) ⟩
-                  C .id _ ⋆⟨ C ⟩ C .id _
+                  C .id ⋆⟨ C ⟩ C .id
                 ≡⟨ C .⋆IdL _ ⟩
-                  C .id (G .F-ob d)
+                  C .id
                 ∎
 
         Δ₂' : PathP (λ i → NatTrans (F-rUnit {F = G} i) (F-lUnit {F = G} i))
@@ -251,20 +251,20 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
 
     -- helper functions for working with this Adjoint definition
 
-    δ₁ : ∀ {c} → (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧) ≡ D .id _
+    δ₁ : ∀ {c} → (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧) ≡ D .id
     δ₁ {c} = (F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧)
           ≡⟨ sym (seqP≡seq {C = D} _ _) ⟩
             seqP {C = D} {p = refl} (F ⟪ η ⟦ c ⟧ ⟫) (ε ⟦ F ⟅ c ⟆ ⟧)
           ≡⟨ (λ j → (Δ₁ j) .N-ob c) ⟩
-            D .id _
+            D .id
           ∎
 
-    δ₂ : ∀ {d} → (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) ≡ C .id _
+    δ₂ : ∀ {d} → (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) ≡ C .id
     δ₂ {d} = (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
         ≡⟨ sym (seqP≡seq {C = C} _ _) ⟩
           seqP {C = C} {p = refl} (η ⟦ G ⟅ d ⟆ ⟧) (G ⟪ ε ⟦ d ⟧ ⟫)
         ≡⟨ (λ j → (Δ₂ j) .N-ob d) ⟩
-          C .id _
+          C .id
         ∎
 
 
@@ -287,7 +287,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
       ≡⟨ C .⋆Assoc _ _ _ ⟩
         g ⋆⟨ C ⟩ (η ⟦ G ⟅ d ⟆ ⟧ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫)
       ≡⟨ lPrecatWhisker {C = C} _ _ _ δ₂ ⟩
-        g ⋆⟨ C ⟩ C .id _
+        g ⋆⟨ C ⟩ C .id
       ≡⟨ C .⋆IdR _ ⟩
         g
       ∎
@@ -307,7 +307,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} (F : Functor
         F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ ε ⟦ F ⟅ c ⟆ ⟧ ⋆⟨ D ⟩ f
       -- apply triangle identity
       ≡⟨ rPrecatWhisker {C = D} _ _ _ δ₁ ⟩
-        (D .id _) ⋆⟨ D ⟩ f
+        D .id ⋆⟨ D ⟩ f
       ≡⟨ D .⋆IdL _ ⟩
         f
       ∎
diff --git a/Cubical/Categories/Category.agda b/Cubical/Categories/Category.agda
index 54f2d8ef9a..8601f97f7b 100644
--- a/Cubical/Categories/Category.agda
+++ b/Cubical/Categories/Category.agda
@@ -13,12 +13,8 @@
     - pathToIso : Turns a path between two objects into an isomorphism between them
     - opposite categories
 
-
 -}
-
 {-# OPTIONS --safe #-}
-
-
 module Cubical.Categories.Category where
 
 open import Cubical.Categories.Category.Base public
diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda
index 5effdaab03..d3f261f91f 100644
--- a/Cubical/Categories/Category/Base.agda
+++ b/Cubical/Categories/Category/Base.agda
@@ -1,9 +1,6 @@
 {-# OPTIONS --safe #-}
-
-
 module Cubical.Categories.Category.Base where
 
-open import Cubical.Core.Glue
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv
@@ -13,17 +10,15 @@ private
     ℓ ℓ' : Level
 
 -- Precategories
-
 record Precategory ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   -- no-eta-equality ; NOTE: need eta equality for `opop`
   field
     ob : Type ℓ
     Hom[_,_] : ob → ob → Type ℓ'
-    id : ∀ x → Hom[ x , x ]
-    _⋆_ : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
-    -- TODO: change these to implicit argument
-    ⋆IdL : ∀ {x y : ob} (f : Hom[ x , y ]) → (id x) ⋆ f ≡ f
-    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ (id y) ≡ f
+    id   : ∀ {x} → Hom[ x , x ]
+    _⋆_  : ∀ {x y z} (f : Hom[ x , y ]) (g : Hom[ y , z ]) → Hom[ x , z ]
+    ⋆IdL : ∀ {x y} (f : Hom[ x , y ]) → id ⋆ f ≡ f
+    ⋆IdR : ∀ {x y} (f : Hom[ x , y ]) → f ⋆ id ≡ f
     ⋆Assoc : ∀ {u v w x} (f : Hom[ u , v ]) (g : Hom[ v , w ]) (h : Hom[ w , x ]) → (f ⋆ g) ⋆ h ≡ f ⋆ (g ⋆ h)
 
   -- composition: alternative to diagramatic order
@@ -34,11 +29,10 @@ open Precategory
 
 
 -- Helpful syntax/notation
-
 _[_,_] : (C : Precategory ℓ ℓ') → (x y : C .ob) → Type ℓ'
 _[_,_] = Hom[_,_]
 
--- needed to define this in order to be able to make the subsequence syntax declaration
+-- Needed to define this in order to be able to make the subsequence syntax declaration
 seq' : ∀ (C : Precategory ℓ ℓ') {x y z} (f : C [ x , y ]) (g : C [ y , z ]) → C [ x , z ]
 seq' = _⋆_
 
@@ -54,46 +48,42 @@ syntax comp' C g f = g ∘⟨ C ⟩ f
 
 
 -- Categories
-
 record isCategory (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
   field
     isSetHom : ∀ {x y} → isSet (C [ x , y ])
 
 -- Isomorphisms and paths in precategories
 
-record CatIso {C : Precategory ℓ ℓ'} (x y : C .Precategory.ob) : Type ℓ' where
+record CatIso {C : Precategory ℓ ℓ'} (x y : C .ob) : Type ℓ' where
   constructor catiso
   field
     mor : C [ x , y ]
     inv : C [ y , x ]
-    sec : inv ⋆⟨ C ⟩ mor ≡ C .id y
-    ret : mor ⋆⟨ C ⟩ inv ≡ C .id x
+    sec : inv ⋆⟨ C ⟩ mor ≡ C .id
+    ret : mor ⋆⟨ C ⟩ inv ≡ C .id
 
 
-pathToIso : {C : Precategory ℓ ℓ'} (x y : C .ob) (p : x ≡ y) → CatIso {C = C} x y
-pathToIso {C = C} x y p = J (λ z _ → CatIso x z) (catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
+pathToIso : {C : Precategory ℓ ℓ'} {x y : C .ob} (p : x ≡ y) → CatIso {C = C} x y
+pathToIso {C = C} p = J (λ z _ → CatIso _ z) (catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)) p
   where
-    idx = C .id x
+    idx = C .id
 
 -- Univalent Categories
 
 record isUnivalent (C : Precategory ℓ ℓ') : Type (ℓ-max ℓ ℓ') where
   field
-    univ : (x y : C .ob) → isEquiv (pathToIso {C = C} x y)
+    univ : (x y : C .ob) → isEquiv (pathToIso {C = C} {x = x} {y = y})
 
   -- package up the univalence equivalence
   univEquiv : ∀ (x y : C .ob) → (x ≡ y) ≃ (CatIso x y)
-  univEquiv x y = (pathToIso {C = C} x y) , (univ x y)
+  univEquiv x y = pathToIso , univ x y
 
   -- The function extracting paths from category-theoretic isomorphisms.
   CatIsoToPath : {x y : C .ob} (p : CatIso x y) → x ≡ y
   CatIsoToPath {x = x} {y = y} p =
     equivFun (invEquiv (univEquiv x y)) p
 
-open isUnivalent public
-
--- Opposite Categories
-
+-- Opposite category
 _^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
 (C ^op) .ob = C .ob
 (C ^op) .Hom[_,_] x y = C .Hom[_,_] y x
@@ -102,5 +92,3 @@ _^op : Precategory ℓ ℓ' → Precategory ℓ ℓ'
 (C ^op) .⋆IdL = C .⋆IdR
 (C ^op) .⋆IdR = C .⋆IdL
 (C ^op) .⋆Assoc f g h = sym (C .⋆Assoc _ _ _)
-
-open isCategory public
diff --git a/Cubical/Categories/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda
index 35fc7b6a44..1d8229bd99 100644
--- a/Cubical/Categories/Category/Properties.agda
+++ b/Cubical/Categories/Category/Properties.agda
@@ -1,12 +1,10 @@
 {-# OPTIONS --safe #-}
-
-
 module Cubical.Categories.Category.Properties where
 
-open import Cubical.Core.Glue
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
-open import Cubical.Categories.Category.Base hiding (isSetHom)
+
+open import Cubical.Categories.Category.Base
 
 open Precategory
 
@@ -32,36 +30,37 @@ module _ {C : Precategory ℓ ℓ'} ⦃ isC : isCategory C ⦄ where
   isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom {y = a})
 
 
-
 -- opposite of opposite is definitionally equal to itself
-involutiveOp : ∀ {C : Precategory ℓ ℓ'} → (C ^op) ^op ≡ C
+involutiveOp : ∀ {C : Precategory ℓ ℓ'} → C ^op ^op ≡ C
 involutiveOp = refl
 
 module _ {C : Precategory ℓ ℓ'} where
   -- Other useful operations on categories
 
   -- whisker the parallel morphisms g and g' with f
-  lPrecatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g') → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
+  lPrecatWhisker : {x y z : C .ob} (f : C [ x , y ]) (g g' : C [ y , z ]) (p : g ≡ g')
+                 → f ⋆⟨ C ⟩ g ≡ f ⋆⟨ C ⟩ g'
   lPrecatWhisker f _ _ p = cong (_⋆_ C f) p
 
-  rPrecatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f') → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g
+  rPrecatWhisker : {x y z : C .ob} (f f' : C [ x , y ]) (g : C [ y , z ]) (p : f ≡ f')
+                 → f ⋆⟨ C ⟩ g ≡ f' ⋆⟨ C ⟩ g
   rPrecatWhisker _ _ g p = cong (λ v → v ⋆⟨ C ⟩ g) p
 
   -- working with equal objects
   idP : ∀ {x x'} {p : x ≡ x'} → C [ x , x' ]
-  idP {x = x} {x'} {p} = subst (λ v → C [ x , v ]) p (C .id x)
+  idP {x} {x'} {p} = subst (λ v → C [ x , v ]) p (C .id)
 
   -- heterogeneous seq
   seqP : ∀ {x y y' z} {p : y ≡ y'}
        → (f : C [ x , y ]) (g : C [ y' , z ])
        → C [ x , z ]
-  seqP {x = x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g)
+  seqP {x} {_} {_} {z} {p} f g = f ⋆⟨ C ⟩ (subst (λ a → C [ a , z ]) (sym p) g)
 
   -- also heterogeneous seq, but substituting on the left
   seqP' : ∀ {x y y' z} {p : y ≡ y'}
-       → (f : C [ x , y ]) (g : C [ y' , z ])
-       → C [ x , z ]
-  seqP' {x = x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g
+        → (f : C [ x , y ]) (g : C [ y' , z ])
+        → C [ x , z ]
+  seqP' {x} {_} {_} {z} {p} f g = subst (λ a → C [ x , a ]) p f ⋆⟨ C ⟩ g
 
   -- show that they're equal
   seqP≡seqP' : ∀ {x y y' z} {p : y ≡ y'}
@@ -74,8 +73,8 @@ module _ {C : Precategory ℓ ℓ'} where
 
   -- seqP is equal to normal seq when y ≡ y'
   seqP≡seq : ∀ {x y z}
-             → (f : C [ x , y ]) (g : C [ y , z ])
-             → seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g
+           → (f : C [ x , y ]) (g : C [ y , z ])
+           → seqP {p = refl} f g ≡ f ⋆⟨ C ⟩ g
   seqP≡seq {y = y} {z} f g i = f ⋆⟨ C ⟩ toPathP {A = λ _ → C [ y , z ]} {x = g} refl (~ i)
 
 
diff --git a/Cubical/Categories/Constructions/Elements.agda b/Cubical/Categories/Constructions/Elements.agda
index a8cad42f82..50a6a7655c 100644
--- a/Cubical/Categories/Constructions/Elements.agda
+++ b/Cubical/Categories/Constructions/Elements.agda
@@ -31,7 +31,7 @@ infix 50 ∫_
 (∫ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
 -- morphisms are f : c → c' which take x to x'
 (∫ F) .Hom[_,_] (c , x) (c' , x')  = Σ[ f ∈ C [ c , c' ] ] x' ≡ (F ⟪ f ⟫) x
-(∫ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
+(∫ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
 (∫ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
   = (f ⋆⟨ C ⟩ g) , (x₂
             ≡⟨ q ⟩
@@ -49,16 +49,16 @@ infix 50 ∫_
       cIdL = C .⋆IdL f
 
       -- proof from composition with id
-      p' : x' ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x
-      p' = snd ((∫ F) ._⋆_ ((∫ F) .id o) f')
+      p' : x' ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x
+      p' = snd ((∫ F) ._⋆_ ((∫ F) .id) f')
 (∫ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
     = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS' x' ((F ⟪ a ⟫) x)) p' p cIdR i
       where
         cIdR = C .⋆IdR f
         isS' = getIsSet F c'
 
-        p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x
-        p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id o1))
+        p' : x' ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x
+        p' = snd ((∫ F) ._⋆_ f' ((∫ F) .id))
 (∫ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
   = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS₃ x₃ ((F ⟪ a ⟫) x)) p1 p2 cAssoc i
     where
@@ -78,7 +78,7 @@ infix 50 ∫_
 (∫ᴾ F) .ob = Σ[ c ∈ C .ob ] fst (F ⟅ c ⟆)
 -- morphisms are f : c → c' which take x to x'
 (∫ᴾ F) .Hom[_,_] (c , x) (c' , x')  = Σ[ f ∈ C [ c , c' ] ] x ≡ (F ⟪ f ⟫) x'
-(∫ᴾ F) .id (c , x) = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
+(∫ᴾ F) .id {x = (c , x)} = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
 (∫ᴾ F) ._⋆_ {c , x} {c₁ , x₁} {c₂ , x₂} (f , p) (g , q)
   = (f ⋆⟨ C ⟩ g) , (x
             ≡⟨ p ⟩
@@ -96,16 +96,16 @@ infix 50 ∫_
       cIdL = C .⋆IdL f
 
       -- proof from composition with id
-      p' : x ≡ (F ⟪ C .id c ⋆⟨ C ⟩ f ⟫) x'
-      p' = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) .id o) f')
+      p' : x ≡ (F ⟪ C .id ⋆⟨ C ⟩ f ⟫) x'
+      p' = snd ((∫ᴾ F) ._⋆_ ((∫ᴾ F) .id) f')
 (∫ᴾ F) .⋆IdR o@{c , x} o1@{c' , x'} f'@(f , p) i
     = (cIdR i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x')) p' p cIdR i
       where
         cIdR = C .⋆IdR f
         isS = getIsSet F c
 
-        p' : x ≡ (F ⟪ f ⋆⟨ C ⟩ C .id c' ⟫) x'
-        p' = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) .id o1))
+        p' : x ≡ (F ⟪ f ⋆⟨ C ⟩ C .id ⟫) x'
+        p' = snd ((∫ᴾ F) ._⋆_ f' ((∫ᴾ F) .id))
 (∫ᴾ F) .⋆Assoc o@{c , x} o1@{c₁ , x₁} o2@{c₂ , x₂} o3@{c₃ , x₃} f'@(f , p) g'@(g , q) h'@(h , r) i
   = (cAssoc i) , isOfHLevel→isOfHLevelDep 1 (λ a → isS x ((F ⟪ a ⟫) x₃)) p1 p2 cAssoc i
     where
diff --git a/Cubical/Categories/Constructions/Slice.agda b/Cubical/Categories/Constructions/Slice.agda
index 2fb55752ef..b1d8427563 100644
--- a/Cubical/Categories/Constructions/Slice.agda
+++ b/Cubical/Categories/Constructions/Slice.agda
@@ -1,21 +1,23 @@
 {-# OPTIONS --safe #-}
 
-open import Cubical.Categories.Category
-open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
-open Iso
 open import Cubical.Foundations.HLevels
-open Precategory
-open import Cubical.Core.Glue
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Transport using (transpFill)
 
-module Cubical.Categories.Constructions.Slice {ℓ ℓ' : Level} (C : Precategory ℓ ℓ') (c : C .ob) {{isC : isCategory C}} where
+open import Cubical.Categories.Category
+open import Cubical.Categories.Morphism renaming (isIso to isIsoC)
 
 open import Cubical.Data.Sigma
 
+open Precategory
+open isCategory
+open isUnivalent
+open Iso
+
+module Cubical.Categories.Constructions.Slice {ℓ ℓ' : Level} (C : Precategory ℓ ℓ') (c : C .ob) {{isC : isCategory C}} where
 
 -- just a helper to prevent redundency
 TypeC : Type (ℓ-suc (ℓ-max ℓ ℓ'))
@@ -103,7 +105,7 @@ SliceHom-Σ-Iso .leftInv = λ x → refl
 SliceCat : Precategory _ _
 SliceCat .ob = SliceOb
 SliceCat .Hom[_,_] = SliceHom
-SliceCat .id (sliceob {x} f) = slicehom (C .id x) (C .⋆IdL _)
+SliceCat .id = slicehom (C .id) (C .⋆IdL _)
 SliceCat ._⋆_ {sliceob j} {sliceob k} {sliceob l} (slicehom f p) (slicehom g p') =
   slicehom
     (f ⋆⟨ C ⟩ g)
@@ -191,7 +193,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where
 
         -- the meat of the proof
         sIso : Iso (xf ≡ yg) (CatIso xf yg)
-        sIso .fun p = pathToIso xf yg p -- we use the normal pathToIso via path induction to get an isomorphism
+        sIso .fun p = pathToIso p -- we use the normal pathToIso via path induction to get an isomorphism
         sIso .inv is@(catiso kc lc s r) = SliceOb-≡-intro x≡y (symP (sym (lc .S-comm) ◁ lf≡f))
           where
             -- we get a path between xf and yg by combining paths between
@@ -215,19 +217,19 @@ module _ ⦃ isU : isUnivalent C ⦄ where
 
             -- to show that f ≡ g, we show that l ≡ id
             -- by using C's isomorphism
-            pToI≡id : PathP (λ i → C [ x≡y (~ i) , x ]) (pathToIso {C = C} x y x≡y .inv) (C .id x)
-            pToI≡id = J (λ y p → PathP (λ i → C [ p (~ i) , x ]) (pathToIso {C = C} x y p .inv) (C .id x))
+            pToI≡id : PathP (λ i → C [ x≡y (~ i) , x ]) (pathToIso {C = C} x≡y .inv) (C .id)
+            pToI≡id = J (λ y p → PathP (λ i → C [ p (~ i) , x ]) (pathToIso {C = C} p .inv) (C .id))
                         (λ j → JRefl pToIFam pToIBase j .inv)
                         x≡y
               where
-                idx = C .id x
+                idx = C .id
                 pToIFam = (λ z _ → CatIso {C = C} x z)
-                pToIBase = catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)
+                pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)
 
-            l≡pToI : l ≡ pathToIso {C = C} x y x≡y .inv
+            l≡pToI : l ≡ pathToIso {C = C} x≡y .inv
             l≡pToI i = pToIIso .rightInv extractIso (~ i) .inv
 
-            l≡id : PathP (λ i → C [ x≡y (~ i) , x ]) l (C .id x)
+            l≡id : PathP (λ i → C [ x≡y (~ i) , x ]) l (C .id)
             l≡id = l≡pToI ◁ pToI≡id
 
             lf≡f : PathP (λ i → C [ x≡y (~ i) , c ]) (l ⋆⟨ C ⟩ f) f
@@ -273,13 +275,13 @@ module _ ⦃ isU : isUnivalent C ⦄ where
             -- sec
 
             s' = (sIso .fun) (sIso .inv is) .sec
-            s'≡s : PathP (λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i ≡ SliceCat .id _) s' s
+            s'≡s : PathP (λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i ≡ SliceCat .id) s' s
             s'≡s = isSetHomP1 _ _ λ i → lc'≡lc i ⋆⟨ SliceCat ⟩ kc'≡kc i
 
             -- ret
 
             r' = (sIso .fun) (sIso .inv is) .ret
-            r'≡r : PathP (λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i ≡ SliceCat .id _) r' r
+            r'≡r : PathP (λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i ≡ SliceCat .id) r' r
             r'≡r = isSetHomP1 _ _ λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i
 
         sIso .leftInv p = p'≡p
@@ -306,17 +308,17 @@ module _ ⦃ isU : isUnivalent C ⦄ where
 
             -- we first show that it's equivalent to use sIso first then extract, or to extract first than use pToIIso
             extractCom : extractIso' (sIso .fun p) ≡ pToIIso .fun pOb
-            extractCom = J (λ yg' p̃ → extractIso' (pathToIso xf yg' p̃) ≡ pToIIso' {xf = xf} {yg'} .fun (λ i → (p̃ i) .S-ob))
+            extractCom = J (λ yg' p̃ → extractIso' (pathToIso p̃) ≡ pToIIso' {xf = xf} {yg'} .fun (λ i → (p̃ i) .S-ob))
                            (cong extractIso' (JRefl pToIFam' pToIBase') ∙ sym (JRefl pToIFam pToIBase))
                            p
                where
-                 idx = C .id x
+                 idx = C .id
                  pToIFam = (λ z _ → CatIso {C = C} x z)
-                 pToIBase = catiso (C .id x) idx (C .⋆IdL idx) (C .⋆IdL idx)
+                 pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx)
 
-                 idxf = SliceCat .id xf
+                 idxf = SliceCat .id
                  pToIFam' = (λ z _ → CatIso {C = SliceCat} xf z)
-                 pToIBase' = catiso (SliceCat .id xf) idxf (SliceCat .⋆IdL idxf) (SliceCat .⋆IdL idxf)
+                 pToIBase' = catiso (SliceCat .id) idxf (SliceCat .⋆IdL idxf) (SliceCat .⋆IdL idxf)
 
             -- why does this not follow definitionally?
             -- from extractCom, we get that performing the roundtrip on pOb gives us back p'Ob
diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda
index 59eb7a227e..11051b3b01 100644
--- a/Cubical/Categories/Functor/Base.agda
+++ b/Cubical/Categories/Functor/Base.agda
@@ -1,28 +1,32 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Functor.Base where
 
 open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Sigma
+
 open import Cubical.Categories.Category
 
 private
   variable
     ℓC ℓC' ℓD ℓD' : Level
 
-record Functor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
+record Functor (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') :
+         Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) where
   no-eta-equality
+
   open Precategory
 
   field
-    F-ob : C .ob → D .ob
-    F-hom : {x y : C .ob} → C [ x , y ] → D [(F-ob x) , (F-ob y)]
-    F-id : {x : C .ob} → F-hom (C .id x) ≡ D .id (F-ob x)
-    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ]) → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)
+    F-ob  : C .ob → D .ob
+    F-hom : {x y : C .ob} → C [ x , y ] → D [ F-ob x , F-ob y ]
+    F-id  : {x : C .ob} → F-hom (C .id) ≡ D .id {x = F-ob x}
+    F-seq : {x y z : C .ob} (f : C [ x , y ]) (g : C [ y , z ])
+          → F-hom (f ⋆⟨ C ⟩ g) ≡ (F-hom f) ⋆⟨ D ⟩ (F-hom g)
 
-  isFull = (x y : _) (F[f] : D [(F-ob x) , (F-ob y)]) → ∃ (C [ x , y ]) (λ f → F-hom f ≡ F[f])
+  isFull = (x y : _) (F[f] : D [ F-ob x , F-ob y ]) → ∃[ f ∈ C [ x , y ] ] F-hom f ≡ F[f]
   isFaithful = (x y : _) (f g : C [ x , y ]) → F-hom f ≡ F-hom g → f ≡ g
-  isEssentiallySurj = ∀ (d : D .ob) → Σ[ c ∈ C .ob ] CatIso {C = D} (F-ob c) d
+  isEssentiallySurj = (d : D .ob) → Σ[ c ∈ C .ob ] CatIso {C = D} (F-ob c) d
 
 private
   variable
@@ -60,30 +64,16 @@ _⟪_⟫ = F-hom
 
 -- functor composition
 funcComp : ∀ (G : Functor D E) (F : Functor C D) → Functor C E
-(funcComp G F) .F-ob c = G ⟅ F ⟅ c ⟆ ⟆
-(funcComp G F) .F-hom f = G ⟪ F ⟪ f ⟫ ⟫
-(funcComp {D = D} {E = E} {C = C} G F) .F-id {c}
-  = (G ⟪ F ⟪ C .id c ⟫ ⟫)
-  ≡⟨ cong (G ⟪_⟫) (F .F-id) ⟩
-    G .F-id
-  --   (G ⟪ D .id (F ⟅ c ⟆) ⟫) -- deleted this cause the extra refl composition was annoying
-  -- ≡⟨ G .F-id ⟩
-  --   E .id (G ⟅ F ⟅ c ⟆ ⟆)
-  -- ∎
-(funcComp {D = D} {E = E} {C = C} G F) .F-seq {x} {y} {z} f g
-  = (G ⟪ F ⟪ f ⋆⟨ C ⟩ g ⟫ ⟫)
-  ≡⟨ cong (G ⟪_⟫) (F .F-seq _ _) ⟩
-    G .F-seq _ _
-  --   (G ⟪ (F ⟪ f ⟫) ⋆⟨ D ⟩ (F ⟪ g ⟫) ⟫) -- deleted for same reason as above
-  -- ≡⟨ G .F-seq _ _ ⟩
-  --   (G ⟪ F ⟪ f ⟫ ⟫) ⋆⟨ E ⟩ (G ⟪ F ⟪ g ⟫ ⟫)
-  -- ∎
+(funcComp G F) .F-ob c    = G ⟅ F ⟅ c ⟆ ⟆
+(funcComp G F) .F-hom f   = G ⟪ F ⟪ f ⟫ ⟫
+(funcComp G F) .F-id      = cong (G ⟪_⟫) (F .F-id) ∙ G .F-id
+(funcComp G F) .F-seq f g = cong (G ⟪_⟫) (F .F-seq _ _) ∙ G .F-seq _ _
 
 infixr 30 funcComp
 syntax funcComp G F = G ∘F F
 
 _^opF : Functor C D → Functor (C ^op) (D ^op)
-(F ^opF) .F-ob = F .F-ob
-(F ^opF) .F-hom = F .F-hom
-(F ^opF) .F-id = F .F-id
+(F ^opF) .F-ob      = F .F-ob
+(F ^opF) .F-hom     = F .F-hom
+(F ^opF) .F-id      = F .F-id
 (F ^opF) .F-seq f g = F .F-seq g f
diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda
index 5073339a3b..e9906f4ca3 100644
--- a/Cubical/Categories/Functor/Properties.agda
+++ b/Cubical/Categories/Functor/Properties.agda
@@ -90,18 +90,18 @@ module _ {F : Functor C D} where
       ≡⟨ sym (F .F-seq f⁻¹ f) ⟩
         F ⟪ f⁻¹ ⋆⟨ C ⟩ f ⟫
       ≡⟨ cong (F .F-hom) sec' ⟩
-        F ⟪ C .id y ⟫
+        F ⟪ C .id ⟫
       ≡⟨ F .F-id ⟩
-        D .id y'
+        D .id
       ∎ )
       -- ret
       ( (g ⋆⟨ D ⟩ g⁻¹)
         ≡⟨ sym (F .F-seq f f⁻¹) ⟩
       F ⟪ f ⋆⟨ C ⟩ f⁻¹ ⟫
         ≡⟨ cong (F .F-hom) ret' ⟩
-      F ⟪ C .id x ⟫
+      F ⟪ C .id ⟫
       ≡⟨ F .F-id ⟩
-        D .id x'
+        D .id
       ∎ )
 
       where
diff --git a/Cubical/Categories/Instances/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda
index 55c8f5ba40..d8cf7bcb32 100644
--- a/Cubical/Categories/Instances/CommRings.agda
+++ b/Cubical/Categories/Instances/CommRings.agda
@@ -14,7 +14,7 @@ open CommRingHoms
 CommRingsPrecategory : ∀ {ℓ} → Precategory (ℓ-suc ℓ) ℓ
 ob CommRingsPrecategory                     = CommRing _
 Hom[_,_] CommRingsPrecategory               = CommRingHom
-id CommRingsPrecategory                     = idCommRingHom
+id CommRingsPrecategory {R}                 = idCommRingHom R
 _⋆_ CommRingsPrecategory {R} {S} {T}        = compCommRingHom R S T
 ⋆IdL CommRingsPrecategory {R} {S}           = compIdCommRingHom {R = R} {S}
 ⋆IdR CommRingsPrecategory {R} {S}           = idCompCommRingHom {R = R} {S}
diff --git a/Cubical/Categories/Instances/Cospan.agda b/Cubical/Categories/Instances/Cospan.agda
index 999bb3589a..38926b439b 100644
--- a/Cubical/Categories/Instances/Cospan.agda
+++ b/Cubical/Categories/Instances/Cospan.agda
@@ -1,5 +1,4 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Instances.Cospan where
 
 open import Cubical.Foundations.Prelude
@@ -33,9 +32,9 @@ CospanCat ._⋆_ {x = ②} {①} {①} f g = tt
 CospanCat ._⋆_ {x = ⓪} {⓪} {①} f g = tt
 CospanCat ._⋆_ {x = ②} {②} {①} f g = tt
 
-CospanCat .id ⓪ = tt
-CospanCat .id ① = tt
-CospanCat .id ② = tt
+CospanCat .id {⓪} = tt
+CospanCat .id {①} = tt
+CospanCat .id {②} = tt
 
 CospanCat .⋆IdL {⓪} {①} _ = refl
 CospanCat .⋆IdL {②} {①} _ = refl
diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda
index 9d03f44368..a984f9b219 100644
--- a/Cubical/Categories/Instances/Functors.agda
+++ b/Cubical/Categories/Instances/Functors.agda
@@ -15,13 +15,14 @@ private
 
 module _ (C : Precategory ℓC ℓC') (D : Precategory ℓD ℓD') ⦃ isCatD : isCategory D ⦄ where
   open Precategory
+  open isCategory
   open NatTrans
   open Functor
 
   FUNCTOR : Precategory (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) (ℓ-max (ℓ-max ℓC ℓC') ℓD')
   FUNCTOR .ob = Functor C D
   FUNCTOR .Hom[_,_] = NatTrans
-  FUNCTOR .id = idTrans
+  FUNCTOR .id {F} = idTrans F
   FUNCTOR ._⋆_ = seqTrans
   FUNCTOR .⋆IdL α = makeNatTransPath λ i x → D .⋆IdL (α .N-ob x) i
   FUNCTOR .⋆IdR α = makeNatTransPath λ i x → D .⋆IdR (α .N-ob x) i
diff --git a/Cubical/Categories/Instances/Rings.agda b/Cubical/Categories/Instances/Rings.agda
index e328fc085c..c161458bb3 100644
--- a/Cubical/Categories/Instances/Rings.agda
+++ b/Cubical/Categories/Instances/Rings.agda
@@ -14,7 +14,7 @@ open RingHoms
 RingsPrecategory : ∀ {ℓ} → Precategory (ℓ-suc ℓ) ℓ
 ob RingsPrecategory       = Ring _
 Hom[_,_] RingsPrecategory = RingHom
-id RingsPrecategory       = idRingHom
+id RingsPrecategory {R}   = idRingHom R
 _⋆_ RingsPrecategory      = compRingHom
 ⋆IdL RingsPrecategory     = compIdRingHom
 ⋆IdR RingsPrecategory     = idCompRingHom
diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda
index 5347b53114..859595b909 100644
--- a/Cubical/Categories/Instances/Sets.agda
+++ b/Cubical/Categories/Instances/Sets.agda
@@ -10,16 +10,17 @@ open import Cubical.Categories.Functor
 open import Cubical.Categories.NaturalTransformation
 
 open Precategory
+open isCategory
 
 module _ ℓ where
   SET : Precategory (ℓ-suc ℓ) ℓ
-  SET .ob = Σ (Type ℓ) isSet
+  SET .ob                       = Σ (Type ℓ) isSet
   SET .Hom[_,_] (A , _) (B , _) = A → B
-  SET .id _  = λ x → x
-  SET ._⋆_ f g = λ x → g (f x)
-  SET .⋆IdL f = refl
-  SET .⋆IdR f = refl
-  SET .⋆Assoc f g h = refl
+  SET .id                       = λ x → x
+  SET ._⋆_ f g                  = λ x → g (f x)
+  SET .⋆IdL f                   = refl
+  SET .⋆IdR f                   = refl
+  SET .⋆Assoc f g h             = refl
 
 module _ {ℓ} where
   isSetExpIdeal : {A B : Type ℓ} → isSet B → isSet (A → B)
@@ -97,10 +98,10 @@ Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv
 -- kind of useless
 module _ ℓ where
   TYPE : Precategory (ℓ-suc ℓ) ℓ
-  TYPE .ob = Type ℓ
+  TYPE .ob           = Type ℓ
   TYPE .Hom[_,_] A B = A → B
-  TYPE .id A  = λ x → x
-  TYPE ._⋆_ f g = λ x → g (f x)
-  TYPE .⋆IdL f = refl
-  TYPE .⋆IdR f = refl
+  TYPE .id           = λ x → x
+  TYPE ._⋆_ f g      = λ x → g (f x)
+  TYPE .⋆IdL f       = refl
+  TYPE .⋆IdR f       = refl
   TYPE .⋆Assoc f g h = refl
diff --git a/Cubical/Categories/Limits.agda b/Cubical/Categories/Limits.agda
index 6d2b58f3e9..8efbf8cb3f 100644
--- a/Cubical/Categories/Limits.agda
+++ b/Cubical/Categories/Limits.agda
@@ -1,5 +1,4 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Limits where
 
 open import Cubical.Categories.Limits.Base public
diff --git a/Cubical/Categories/Limits/Base.agda b/Cubical/Categories/Limits/Base.agda
index 6eb20af4c3..5dde339dd4 100644
--- a/Cubical/Categories/Limits/Base.agda
+++ b/Cubical/Categories/Limits/Base.agda
@@ -26,7 +26,7 @@ module _ {J : Precategory ℓJ ℓJ'}
   -- morphisms to the identity
   constF : (c : C .ob) → Functor J C
   constF c .F-ob _ = c
-  constF c .F-hom _ = C .id c
+  constF c .F-hom _ = C .id
   constF c .F-id = refl
   constF c .F-seq _ _ = sym (C .⋆IdL _)
 
@@ -45,11 +45,11 @@ module _ {J : Precategory ℓJ ℓJ'}
         → Cone K d
     (f ◼ μ) .N-ob x = f ⋆⟨ C ⟩ μ ⟦ x ⟧
     (f ◼ μ) .N-hom {x = x} {y} k
-      = C .id _ ⋆⟨ C ⟩ (f ⋆⟨ C ⟩ μ ⟦ y ⟧)
+      = C .id ⋆⟨ C ⟩ (f ⋆⟨ C ⟩ μ ⟦ y ⟧)
       ≡⟨ C .⋆IdL _ ⟩
         f ⋆⟨ C ⟩ μ ⟦ y ⟧
       ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (sym (C .⋆IdL _)) ⟩
-        f ⋆⟨ C ⟩ (C .id _ ⋆⟨ C ⟩ μ ⟦ y ⟧)
+        f ⋆⟨ C ⟩ (C .id ⋆⟨ C ⟩ μ ⟦ y ⟧)
       ≡⟨ cong (λ v → f ⋆⟨ C ⟩ v) (μ .N-hom k) ⟩
         f ⋆⟨ C ⟩ (μ ⟦ x ⟧ ⋆⟨ C ⟩ K ⟪ k ⟫)
       ≡⟨ sym (C .⋆Assoc _ _ _) ⟩
diff --git a/Cubical/Categories/Limits/Pullback.agda b/Cubical/Categories/Limits/Pullback.agda
index 38e0561fe4..4fbfffece7 100644
--- a/Cubical/Categories/Limits/Pullback.agda
+++ b/Cubical/Categories/Limits/Pullback.agda
@@ -62,9 +62,9 @@ module _ {C : Precategory ℓ ℓ'} where
   Cospan→Func (cospan l m r f g) .F-ob ② = r
   Cospan→Func (cospan l m r f g) .F-hom {⓪} {①} k = f
   Cospan→Func (cospan l m r f g) .F-hom {②} {①} k = g
-  Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id l
-  Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id m
-  Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id r
+  Cospan→Func (cospan l m r f g) .F-hom {⓪} {⓪} k = id
+  Cospan→Func (cospan l m r f g) .F-hom {①} {①} k = id
+  Cospan→Func (cospan l m r f g) .F-hom {②} {②} k = id
   Cospan→Func (cospan l m r f g) .F-id {⓪} = refl
   Cospan→Func (cospan l m r f g) .F-id {①} = refl
   Cospan→Func (cospan l m r f g) .F-id {②} = refl
diff --git a/Cubical/Categories/Limits/Terminal.agda b/Cubical/Categories/Limits/Terminal.agda
index f52b6a7186..6cf045e064 100644
--- a/Cubical/Categories/Limits/Terminal.agda
+++ b/Cubical/Categories/Limits/Terminal.agda
@@ -40,9 +40,9 @@ module _ (C : Precategory ℓ ℓ') where
         x→y = fst (hx y) -- morphism forwards
         y→x : C [ y , x ]
         y→x = fst (hy x) -- morphism backwards
-        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id x
+        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id
         x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
-        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id y
+        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id
         y→x→y = isContr→isProp (hy y) _ _ -- similar.
     in catiso x→y y→x y→x→y x→y→x
 
@@ -71,9 +71,9 @@ module _ (C : Precategory ℓ ℓ') where
         x→y = fst (hy x) -- morphism forwards
         y→x : C [ y , x ]
         y→x = fst (hx y) -- morphism backwards
-        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id x
+        x→y→x : x→y ⋆⟨ C ⟩ y→x ≡ id
         x→y→x = isContr→isProp (hx x) _ _ -- compose to id by uniqueness
-        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id y
+        y→x→y : y→x ⋆⟨ C ⟩ x→y ≡ id
         y→x→y = isContr→isProp (hy y) _ _ -- similar.
     in catiso x→y y→x y→x→y x→y→x
 
diff --git a/Cubical/Categories/Morphism.agda b/Cubical/Categories/Morphism.agda
index c075003e39..27e81b28f3 100644
--- a/Cubical/Categories/Morphism.agda
+++ b/Cubical/Categories/Morphism.agda
@@ -1,9 +1,10 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Morphism where
 
 open import Cubical.Foundations.Prelude
+
 open import Cubical.Data.Sigma
+
 open import Cubical.Categories.Category
 
 private
@@ -12,37 +13,37 @@ private
 
 module _ {C : Precategory ℓ ℓ'} where
   open Precategory C
+
   private
     variable
       x y z w : ob
 
-  isMonic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')
-  isMonic {x} {y} f = ∀ {z : ob} {a a' : Hom[ z , x ]}
-    → (f ∘ a ≡ f ∘ a') → (a ≡ a')
+  isMonic : Hom[ x , y ] → Type (ℓ-max ℓ ℓ')
+  isMonic {x} {y} f =
+    ∀ {z} {a a' : Hom[ z , x ]} → f ∘ a ≡ f ∘ a' → a ≡ a'
 
   isEpic : (Hom[ x , y ]) → Type (ℓ-max ℓ ℓ')
-  isEpic {x} {y} g = ∀ {z : ob} {b b' : Hom[ y , z ]}
-    → (b ∘ g ≡ b' ∘ g) → (b ≡ b')
+  isEpic {x} {y} g =
+    ∀ {z} {b b' : Hom[ y , z ]} → b ∘ g ≡ b' ∘ g → b ≡ b'
 
   -- A morphism is split monic if it has a *retraction*
   isSplitMon : (Hom[ x , y ]) → Type ℓ'
-  isSplitMon {x} {y} f = ∃[ r ∈ Hom[ y , x ] ] r ∘ f ≡ id x
+  isSplitMon {x} {y} f = ∃[ r ∈ Hom[ y , x ] ] r ∘ f ≡ id
 
   -- A morphism is split epic if it has a *section*
   isSplitEpi : (Hom[ x , y ]) → Type ℓ'
-  isSplitEpi {x} {y} g = ∃[ s ∈ Hom[ y , x ] ] g ∘ s ≡ id y
+  isSplitEpi {x} {y} g = ∃[ s ∈ Hom[ y , x ] ] g ∘ s ≡ id
 
   record areInv (f : Hom[ x , y ]) (g : Hom[ y , x ]) : Type ℓ' where
     field
-      sec : g ⋆ f ≡ id y
-      ret : f ⋆ g ≡ id x
+      sec : g ⋆ f ≡ id
+      ret : f ⋆ g ≡ id
 
   open areInv
 
-  symAreInv : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]}
-            → areInv f g
-            → areInv g f
-  symAreInv record { sec = sec ; ret = ret } = record { sec = ret ; ret = sec }
+  symAreInv : {f : Hom[ x , y ]} {g : Hom[ y , x ]} → areInv f g → areInv g f
+  sec (symAreInv x) = ret x
+  ret (symAreInv x) = sec x
 
   -- equational reasoning with inverses
   invMoveR : ∀ {f : Hom[ x , y ]} {g : Hom[ y , x ]} {h : Hom[ z , x ]} {k : Hom[ z , y ]}
@@ -52,7 +53,7 @@ module _ {C : Precategory ℓ ℓ'} where
   invMoveR {f = f} {g} {h} {k} ai p
     = h
     ≡⟨ sym (⋆IdR _) ⟩
-      (h ⋆ id _)
+      (h ⋆ id)
     ≡⟨ cong (h ⋆_) (sym (ai .ret)) ⟩
       (h ⋆ (f ⋆ g))
     ≡⟨ sym (⋆Assoc _ _ _) ⟩
@@ -68,7 +69,7 @@ module _ {C : Precategory ℓ ℓ'} where
   invMoveL {f = f} {g} {h} {k} ai p
     = h
     ≡⟨ sym (⋆IdL _) ⟩
-      id _ ⋆ h
+      id ⋆ h
     ≡⟨ cong (_⋆ h) (sym (ai .sec)) ⟩
       (g ⋆ f) ⋆ h
     ≡⟨ ⋆Assoc _ _ _ ⟩
@@ -80,15 +81,16 @@ module _ {C : Precategory ℓ ℓ'} where
   record isIso (f : Hom[ x , y ]) : Type ℓ' where
     field
       inv : Hom[ y , x ]
-      sec : inv ⋆ f ≡ id y
-      ret : f ⋆ inv ≡ id x
+      sec : inv ⋆ f ≡ id
+      ret : f ⋆ inv ≡ id
 
   open isIso
 
   isIso→areInv : ∀ {f : Hom[ x , y ]}
                → (isI : isIso f)
                → areInv f (isI .inv)
-  isIso→areInv record { inv = inv ; sec = sec ; ret = ret } = record { sec = sec ; ret = ret }
+  sec (isIso→areInv isI) = sec isI
+  ret (isIso→areInv isI) = ret isI
 
   open CatIso
 
@@ -96,11 +98,16 @@ module _ {C : Precategory ℓ ℓ'} where
   isIso→CatIso : ∀ {f : C [ x , y ]}
                → isIso f
                → CatIso {C = C} x y
-  isIso→CatIso {f = f} record { inv = f⁻¹ ; sec = sec ; ret = ret } = catiso f f⁻¹ sec ret
+  mor (isIso→CatIso {f = f} x) = f
+  inv (isIso→CatIso x) = inv x
+  sec (isIso→CatIso x) = sec x
+  ret (isIso→CatIso x) = ret x
 
   CatIso→isIso : (cIso : CatIso {C = C} x y)
                → isIso (cIso .mor)
-  CatIso→isIso (catiso mor inv sec ret) = record { inv = inv ; sec = sec ; ret = ret }
+  inv (CatIso→isIso f) = inv f
+  sec (CatIso→isIso f) = sec f
+  ret (CatIso→isIso f) = ret f
 
   CatIso→areInv : (cIso : CatIso {C = C} x y)
                 → areInv (cIso .mor) (cIso .inv)
diff --git a/Cubical/Categories/NaturalTransformation/Base.agda b/Cubical/Categories/NaturalTransformation/Base.agda
index 93f538a635..59e8606ef1 100644
--- a/Cubical/Categories/NaturalTransformation/Base.agda
+++ b/Cubical/Categories/NaturalTransformation/Base.agda
@@ -1,5 +1,4 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.NaturalTransformation.Base where
 
 open import Cubical.Foundations.Prelude
@@ -79,17 +78,17 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
 
   -- component of a natural transformation
   infix 30 _⟦_⟧
-  _⟦_⟧ : ∀ {F G : Functor C D} → (F ⇒ G) → (x : C .ob) → D [(F .F-ob x) , (G .F-ob x)]
+  _⟦_⟧ : ∀ {F G : Functor C D} → F ⇒ G → (x : C .ob) → D [ F .F-ob x , G .F-ob x ]
   _⟦_⟧ = N-ob
 
   idTrans : (F : Functor C D) → NatTrans F F
-  idTrans F .N-ob x = D .id (F .F-ob x)
+  idTrans F .N-ob x  = D .id
   idTrans F .N-hom f =
       (F .F-hom f) ⋆ᴰ (idTrans F .N-ob _)
     ≡⟨ D .⋆IdR _ ⟩
       F .F-hom f
     ≡⟨ sym (D .⋆IdL _) ⟩
-      (D .id (F .F-ob _)) ⋆ᴰ (F .F-hom f)
+      (D .id) ⋆ᴰ (F .F-hom f)
     ∎
 
   syntax idTrans F = 1[ F ]
@@ -175,6 +174,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
 
   module _  ⦃ isCatD : isCategory D ⦄ {F G : Functor C D} {α β : NatTrans F G} where
     open Precategory
+    open isCategory
     open Functor
     open NatTrans
 
@@ -189,6 +189,7 @@ module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
             {α : NatTrans F G}
             {β : NatTrans F' G'} where
     open Precategory
+    open isCategory
     open Functor
     open NatTrans
     makeNatTransPathP : ∀ (p : F ≡ F') (q : G ≡ G')
diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda
index 2ba0eacc4f..85216496cd 100644
--- a/Cubical/Categories/NaturalTransformation/Properties.agda
+++ b/Cubical/Categories/NaturalTransformation/Properties.agda
@@ -21,6 +21,7 @@ open isIsoC
 open NatIso
 open NatTrans
 open Precategory
+open isCategory
 open Functor
 
 module _ {C : Precategory ℓC ℓC'} {D : Precategory ℓD ℓD'} where
diff --git a/Cubical/Categories/Presheaf/Base.agda b/Cubical/Categories/Presheaf/Base.agda
index 074874757d..5908c588d5 100644
--- a/Cubical/Categories/Presheaf/Base.agda
+++ b/Cubical/Categories/Presheaf/Base.agda
@@ -15,70 +15,11 @@ open import Cubical.Categories.Instances.Functors
 
 module _ {ℓ ℓ'} where
 
-  PreShv : Precategory ℓ ℓ' → (ℓS : Level) → Precategory (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS)) (ℓ-max (ℓ-max ℓ ℓ') ℓS)
+  PreShv : Precategory ℓ ℓ' → (ℓS : Level)
+         → Precategory (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS)) (ℓ-max (ℓ-max ℓ ℓ') ℓS)
   PreShv C ℓS = FUNCTOR (C ^op) (SET ℓS)
 
 instance
   isCatPreShv : ∀ {ℓ ℓ'} {C : Precategory ℓ ℓ'} {ℓS}
     → isCategory (PreShv C ℓS)
   isCatPreShv {C = C} {ℓS} = isCatFUNCTOR (C ^op) (SET ℓS)
-
-private
-  variable
-    ℓ ℓ' : Level
-
-module Yoneda (C : Precategory ℓ ℓ') ⦃ C-cat : isCategory C ⦄ where
-  open Functor
-  open NatTrans
-  open Precategory C
-
-  yo : ob → Functor (C ^op) (SET ℓ')
-  yo x .F-ob y .fst = C [ y , x ]
-  yo x .F-ob y .snd = C-cat .isSetHom
-  yo x .F-hom f g = f ⋆⟨ C ⟩ g
-  yo x .F-id i f = ⋆IdL f i
-  yo x .F-seq f g i h = ⋆Assoc g f h i
-
-  YO : Functor C (PreShv C ℓ')
-  YO .F-ob = yo
-  YO .F-hom f .N-ob z g = g ⋆⟨ C ⟩ f
-  YO .F-hom f .N-hom g i h = ⋆Assoc g h f i
-  YO .F-id = makeNatTransPath λ i _ → λ f → ⋆IdR f i
-  YO .F-seq f g = makeNatTransPath λ i _ → λ h → ⋆Assoc h f g (~ i)
-
-
-  module _ {x} (F : Functor (C ^op) (SET ℓ')) where
-    yo-yo-yo : NatTrans (yo x) F → F .F-ob x .fst
-    yo-yo-yo α = α .N-ob _ (id _)
-
-    no-no-no : F .F-ob x .fst → NatTrans (yo x) F
-    no-no-no a .N-ob y f = F .F-hom f a
-    no-no-no a .N-hom f = funExt λ g i → F .F-seq g f i a
-
-    yoIso : Iso (NatTrans (yo x) F) (F .F-ob x .fst)
-    yoIso .Iso.fun = yo-yo-yo
-    yoIso .Iso.inv = no-no-no
-    yoIso .Iso.rightInv b i = F .F-id i b
-    yoIso .Iso.leftInv a = makeNatTransPath (funExt λ _ → funExt rem)
-      where
-        rem : ∀ {z} (x₁ : C [ z , x ]) → F .F-hom x₁ (yo-yo-yo a) ≡ (a .N-ob z) x₁
-        rem g =
-          F .F-hom g (yo-yo-yo a)
-            ≡[ i ]⟨ a .N-hom g (~ i) (id x) ⟩
-          a .N-hom g i0 (id x)
-            ≡[ i ]⟨ a .N-ob _ (⋆IdR g i) ⟩
-          (a .N-ob _) g
-            ∎
-
-    yoEquiv : NatTrans (yo x) F ≃ F .F-ob x .fst
-    yoEquiv = isoToEquiv yoIso
-
-
-  isFullYO : isFull YO
-  isFullYO x y F[f] = ∣ yo-yo-yo _ F[f] , yoIso {x} (yo y) .Iso.leftInv F[f] ∣
-
-  isFaithfulYO : isFaithful YO
-  isFaithfulYO x y f g p i =
-    hcomp
-      (λ j → λ{ (i = i0) → ⋆IdL f j; (i = i1) → ⋆IdL g j})
-      (yo-yo-yo _ (p i))
diff --git a/Cubical/Categories/Presheaf/KanExtension.agda b/Cubical/Categories/Presheaf/KanExtension.agda
index da9be180a4..841ceb4285 100644
--- a/Cubical/Categories/Presheaf/KanExtension.agda
+++ b/Cubical/Categories/Presheaf/KanExtension.agda
@@ -76,7 +76,7 @@ module Lan {ℓC ℓC' ℓD ℓD'} ℓS
     mapR h (squash/ t u p q i j) =
       squash/ (mapR h t) (mapR h u) (cong (mapR h) p) (cong (mapR h) q) i j
 
-    mapRId : (d : D.ob) → mapR (D.id d) ≡ (idfun _)
+    mapRId : (d : D.ob) → mapR (D.id {x = d}) ≡ idfun (Quo d)
     mapRId d =
       funExt (elimProp (λ _ → squash/ _ _) (λ (c , g , a) i → [ c , D.⋆IdL g i , a ]))
 
@@ -143,17 +143,17 @@ module Lan {ℓC ℓC' ℓD ℓD'} ℓS
   open UnitCounit
 
   η : 𝟙⟨ FUNCTOR (C ^op) (SET ℓ) ⟩ ⇒ funcComp F* Lan
-  η .N-ob G .N-ob c a = [ c , D.id _ , a ]
+  η .N-ob G .N-ob c a = [ c , D.id , a ]
   η .N-ob G .N-hom {c'} {c} f =
     funExt λ a →
-    [ c , D.id _ , (G ⟪ f ⟫) a ]
-      ≡⟨ sym (shift/ (D.id _) f a) ⟩
-    [ c' , ((D.id _) D.⋆ F ⟪ f ⟫) , a ]
+    [ c , D.id , (G ⟪ f ⟫) a ]
+      ≡⟨ sym (shift/ D.id f a) ⟩
+    [ c' , (D.id D.⋆ F ⟪ f ⟫) , a ]
       ≡[ i ]⟨ [ c' , lem i , a ] ⟩
-    [ c' , (F ⟪ f ⟫ D.⋆ (D.id _)) , a ]
+    [ c' , (F ⟪ f ⟫ D.⋆ D.id) , a ]
     ∎
     where
-    lem : (D.id _) D.⋆ F ⟪ f ⟫ ≡ F ⟪ f ⟫ D.⋆ (D.id _)
+    lem : D.id D.⋆ F ⟪ f ⟫ ≡ F ⟪ f ⟫ D.⋆ D.id
     lem = D.⋆IdL (F ⟪ f ⟫) ∙ sym (D.⋆IdR (F ⟪ f ⟫))
   η .N-hom f = makeNatTransPath refl
 
@@ -177,11 +177,11 @@ module Lan {ℓC ℓC' ℓD ℓD'} ℓS
       (funExt₂ λ d →
         elimProp (λ _ → squash/ _ _)
           (λ (c , g , a) →
-            [ c , g D.⋆ D.id _ , a ]
+            [ c , g D.⋆ D.id , a ]
               ≡[ i ]⟨ [ c , (g D.⋆ F .F-id (~ i)) , a ] ⟩
-            [ c , g D.⋆ (F ⟪ C.id _ ⟫) , a ]
-              ≡⟨ shift/ g (C.id _) a ⟩
-            [ c , g , (G ⟪ C.id _ ⟫) a ]
+            [ c , g D.⋆ (F ⟪ C.id ⟫) , a ]
+              ≡⟨ shift/ g C.id a ⟩
+            [ c , g , (G ⟪ C.id ⟫) a ]
               ≡[ i ]⟨ [ c , g , G .F-id i a ] ⟩
             [ c , g , a ]
             ∎))
@@ -243,7 +243,7 @@ module Ran {ℓC ℓC' ℓD ℓD'} ℓS
     mapR h x .fun c g = x .fun c (g ⋆⟨ D ⟩ h)
     mapR h x .coh f g = cong (x .fun _) (D.⋆Assoc (F ⟪ f ⟫) g h) ∙ x .coh f (g ⋆⟨ D ⟩ h)
 
-    mapRId : (d : D.ob) → mapR (D.id d) ≡ (idfun _)
+    mapRId : (d : D.ob) → mapR (D.id {x = d}) ≡ idfun (End d)
     mapRId h = funExt λ x → end≡ λ c g → cong (x .fun c) (D.⋆IdR g)
 
     mapR∘ : {d d' d'' : D.ob}
@@ -325,10 +325,10 @@ module Ran {ℓC ℓC' ℓD ℓD'} ℓS
     makeNatTransPath (funExt₂ λ d a → end≡ _ λ c g → sym (funExt⁻ (α .N-hom g) a))
 
   ε : funcComp F* Ran ⇒ 𝟙⟨ FUNCTOR (C ^op) (SET ℓ) ⟩
-  ε .N-ob H .N-ob c x = x .fun c (D.id _)
+  ε .N-ob H .N-ob c x = x .fun c D.id
   ε .N-ob H .N-hom {c} {c'} g =
     funExt λ x →
-    cong (x .fun c') (D.⋆IdL _ ∙ sym (D.⋆IdR _)) ∙ x .coh g (D.id _)
+    cong (x .fun c') (D.⋆IdL _ ∙ sym (D.⋆IdR _)) ∙ x .coh g D.id
   ε .N-hom {H} {H'} α = makeNatTransPath refl
 
   Δ₁ : ∀ G → seqTrans (F* ⟪ η ⟦ G ⟧ ⟫) (ε ⟦ F* ⟅ G ⟆ ⟧) ≡ idTrans _
diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda
index 077979dd31..58b2488556 100644
--- a/Cubical/Categories/Presheaf/Properties.agda
+++ b/Cubical/Categories/Presheaf/Properties.agda
@@ -138,28 +138,28 @@ module _ {ℓS : Level} (C : Precategory ℓ ℓ') (F : Functor (C ^op) (SET ℓ
         = funExt idFunExt
           where
             idFunExt : ∀ (un : fst (LF-ob c))
-                      → (LF-hom (C .id c) un) ≡ un
+                      → (LF-hom (C .id) un) ≡ un
             idFunExt (x , X) = ΣPathP (leftEq , rightEq)
               where
-                leftEq : (F ⟪ C .id c ⟫) x ≡ x
+                leftEq : (F ⟪ C .id ⟫) x ≡ x
                 leftEq i = F .F-id i x
 
                 rightEq : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
-                          ((P ⟪ C .id c , refl ⟫) X) X
+                          ((P ⟪ C .id , refl ⟫) X) X
                 rightEq = left ▷ right
                   where
                     -- the id morphism in (∫ᴾ F)
-                    ∫id = C .id c , sym (funExt⁻ (F .F-id) x ∙ refl)
+                    ∫id = C .id , sym (funExt⁻ (F .F-id) x ∙ refl)
 
                     -- functoriality of P gives us close to what we want
                     right : (P ⟪ ∫id ⟫) X ≡ X
                     right i = P .F-id i X
 
-                    -- but need to do more work to show that (C .id c , refl) ≡ ∫id
+                    -- but need to do more work to show that (C .id , refl) ≡ ∫id
                     left : PathP (λ i → fst (P ⟅ c , leftEq i ⟆))
-                                  ((P ⟪ C .id c , refl ⟫) X)
+                                  ((P ⟪ C .id , refl ⟫) X)
                                   ((P ⟪ ∫id ⟫) X)
-                    left i = (P ⟪ ∫ᴾhomEq {F = F} (C .id c , refl) ∫id (λ i → (c , leftEq i)) refl refl i ⟫) X
+                    left i = (P ⟪ ∫ᴾhomEq {F = F} (C .id , refl) ∫id (λ i → (c , leftEq i)) refl refl i ⟫) X
       L-ob-ob .F-seq {x = c} {d} {e} f g
         = funExt seqFunEq
           where
diff --git a/Cubical/Categories/Sets.agda b/Cubical/Categories/Sets.agda
deleted file mode 100644
index caabf85a85..0000000000
--- a/Cubical/Categories/Sets.agda
+++ /dev/null
@@ -1,93 +0,0 @@
-{-# OPTIONS --safe #-}
-
-module Cubical.Categories.Sets where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
-open import Cubical.Categories.NaturalTransformation
-
-open Precategory
-
-module _ ℓ where
-  SET : Precategory (ℓ-suc ℓ) ℓ
-  SET .ob = Σ (Type ℓ) isSet
-  SET .Hom[_,_] (A , _) (B , _) = A → B
-  SET .id _  = λ x → x
-  SET ._⋆_ f g = λ x → g (f x)
-  SET .⋆IdL f = refl
-  SET .⋆IdR f = refl
-  SET .⋆Assoc f g h = refl
-
-module _ {ℓ} where
-  isSetExpIdeal : {A B : Type ℓ} → isSet B → isSet (A → B)
-  isSetExpIdeal B/set = isSetΠ λ _ → B/set
-
-  isSetLift : {A : Type ℓ} → isSet A → isSet (Lift {ℓ} {ℓ-suc ℓ} A)
-  isSetLift = isOfHLevelLift 2
-
-  module _ {A B : SET ℓ .ob} where
-    -- monic/surjectiveness
-    open import Cubical.Categories.Morphism
-    isSurjSET : (f : SET ℓ [ A , B ]) → Type _
-    isSurjSET f = ∀ (b : fst B) → Σ[ a ∈ fst A ] f a ≡ b
-
-    -- isMonic→isSurjSET : {f : SET ℓ [ A , B ]}
-    --                   → isEpic {C = SET ℓ} {x = A} {y = B} f
-    --                   → isSurjSET f
-    -- isMonic→isSurjSET ism b = {!!} , {!!}
-
-  instance
-    SET-category : isCategory (SET ℓ)
-    SET-category .isSetHom {_} {B , B/set} = isSetExpIdeal B/set
-
-private
-  variable
-    ℓ ℓ' : Level
-
-open Functor
-
--- Hom functors
-_[-,_] : (C : Precategory ℓ ℓ') → (c : C .ob) → ⦃ isCat : isCategory C ⦄ → Functor (C ^op) (SET _)
-(C [-, c ]) ⦃ isCat ⦄ .F-ob x = (C [ x , c ]) , isCat .isSetHom
-(C [-, c ])           .F-hom f k = f ⋆⟨ C ⟩ k
-(C [-, c ])           .F-id = funExt λ _ → C .⋆IdL _
-(C [-, c ])           .F-seq _ _ = funExt λ _ → C .⋆Assoc _ _ _
-
-_[_,-] : (C : Precategory ℓ ℓ') → (c : C .ob) → ⦃ isCat : isCategory C ⦄ → Functor C (SET _)
-(C [ c ,-]) ⦃ isCat ⦄ .F-ob x = (C [ c , x ]) , isCat .isSetHom
-(C [ c ,-])           .F-hom f k = k ⋆⟨ C ⟩ f
-(C [ c ,-])           .F-id = funExt λ _ → C .⋆IdR _
-(C [ c ,-])           .F-seq _ _ = funExt λ _ → sym (C .⋆Assoc _ _ _)
-
-module _ {C : Precategory ℓ ℓ'} ⦃ _ : isCategory C ⦄ {F : Functor C (SET ℓ')} where
-  open NatTrans
-
-  -- natural transformations by pre/post composition
-  preComp : {x y : C .ob}
-          → (f : C [ x , y ])
-          → C [ x ,-] ⇒ F
-          → C [ y ,-] ⇒ F
-  preComp f α .N-ob c k = (α ⟦ c ⟧) (f ⋆⟨ C ⟩ k)
-  preComp f α .N-hom {x = c} {d} k
-    = (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ (l ⋆⟨ C ⟩ k)))
-    ≡[ i ]⟨ (λ l → (α ⟦ d ⟧) (⋆Assoc C f l k (~ i))) ⟩
-      (λ l → (α ⟦ d ⟧) (f ⋆⟨ C ⟩ l ⋆⟨ C ⟩ k))
-    ≡[ i ]⟨ (λ l → (α .N-hom k) i (f ⋆⟨ C ⟩ l)) ⟩
-      (λ l → (F ⟪ k ⟫) ((α ⟦ c ⟧) (f ⋆⟨ C ⟩ l)))
-    ∎
-
--- properties
--- TODO: move to own file
-open CatIso renaming (inv to cInv)
-open Iso
-
-Iso→CatIso : ∀ {A B : (SET ℓ) .ob}
-           → Iso (fst A) (fst B)
-           → CatIso {C = SET ℓ} A B
-Iso→CatIso is .mor = is .fun
-Iso→CatIso is .cInv = is .inv
-Iso→CatIso is .sec = funExt λ b → is .rightInv b -- is .rightInv
-Iso→CatIso is .ret = funExt λ b → is .leftInv b -- is .rightInv
diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda
index a5178cc8d2..8cecb7eacf 100644
--- a/Cubical/Categories/Yoneda.agda
+++ b/Cubical/Categories/Yoneda.agda
@@ -1,5 +1,4 @@
 {-# OPTIONS --safe #-}
-
 module Cubical.Categories.Yoneda where
 
 open import Cubical.Foundations.Prelude
@@ -24,12 +23,12 @@ private
 
 -- THE YONEDA LEMMA
 
+open isCategory
 open NatTrans
 open NatTransP
 open Functor
 open Iso
 
-
 module _ (A B : Type ℓ) (f : A → B) where
 
   isInj = ∀ (x y : A) → (f x ≡ f y) → x ≡ y
@@ -41,6 +40,7 @@ module _ (A B : Type ℓ) (f : A → B) where
 
 module _ {C : Precategory ℓ ℓ'} ⦃ isCatC : isCategory C ⦄ where
   open Precategory
+
   yoneda : (F : Functor C (SET ℓ'))
          → (c : C .ob)
          → Iso ((FUNCTOR C (SET ℓ')) [ C [ c ,-] , F ]) (fst (F ⟅ c ⟆))
@@ -51,7 +51,7 @@ module _ {C : Precategory ℓ ℓ'} ⦃ isCatC : isCategory C ⦄ where
 
       -- takes a natural transformation to what it does on id
       ϕ : natType → setType
-      ϕ α = (α ⟦ _ ⟧) (C .id c)
+      ϕ α = (α ⟦ _ ⟧) (C .id)
 
       -- takes an element x of F c and sends it to the (only) natural transformation
       -- which takes the identity to x
@@ -79,9 +79,9 @@ module _ {C : Precategory ℓ ℓ'} ⦃ isCatC : isCategory C ⦄ where
           αo≡βo = funExt λ x → funExt λ f
                 → αo x f
                 ≡[ i ]⟨ αo x (C .⋆IdL f (~ i)) ⟩ -- expand into the bottom left of the naturality diagram
-                  αo x (C .id c ⋆⟨ C ⟩ f)
-                ≡[ i ]⟨ αh f i (C .id c) ⟩ -- apply naturality
-                  (F ⟪ f ⟫) ((αo _) (C .id c))
+                  αo x (C .id ⋆⟨ C ⟩ f)
+                ≡[ i ]⟨ αh f i (C .id) ⟩ -- apply naturality
+                  (F ⟪ f ⟫) ((αo _) (C .id))
                 ∎
 
           -- type aliases for natural transformation
@@ -122,13 +122,13 @@ module _ {C : Precategory ℓ ℓ'} ⦃ isCatC : isCategory C ⦄ where
   yonedaIsNaturalInOb {F = F} c c' f = funExt (λ α
                              → (yoneda F c' .fun ◍ preComp f) α
                              ≡⟨ refl ⟩
-                               (α ⟦ c' ⟧) (f ⋆⟨ C ⟩ C .id c')
+                               (α ⟦ c' ⟧) (f ⋆⟨ C ⟩ C .id)
                              ≡[ i ]⟨ (α ⟦ c' ⟧) (C .⋆IdR f i) ⟩
                                (α ⟦ c' ⟧) f
                              ≡[ i ]⟨ (α ⟦ c' ⟧) (C .⋆IdL f (~ i)) ⟩
-                               (α ⟦ c' ⟧) (C .id c ⋆⟨ C ⟩ f)
-                             ≡[ i ]⟨ (α .N-hom f i) (C .id c) ⟩
-                               (F ⟪ f ⟫) ((α ⟦ c ⟧) (C .id c))
+                               (α ⟦ c' ⟧) (C .id ⋆⟨ C ⟩ f)
+                             ≡[ i ]⟨ (α .N-hom f i) (C .id) ⟩
+                               (F ⟪ f ⟫) ((α ⟦ c ⟧) (C .id))
                              ≡⟨ refl ⟩
                                ((F ⟪ f ⟫) ◍ yoneda F c .fun) α
                              ∎)
@@ -157,7 +157,7 @@ module _ {C : Precategory ℓ ℓ} ⦃ C-cat : isCategory C ⦄ where
 
   module _ {x} (F : Functor (C ^op) (SET ℓ)) where
     yo-yo-yo : NatTrans (yo x) F → F .F-ob x .fst
-    yo-yo-yo α = α .N-ob _ (id _)
+    yo-yo-yo α = α .N-ob _ id
 
     no-no-no : F .F-ob x .fst → NatTrans (yo x) F
     no-no-no a .N-ob y f = F .F-hom f a
@@ -172,8 +172,8 @@ module _ {C : Precategory ℓ ℓ} ⦃ C-cat : isCategory C ⦄ where
         rem : ∀ {z} (x₁ : C [ z , x ]) → F .F-hom x₁ (yo-yo-yo a) ≡ (a .N-ob z) x₁
         rem g =
           F .F-hom g (yo-yo-yo a)
-            ≡[ i ]⟨ a .N-hom g (~ i) (id x) ⟩
-          a .N-hom g i0 (id x)
+            ≡[ i ]⟨ a .N-hom g (~ i) id ⟩
+          a .N-hom g i0 id
             ≡[ i ]⟨ a .N-ob _ (⋆IdR g i) ⟩
           (a .N-ob _) g
             ∎