From 059c74b687c587d165d277ff45b1de6b4504fab4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 11:15:45 +0100
Subject: [PATCH] Use already defined category

---
 src/Cat/Category/Yoneda.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index abd76d0..be6e6b6 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -25,7 +25,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
     𝓢 = Sets ℓ
     open Fun (opposite ℂ) 𝓢
     Catℓ : Category _ _
-    Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
+    Catℓ = Cat.Cat ℓ ℓ unprovable
     prshf = presheaf {ℂ = ℂ}
     module ℂ = Category ℂ