Categories.Category.Construction.KaroubiEnvelope.Properties: new func…

…tion hierarchy
agda · Dec 16, 2023 · bdfbb11 · bdfbb11
1 parent e5b2f35
commit bdfbb11
Showing 1 changed file with 2 additions and 8 deletions.
diff --git 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