From ee2e84edfefeff9c1c99178e3ae0563e2d40cf9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 25 Jan 2018 14:11:28 +0100
Subject: [PATCH] Remove unused bindings

---
 src/Cat/Categories/Cat.agda      | 2 --
 src/Cat/Category/Properties.agda | 3 ++-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 4bac632..1bd1c51 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -34,8 +34,6 @@ module _ (ℓ ℓ' : Level) where
           (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y))
           (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
         eq→ = refl
-        id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
-        id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
         postulate eqI : PathP
                    (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c})
                    (ident ((h ∘f (g ∘f f))))
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 35a4a39..a641f28 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -74,6 +74,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
     :func*: A = {!!}
 
     -- prsh = presheaf {ℂ = ℂ}
+    -- k = prsh {!!}
     -- :func*:' : ℂ .Object → Presheaf ℂ
     -- :func*:' = prsh
     -- module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
@@ -83,7 +84,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
   yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ))
   yoneda = record
     { func* = :func*:
-    ; func→ = {!:func→:'!}
+    ; func→ = {!!}
     ; ident = {!!}
     ; distrib = {!!}
     }