open import Category -- https://github.com/konn/category-agda                                                                                     
open import Level
open import Category.Sets

module freyd {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
     (C : Category zero zero zero )
  where

open import Relation.Binary.Core

postulate ≈→≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y  ]) → x ≡ y


-- record SmallCategory