diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda
index 326152a..19cabeb 100644
--- a/src/Cat/Categories/Free.agda
+++ b/src/Cat/Categories/Free.agda
@@ -9,14 +9,6 @@ open import Cat.Category
 
 open IsCategory
 
--- data Path {ℓ : Level} {A : Set ℓ} : (a b : A) → Set ℓ where
---   emptyPath : {a : A} → Path a a
---   concatenate : {a b c : A} → Path a b → Path b c → Path a b
-
--- import Data.List
--- P : (a b : Object ℂ) → Set (ℓ ⊔ ℓ')
--- P = {!Data.List.List ?!}
--- Generalized paths:
 data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where
   empty : {a : A} → Path R a a
   cons : {a b c : A} → R b c → Path R a b → Path R a c
diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda
index c3c333d..d6b3dc0 100644
--- a/src/Cat/Equality.agda
+++ b/src/Cat/Equality.agda
@@ -20,28 +20,3 @@ module Equality where
         Σ≡ : a ≡ b
         proj₁ (Σ≡ i) = proj₁≡ i
         proj₂ (Σ≡ i) = proj₂≡ i
-
-        -- Remark 2.7.1: This theorem:
-        --
-        --   (x , u) ≡ (x , v) → u ≡ v
-        --
-        -- does *not* hold! We can only conclude that there *exists* `p : x ≡ x`
-        -- such that
-        --
-        --   p* u ≡ v
-        -- thm : isSet A → (∀ {a} → isSet (B a)) → isSet (Σ A B)
-        -- thm sA sB (x , y) (x' , y') p q = res
-        --   where
-        --     x≡x'0 : x ≡ x'
-        --     x≡x'0 = λ i → proj₁ (p i)
-        --     x≡x'1 : x ≡ x'
-        --     x≡x'1 = λ i → proj₁ (q i)
-        --     someP : x ≡ x'
-        --     someP = {!!}
-        --     tricky : {!y!} ≡ y'
-        --     tricky = {!!}
-        --     -- res' : (λ _ → Σ A B) [ (x , y) ≡ (x' , y') ]
-        --     res' : ({!!} , {!!}) ≡ ({!!} , {!!})
-        --     res' = {!!}
-        --     res : p ≡ q
-        --     res i = {!res'!}