diff --git a/Cubical/Categories/Functors/YonedaEmbedding.agda b/Cubical/Categories/Functors/YonedaEmbedding.agda deleted file mode 100644 index 30ff28a1c4..0000000000 --- a/Cubical/Categories/Functors/YonedaEmbedding.agda +++ /dev/null @@ -1,21 +0,0 @@ -{-# OPTIONS --safe #-} - -module Cubical.Categories.Functors.YonedaEmbedding where - -open import Cubical.Foundations.Prelude -open import Cubical.Categories.Category -open import Cubical.Categories.Functor.Base -open import Cubical.Categories.Instances.Sets -open import Cubical.Categories.Constructions.BinProduct -open import Cubical.Categories.Presheaf -open import Cubical.Categories.Functors.HomFunctor -open import Cubical.Categories.Instances.Functors.Currying - -private - variable - ℓC ℓC' : Level - -module _ (C : Category ℓC ℓC') where - - YonedaEmbedding : Functor C (PresheafCategory C ℓC') - YonedaEmbedding = λF (C ^op) (SET ℓC') C (funcComp (HomFunctor C) (×C-sym C (C ^op)))