2018-02-05 13:47:15 +00:00
|
|
|
|
{-# OPTIONS --allow-unsolved-metas --cubical #-}
|
2018-01-15 15:13:23 +00:00
|
|
|
|
module Cat.Categories.Sets where
|
2017-11-15 20:51:10 +00:00
|
|
|
|
|
2018-01-30 10:19:48 +00:00
|
|
|
|
open import Cubical
|
2017-11-15 20:51:10 +00:00
|
|
|
|
open import Agda.Primitive
|
2018-01-15 15:13:23 +00:00
|
|
|
|
open import Data.Product
|
2018-02-05 10:43:38 +00:00
|
|
|
|
import Function
|
2018-01-15 15:13:23 +00:00
|
|
|
|
|
|
|
|
|
open import Cat.Category
|
2018-02-05 13:59:53 +00:00
|
|
|
|
open import Cat.Category.Functor
|
|
|
|
|
open import Cat.Category.Product
|
2017-11-15 20:51:10 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
module _ (ℓ : Level) where
|
|
|
|
|
private
|
|
|
|
|
open RawCategory
|
|
|
|
|
open IsCategory
|
|
|
|
|
open import Cubical.Univalence
|
|
|
|
|
open import Cubical.NType.Properties
|
|
|
|
|
open import Cubical.Universe
|
|
|
|
|
|
|
|
|
|
SetsRaw : RawCategory (lsuc ℓ) ℓ
|
2018-02-23 12:20:30 +00:00
|
|
|
|
Object SetsRaw = hSet
|
2018-02-21 12:37:07 +00:00
|
|
|
|
Arrow SetsRaw (T , _) (U , _) = T → U
|
|
|
|
|
𝟙 SetsRaw = Function.id
|
|
|
|
|
_∘_ SetsRaw = Function._∘′_
|
|
|
|
|
|
|
|
|
|
SetsIsCategory : IsCategory SetsRaw
|
2018-02-23 11:43:49 +00:00
|
|
|
|
isAssociative SetsIsCategory = refl
|
2018-02-23 11:49:41 +00:00
|
|
|
|
proj₁ (isIdentity SetsIsCategory) = funExt λ _ → refl
|
|
|
|
|
proj₂ (isIdentity SetsIsCategory) = funExt λ _ → refl
|
2018-02-23 11:51:44 +00:00
|
|
|
|
arrowsAreSets SetsIsCategory {B = (_ , s)} = setPi λ _ → s
|
2018-02-21 12:37:07 +00:00
|
|
|
|
univalent SetsIsCategory = {!!}
|
|
|
|
|
|
|
|
|
|
𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
|
|
|
|
|
Category.raw 𝓢𝓮𝓽 = SetsRaw
|
|
|
|
|
Category.isCategory 𝓢𝓮𝓽 = SetsIsCategory
|
|
|
|
|
Sets = 𝓢𝓮𝓽
|
2018-01-24 15:38:28 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
module _ {ℓ : Level} where
|
2018-01-24 15:38:28 +00:00
|
|
|
|
private
|
2018-02-21 12:37:07 +00:00
|
|
|
|
𝓢 = 𝓢𝓮𝓽 ℓ
|
|
|
|
|
open Category 𝓢
|
|
|
|
|
open import Cubical.Sigma
|
|
|
|
|
|
|
|
|
|
module _ (0A 0B : Object) where
|
|
|
|
|
private
|
|
|
|
|
A : Set ℓ
|
|
|
|
|
A = proj₁ 0A
|
|
|
|
|
sA : isSet A
|
|
|
|
|
sA = proj₂ 0A
|
|
|
|
|
B : Set ℓ
|
|
|
|
|
B = proj₁ 0B
|
|
|
|
|
sB : isSet B
|
|
|
|
|
sB = proj₂ 0B
|
|
|
|
|
0A×0B : Object
|
|
|
|
|
0A×0B = (A × B) , sigPresSet sA λ _ → sB
|
|
|
|
|
|
|
|
|
|
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
|
|
|
|
|
_&&&_ : (X → A × B)
|
|
|
|
|
_&&&_ x = f x , g x
|
|
|
|
|
module _ {0X : Object} where
|
|
|
|
|
X = proj₁ 0X
|
|
|
|
|
module _ (f : X → A ) (g : X → B) where
|
|
|
|
|
lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g
|
|
|
|
|
proj₁ lem = refl
|
|
|
|
|
proj₂ lem = refl
|
|
|
|
|
instance
|
|
|
|
|
isProduct : IsProduct 𝓢 {0A} {0B} {0A×0B} proj₁ proj₂
|
|
|
|
|
isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g
|
|
|
|
|
|
|
|
|
|
product : Product {ℂ = 𝓢} 0A 0B
|
|
|
|
|
product = record
|
|
|
|
|
{ obj = 0A×0B
|
|
|
|
|
; proj₁ = Data.Product.proj₁
|
|
|
|
|
; proj₂ = Data.Product.proj₂
|
|
|
|
|
; isProduct = λ { {X} → isProduct {X = X}}
|
|
|
|
|
}
|
2018-01-24 15:38:28 +00:00
|
|
|
|
|
|
|
|
|
instance
|
2018-02-21 12:37:07 +00:00
|
|
|
|
SetsHasProducts : HasProducts 𝓢
|
2018-01-24 15:38:28 +00:00
|
|
|
|
SetsHasProducts = record { product = product }
|
2017-11-15 20:51:10 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
module _ {ℓa ℓb : Level} where
|
|
|
|
|
module _ (ℂ : Category ℓa ℓb) where
|
|
|
|
|
-- Covariant Presheaf
|
|
|
|
|
Representable : Set (ℓa ⊔ lsuc ℓb)
|
|
|
|
|
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
|
|
|
|
|
|
|
|
|
|
-- Contravariant Presheaf
|
|
|
|
|
Presheaf : Set (ℓa ⊔ lsuc ℓb)
|
2018-02-25 14:23:33 +00:00
|
|
|
|
Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
|
2018-01-17 11:16:07 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
-- The "co-yoneda" embedding.
|
|
|
|
|
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
|
|
|
|
|
representable {ℂ = ℂ} A = record
|
|
|
|
|
{ raw = record
|
2018-02-23 11:51:44 +00:00
|
|
|
|
{ func* = λ B → ℂ [ A , B ] , arrowsAreSets
|
2018-02-21 12:37:07 +00:00
|
|
|
|
; func→ = ℂ [_∘_]
|
|
|
|
|
}
|
|
|
|
|
; isFunctor = record
|
2018-02-23 11:49:41 +00:00
|
|
|
|
{ isIdentity = funExt λ _ → proj₂ isIdentity
|
2018-02-23 11:53:35 +00:00
|
|
|
|
; isDistributive = funExt λ x → sym isAssociative
|
2018-02-21 12:37:07 +00:00
|
|
|
|
}
|
2018-02-06 13:24:34 +00:00
|
|
|
|
}
|
2018-02-21 12:37:07 +00:00
|
|
|
|
where
|
|
|
|
|
open Category ℂ
|
|
|
|
|
|
|
|
|
|
-- Alternate name: `yoneda`
|
2018-02-25 14:23:33 +00:00
|
|
|
|
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
|
2018-02-21 12:37:07 +00:00
|
|
|
|
presheaf {ℂ = ℂ} B = record
|
|
|
|
|
{ raw = record
|
2018-02-23 11:51:44 +00:00
|
|
|
|
{ func* = λ A → ℂ [ A , B ] , arrowsAreSets
|
2018-02-21 12:37:07 +00:00
|
|
|
|
; func→ = λ f g → ℂ [ g ∘ f ]
|
2018-01-30 15:23:36 +00:00
|
|
|
|
}
|
2018-02-21 12:37:07 +00:00
|
|
|
|
; isFunctor = record
|
2018-02-23 11:49:41 +00:00
|
|
|
|
{ isIdentity = funExt λ x → proj₁ isIdentity
|
2018-02-23 11:53:35 +00:00
|
|
|
|
; isDistributive = funExt λ x → isAssociative
|
2018-02-21 12:37:07 +00:00
|
|
|
|
}
|
2018-01-30 15:23:36 +00:00
|
|
|
|
}
|
2018-02-21 12:37:07 +00:00
|
|
|
|
where
|
|
|
|
|
open Category ℂ
|