diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 0ed99a3..11ddc3f 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -80,19 +80,20 @@ module _ {โ„“ : Level} where SetsHasProducts : HasProducts ๐“ข SetsHasProducts = record { product = product } -module _ {โ„“a โ„“b : Level} where - module _ (โ„‚ : Category โ„“a โ„“b) where - -- Covariant Presheaf - Representable : Set (โ„“a โŠ” lsuc โ„“b) - Representable = Functor โ„‚ (๐“ข๐“ฎ๐“ฝ โ„“b) +module _ {โ„“a โ„“b : Level} (โ„‚ : Category โ„“a โ„“b) where + -- Covariant Presheaf + Representable : Set (โ„“a โŠ” lsuc โ„“b) + Representable = Functor โ„‚ (๐“ข๐“ฎ๐“ฝ โ„“b) - -- Contravariant Presheaf - Presheaf : Set (โ„“a โŠ” lsuc โ„“b) - Presheaf = Functor (opposite โ„‚) (๐“ข๐“ฎ๐“ฝ โ„“b) + -- Contravariant Presheaf + Presheaf : Set (โ„“a โŠ” lsuc โ„“b) + Presheaf = Functor (opposite โ„‚) (๐“ข๐“ฎ๐“ฝ โ„“b) + + open Category โ„‚ -- The "co-yoneda" embedding. - representable : {โ„‚ : Category โ„“a โ„“b} โ†’ Category.Object โ„‚ โ†’ Representable โ„‚ - representable {โ„‚ = โ„‚} A = record + representable : Category.Object โ„‚ โ†’ Representable + representable A = record { raw = record { func* = ฮป B โ†’ โ„‚ [ A , B ] , arrowsAreSets ; funcโ†’ = โ„‚ [_โˆ˜_] @@ -102,12 +103,10 @@ module _ {โ„“a โ„“b : Level} where ; isDistributive = funExt ฮป x โ†’ sym isAssociative } } - where - open Category โ„‚ -- Alternate name: `yoneda` - presheaf : {โ„‚ : Category โ„“a โ„“b} โ†’ Category.Object (opposite โ„‚) โ†’ Presheaf โ„‚ - presheaf {โ„‚ = โ„‚} B = record + presheaf : Category.Object (opposite โ„‚) โ†’ Presheaf + presheaf B = record { raw = record { func* = ฮป A โ†’ โ„‚ [ A , B ] , arrowsAreSets ; funcโ†’ = ฮป f g โ†’ โ„‚ [ g โˆ˜ f ] @@ -117,5 +116,3 @@ module _ {โ„“a โ„“b : Level} where ; isDistributive = funExt ฮป x โ†’ isAssociative } } - where - open Category โ„‚ diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index be6e6b6..df39252 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -26,7 +26,7 @@ module _ {โ„“ : Level} {โ„‚ : Category โ„“ โ„“} (unprovable : IsCategory (RawCat open Fun (opposite โ„‚) ๐“ข Catโ„“ : Category _ _ Catโ„“ = Cat.Cat โ„“ โ„“ unprovable - prshf = presheaf {โ„‚ = โ„‚} + prshf = presheaf โ„‚ module โ„‚ = Category โ„‚ _โ‡‘_ : (A B : Category.Object Catโ„“) โ†’ Category.Object Catโ„“