From bdfbb115375c148969b05f13d6873f79bedf4116 Mon Sep 17 00:00:00 2001
From: Nathan van Doorn <nvd1234@gmail.com>
Date: Sat, 16 Dec 2023 06:35:04 +0100
Subject: [PATCH] Categories.Category.Construction.KaroubiEnvelope.Properties:
 new function hierarchy

---
 .../Construction/KaroubiEnvelope/Properties.agda       | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda b/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
index a34240c75..410a6ab91 100644
--- a/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
+++ b/src/Categories/Category/Construction/KaroubiEnvelope/Properties.agda
@@ -43,16 +43,10 @@ private
   module KaroubiEmbedding = Functor KaroubiEmbedding
 
 karoubi-embedding-full : Full KaroubiEmbedding
-karoubi-embedding-full = record
-  { from = record
-    { _⟨$⟩_ = λ f → BundledIdem.Idempotent⇒.hom f
-    ; cong = λ eq → eq
-    }
-  ; right-inverse-of = λ _ → refl
-  }
+karoubi-embedding-full f = BundledIdem.Idempotent⇒.hom f , λ eq → eq
 
 karoubi-embedding-faithful : Faithful KaroubiEmbedding
-karoubi-embedding-faithful f g eq = eq
+karoubi-embedding-faithful eq = eq
 
 karoubi-embedding-fully-faithful : FullyFaithful KaroubiEmbedding
 karoubi-embedding-fully-faithful = karoubi-embedding-full , karoubi-embedding-faithful