Make sets a category according to HoTT
This commit is contained in:
parent
ed40824edc
commit
57d7eab4cb
|
|
@ -9,80 +9,116 @@ import Function
|
|||
open import Cat.Category
|
||||
open import Cat.Category.Functor
|
||||
open import Cat.Category.Product
|
||||
open Category
|
||||
|
||||
module _ (ℓ : Level) where
|
||||
private
|
||||
open RawCategory
|
||||
open IsCategory
|
||||
open import Cubical.Univalence
|
||||
open import Cubical.NType.Properties
|
||||
open import Cubical.Universe
|
||||
|
||||
SetsRaw : RawCategory (lsuc ℓ) ℓ
|
||||
Object SetsRaw = Cubical.Universe.0-Set
|
||||
Arrow SetsRaw (T , _) (U , _) = T → U
|
||||
𝟙 SetsRaw = Function.id
|
||||
_∘_ SetsRaw = Function._∘′_
|
||||
|
||||
setIsSet : (A : Set ℓ) → isSet A
|
||||
setIsSet A x y p q = {!ua!}
|
||||
|
||||
SetsIsCategory : IsCategory SetsRaw
|
||||
assoc SetsIsCategory = refl
|
||||
proj₁ (ident SetsIsCategory) = funExt λ _ → refl
|
||||
proj₂ (ident SetsIsCategory) = funExt λ _ → refl
|
||||
arrowIsSet SetsIsCategory {B = (_ , s)} = setPi λ _ → s
|
||||
univalent SetsIsCategory = {!!}
|
||||
|
||||
𝓢𝓮𝓽 Sets : Category (lsuc ℓ) ℓ
|
||||
Category.raw 𝓢𝓮𝓽 = SetsRaw
|
||||
Category.isCategory 𝓢𝓮𝓽 = SetsIsCategory
|
||||
Sets = 𝓢𝓮𝓽
|
||||
|
||||
module _ {ℓ : Level} where
|
||||
SetsRaw : RawCategory (lsuc ℓ) ℓ
|
||||
RawCategory.Object SetsRaw = Set ℓ
|
||||
RawCategory.Arrow SetsRaw = λ T U → T → U
|
||||
RawCategory.𝟙 SetsRaw = Function.id
|
||||
RawCategory._∘_ SetsRaw = Function._∘′_
|
||||
|
||||
open IsCategory
|
||||
SetsIsCategory : IsCategory SetsRaw
|
||||
assoc SetsIsCategory = refl
|
||||
proj₁ (ident SetsIsCategory) = funExt λ _ → refl
|
||||
proj₂ (ident SetsIsCategory) = funExt λ _ → refl
|
||||
arrowIsSet SetsIsCategory = {!!}
|
||||
univalent SetsIsCategory = {!!}
|
||||
|
||||
Sets : Category (lsuc ℓ) ℓ
|
||||
raw Sets = SetsRaw
|
||||
isCategory Sets = SetsIsCategory
|
||||
|
||||
private
|
||||
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
|
||||
_&&&_ : (X → A × B)
|
||||
_&&&_ x = f x , g x
|
||||
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
|
||||
lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
|
||||
proj₁ lem = refl
|
||||
proj₂ lem = refl
|
||||
instance
|
||||
isProduct : {A B : Object Sets} → IsProduct Sets {A} {B} proj₁ proj₂
|
||||
isProduct f g = f &&& g , lem f g
|
||||
𝓢 = 𝓢𝓮𝓽 ℓ
|
||||
open Category 𝓢
|
||||
open import Cubical.Sigma
|
||||
|
||||
product : (A B : Object Sets) → Product {ℂ = Sets} A B
|
||||
product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
|
||||
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}}
|
||||
}
|
||||
|
||||
instance
|
||||
SetsHasProducts : HasProducts Sets
|
||||
SetsHasProducts : HasProducts 𝓢
|
||||
SetsHasProducts = record { product = product }
|
||||
|
||||
-- Covariant Presheaf
|
||||
Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
|
||||
Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
|
||||
module _ {ℓa ℓb : Level} where
|
||||
module _ (ℂ : Category ℓa ℓb) where
|
||||
-- Covariant Presheaf
|
||||
Representable : Set (ℓa ⊔ lsuc ℓb)
|
||||
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
|
||||
|
||||
-- The "co-yoneda" embedding.
|
||||
representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
|
||||
representable {ℂ = ℂ} A = record
|
||||
{ raw = record
|
||||
{ func* = λ B → ℂ [ A , B ]
|
||||
; func→ = ℂ [_∘_]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ ident = funExt λ _ → proj₂ ident
|
||||
; distrib = funExt λ x → sym assoc
|
||||
}
|
||||
}
|
||||
where
|
||||
open IsCategory (isCategory ℂ)
|
||||
-- Contravariant Presheaf
|
||||
Presheaf : Set (ℓa ⊔ lsuc ℓb)
|
||||
Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
|
||||
|
||||
-- Contravariant Presheaf
|
||||
Presheaf : ∀ {ℓ ℓ'} (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ')
|
||||
Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
|
||||
|
||||
-- Alternate name: `yoneda`
|
||||
presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
|
||||
presheaf {ℂ = ℂ} B = record
|
||||
{ raw = record
|
||||
{ func* = λ A → ℂ [ A , B ]
|
||||
; func→ = λ f g → ℂ [ g ∘ f ]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ ident = funExt λ x → proj₁ ident
|
||||
; distrib = funExt λ x → assoc
|
||||
-- The "co-yoneda" embedding.
|
||||
representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
|
||||
representable {ℂ = ℂ} A = record
|
||||
{ raw = record
|
||||
{ func* = λ B → ℂ [ A , B ] , arrowIsSet
|
||||
; func→ = ℂ [_∘_]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ ident = funExt λ _ → proj₂ ident
|
||||
; distrib = funExt λ x → sym assoc
|
||||
}
|
||||
}
|
||||
}
|
||||
where
|
||||
open IsCategory (isCategory ℂ)
|
||||
where
|
||||
open Category ℂ
|
||||
|
||||
-- Alternate name: `yoneda`
|
||||
presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
|
||||
presheaf {ℂ = ℂ} B = record
|
||||
{ raw = record
|
||||
{ func* = λ A → ℂ [ A , B ] , arrowIsSet
|
||||
; func→ = λ f g → ℂ [ g ∘ f ]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ ident = funExt λ x → proj₁ ident
|
||||
; distrib = funExt λ x → assoc
|
||||
}
|
||||
}
|
||||
where
|
||||
open Category ℂ
|
||||
|
|
|
|||
|
|
@ -84,6 +84,7 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
|||
idIso : (A : Object) → A ≅ A
|
||||
idIso A = 𝟙 , (𝟙 , ident)
|
||||
|
||||
-- Lemma 9.1.4 in [HoTT]
|
||||
id-to-iso : (A B : Object) → A ≡ B → A ≅ B
|
||||
id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A)
|
||||
|
||||
|
|
@ -93,12 +94,6 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
|||
Univalent : Set (ℓa ⊔ ℓb)
|
||||
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
|
||||
|
||||
-- Thierry: All projections must be `isProp`'s
|
||||
|
||||
-- According to definitions 9.1.1 and 9.1.6 in the HoTT book the
|
||||
-- arrows of a category form a set (arrow-is-set), and there is an
|
||||
-- equivalence between the equality of objects and isomorphisms
|
||||
-- (univalent).
|
||||
record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||
open RawCategory ℂ
|
||||
open Univalence ℂ public
|
||||
|
|
@ -192,14 +187,16 @@ record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
{{isCategory}} : IsCategory raw
|
||||
|
||||
open RawCategory raw public
|
||||
open IsCategory isCategory public
|
||||
|
||||
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||
open Category ℂ
|
||||
_[_,_] : (A : Object) → (B : Object) → Set ℓb
|
||||
_[_,_] = Arrow
|
||||
|
||||
_[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
|
||||
_[_∘_] = _∘_
|
||||
|
||||
|
||||
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||
private
|
||||
open Category ℂ
|
||||
|
|
@ -210,8 +207,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
RawCategory.𝟙 OpRaw = 𝟙
|
||||
RawCategory._∘_ OpRaw = Function.flip _∘_
|
||||
|
||||
open IsCategory isCategory
|
||||
|
||||
OpIsCategory : IsCategory OpRaw
|
||||
IsCategory.assoc OpIsCategory = sym assoc
|
||||
IsCategory.ident OpIsCategory = swap ident
|
||||
|
|
|
|||
Loading…
Reference in a new issue