diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda
index da80ea1b07..d2e424c743 100644
--- a/Cubical/Categories/Constructions/BinProduct.agda
+++ b/Cubical/Categories/Constructions/BinProduct.agda
@@ -68,22 +68,30 @@ module _ where
 Δ : ∀ (C : Category ℓC ℓC') → Functor C (C ×C C)
 Δ C = Id ,F Id
 
-Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C)
-Sym {C = C}{D = D} = Snd C D ,F Fst C D
-
 -- Some useful functors
 module _ (C : Category ℓC ℓC')
          (D : Category ℓD ℓD') where
   open Functor
 
+  -- Symmetry of cartesian product (swapping components)
+  ×C-sym : Functor (C ×C D) (D ×C C)
+  ×C-sym = Snd C D ,F Fst C D
+  -- TODO: Prove involution
+
   module _ (E : Category ℓE ℓE') where
-    -- Associativity of product
+    -- Associativity of cartesian product
     ×C-assoc : Functor (C ×C (D ×C E)) ((C ×C D) ×C E)
     ×C-assoc .F-ob (c , (d , e)) = ((c , d), e)
     ×C-assoc .F-hom (f , (g , h)) = ((f , g), h)
     ×C-assoc .F-id = refl
     ×C-assoc .F-seq _ _ = refl
 
+    {-
+      TODO:
+        - define inverse to `assoc`, prove isomorphism
+        - prove product is commutative up to isomorphism
+    -}
+
   -- Left/right injections into product
   linj : (d : ob D) → Functor C (C ×C D)
   linj d = Id ,F Constant C D d
@@ -91,12 +99,6 @@ module _ (C : Category ℓC ℓC')
   rinj : (c : ob C) → Functor D (C ×C D)
   rinj c = Constant D C c ,F Id
 
-{-
-  TODO:
-    - define inverse to `assoc`, prove isomorphism
-    - prove product is commutative up to isomorphism
--}
-
 
   -- The isomorphisms in product category
 
@@ -107,3 +109,7 @@ module _ (C : Category ℓC ℓC')
   CatIso× f g .snd .inv = f .snd .inv , g .snd .inv
   CatIso× f g .snd .sec i = f .snd .sec i , g .snd .sec i
   CatIso× f g .snd .ret i = f .snd .ret i , g .snd .ret i
+  
+Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C)
+Sym {C = C}{D = D} = Snd C D ,F Fst C D
+{-# WARNING_ON_USAGE Sym "DEPRECATED: Use `×C-sym` instead of `Sym`" #-}
diff --git a/Cubical/Categories/Functors/YonedaEmbedding.agda b/Cubical/Categories/Functors/YonedaEmbedding.agda
new file mode 100644
index 0000000000..30ff28a1c4
--- /dev/null
+++ b/Cubical/Categories/Functors/YonedaEmbedding.agda
@@ -0,0 +1,21 @@
+{-# 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)))