From 6941f1557f6d9ec8b72708d989904442dbfe6320 Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Mon, 21 Oct 2024 14:54:54 +0200 Subject: [PATCH 1/3] Yoneda embedding. Clean up code in BinProduct. --- .../Categories/Constructions/BinProduct.agda | 26 ++++++++++++------- .../Categories/Functors/YonedaEmbedding.agda | 21 +++++++++++++++ 2 files changed, 37 insertions(+), 10 deletions(-) create mode 100644 Cubical/Categories/Functors/YonedaEmbedding.agda 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))) From 96f21a2adca8bd54a45f9d9f9a82271007fa236a Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Mon, 21 Oct 2024 15:22:37 +0200 Subject: [PATCH 2/3] Fix whitespace crime --- Cubical/Categories/Constructions/BinProduct.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Categories/Constructions/BinProduct.agda b/Cubical/Categories/Constructions/BinProduct.agda index d2e424c743..1b9c87aa6c 100644 --- a/Cubical/Categories/Constructions/BinProduct.agda +++ b/Cubical/Categories/Constructions/BinProduct.agda @@ -109,7 +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`" #-} From 216268e0319b9adfaec25cce0c49f47e305712fa Mon Sep 17 00:00:00 2001 From: Andreas Nuyts Date: Fri, 25 Oct 2024 19:09:17 +0200 Subject: [PATCH 3/3] Un-add YonedaEmbedding. --- .../Categories/Functors/YonedaEmbedding.agda | 21 ------------------- 1 file changed, 21 deletions(-) delete mode 100644 Cubical/Categories/Functors/YonedaEmbedding.agda 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)))