2018-03-08 13:44:23 +00:00
|
|
|
|
-- | The category of homotopy sets
|
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
|
|
|
|
|
|
|
|
|
open import Agda.Primitive
|
2018-01-15 15:13:23 +00:00
|
|
|
|
open import Data.Product
|
2018-03-12 12:36:55 +00:00
|
|
|
|
open import Function using (_∘_)
|
|
|
|
|
|
|
|
|
|
open import Cubical hiding (_≃_ ; inverse)
|
|
|
|
|
open import Cubical.Equivalence
|
|
|
|
|
renaming
|
|
|
|
|
( _≅_ to _A≅_ )
|
|
|
|
|
using
|
|
|
|
|
(_≃_ ; con ; AreInverses)
|
|
|
|
|
open import Cubical.Univalence
|
2018-03-08 13:44:23 +00:00
|
|
|
|
open import Cubical.GradLemma
|
|
|
|
|
|
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
|
2018-03-08 13:44:23 +00:00
|
|
|
|
open import Cat.Wishlist
|
2017-11-15 20:51:10 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
module _ (ℓ : Level) where
|
|
|
|
|
private
|
|
|
|
|
open import Cubical.Univalence
|
|
|
|
|
open import Cubical.NType.Properties
|
|
|
|
|
open import Cubical.Universe
|
|
|
|
|
|
|
|
|
|
SetsRaw : RawCategory (lsuc ℓ) ℓ
|
2018-03-08 13:44:23 +00:00
|
|
|
|
RawCategory.Object SetsRaw = hSet
|
|
|
|
|
RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U
|
|
|
|
|
RawCategory.𝟙 SetsRaw = Function.id
|
|
|
|
|
RawCategory._∘_ SetsRaw = Function._∘′_
|
|
|
|
|
|
2018-03-12 12:36:55 +00:00
|
|
|
|
open RawCategory SetsRaw hiding (_∘_)
|
2018-03-08 13:44:23 +00:00
|
|
|
|
open Univalence SetsRaw
|
|
|
|
|
|
|
|
|
|
isIdentity : IsIdentity Function.id
|
|
|
|
|
proj₁ isIdentity = funExt λ _ → refl
|
|
|
|
|
proj₂ isIdentity = funExt λ _ → refl
|
|
|
|
|
|
|
|
|
|
arrowsAreSets : ArrowsAreSets
|
|
|
|
|
arrowsAreSets {B = (_ , s)} = setPi λ _ → s
|
|
|
|
|
|
|
|
|
|
module _ {hA hB : Object} where
|
|
|
|
|
private
|
|
|
|
|
A = proj₁ hA
|
|
|
|
|
isSetA : isSet A
|
|
|
|
|
isSetA = proj₂ hA
|
|
|
|
|
B = proj₁ hB
|
|
|
|
|
isSetB : isSet B
|
|
|
|
|
isSetB = proj₂ hB
|
|
|
|
|
|
|
|
|
|
toIsomorphism : A ≃ B → hA ≅ hB
|
|
|
|
|
toIsomorphism e = obverse , inverse , verso-recto , recto-verso
|
|
|
|
|
where
|
|
|
|
|
open _≃_ e
|
|
|
|
|
|
|
|
|
|
fromIsomorphism : hA ≅ hB → A ≃ B
|
|
|
|
|
fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto)
|
|
|
|
|
where
|
|
|
|
|
obverse : A → B
|
|
|
|
|
obverse = proj₁ iso
|
|
|
|
|
inverse : B → A
|
|
|
|
|
inverse = proj₁ (proj₂ iso)
|
|
|
|
|
-- FIXME IsInverseOf should change name to AreInverses and the
|
|
|
|
|
-- ordering should be swapped.
|
|
|
|
|
areInverses : IsInverseOf {A = hA} {hB} obverse inverse
|
|
|
|
|
areInverses = proj₂ (proj₂ iso)
|
2018-03-12 12:36:55 +00:00
|
|
|
|
verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a
|
2018-03-08 13:44:23 +00:00
|
|
|
|
verso-recto a i = proj₁ areInverses i a
|
|
|
|
|
recto-verso : ∀ b → (obverse Function.∘ inverse) b ≡ b
|
|
|
|
|
recto-verso b i = proj₂ areInverses i b
|
|
|
|
|
|
2018-03-12 12:36:55 +00:00
|
|
|
|
private
|
|
|
|
|
univIso : (A ≡ B) A≅ (A ≃ B)
|
|
|
|
|
univIso = _≃_.toIsomorphism univalence
|
|
|
|
|
obverse' : A ≡ B → A ≃ B
|
|
|
|
|
obverse' = proj₁ univIso
|
|
|
|
|
inverse' : A ≃ B → A ≡ B
|
|
|
|
|
inverse' = proj₁ (proj₂ univIso)
|
|
|
|
|
-- Drop proof of being a set from both sides of an equality.
|
|
|
|
|
dropP : hA ≡ hB → A ≡ B
|
|
|
|
|
dropP eq i = proj₁ (eq i)
|
|
|
|
|
-- Add proof of being a set to both sides of a set-theoretic equivalence
|
|
|
|
|
-- returning a category-theoretic equivalence.
|
|
|
|
|
addE : A A≅ B → hA ≅ hB
|
|
|
|
|
addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair
|
2018-03-08 13:44:23 +00:00
|
|
|
|
where
|
2018-03-12 12:36:55 +00:00
|
|
|
|
areeqv = proj₂ (proj₂ eqv)
|
|
|
|
|
asPair =
|
|
|
|
|
let module Inv = AreInverses areeqv
|
|
|
|
|
in Inv.verso-recto , Inv.recto-verso
|
2018-03-08 13:44:23 +00:00
|
|
|
|
|
2018-03-12 12:36:55 +00:00
|
|
|
|
obverse : hA ≡ hB → hA ≅ hB
|
|
|
|
|
obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
|
|
|
|
|
|
|
|
|
|
-- Drop proof of being a set form both sides of a category-theoretic
|
|
|
|
|
-- equivalence returning a set-theoretic equivalence.
|
|
|
|
|
dropE : hA ≅ hB → A A≅ B
|
|
|
|
|
dropE eqv = obv , inv , asAreInverses
|
2018-03-08 13:44:23 +00:00
|
|
|
|
where
|
2018-03-12 12:36:55 +00:00
|
|
|
|
obv = proj₁ eqv
|
|
|
|
|
inv = proj₁ (proj₂ eqv)
|
|
|
|
|
areEq = proj₂ (proj₂ eqv)
|
|
|
|
|
asAreInverses : AreInverses A B obv inv
|
|
|
|
|
asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq }
|
|
|
|
|
|
|
|
|
|
-- Dunno if this is a thing.
|
|
|
|
|
isoToEquiv : A A≅ B → A ≃ B
|
|
|
|
|
isoToEquiv = {!!}
|
|
|
|
|
-- Add proof of being a set to both sides of an equality.
|
|
|
|
|
addP : A ≡ B → hA ≡ hB
|
|
|
|
|
addP p = lemSig (λ X → propPi λ x → propPi (λ y → propIsProp)) hA hB p
|
|
|
|
|
inverse : hA ≅ hB → hA ≡ hB
|
|
|
|
|
inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE
|
|
|
|
|
|
|
|
|
|
-- open AreInverses (proj₂ (proj₂ univIso)) renaming
|
|
|
|
|
-- ( verso-recto to verso-recto'
|
|
|
|
|
-- ; recto-verso to recto-verso'
|
|
|
|
|
-- )
|
|
|
|
|
-- I can just open them but I wanna be able to see the type annotations.
|
|
|
|
|
verso-recto' : inverse' ∘ obverse' ≡ Function.id
|
|
|
|
|
verso-recto' = AreInverses.verso-recto (proj₂ (proj₂ univIso))
|
|
|
|
|
recto-verso' : obverse' ∘ inverse' ≡ Function.id
|
|
|
|
|
recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso))
|
|
|
|
|
verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso
|
|
|
|
|
verso-recto iso = begin
|
|
|
|
|
obverse (inverse iso) ≡⟨⟩
|
|
|
|
|
( addE ∘ _≃_.toIsomorphism
|
|
|
|
|
∘ obverse' ∘ dropP ∘ addP
|
|
|
|
|
∘ inverse' ∘ isoToEquiv
|
|
|
|
|
∘ dropE) iso
|
|
|
|
|
≡⟨⟩
|
|
|
|
|
( addE ∘ _≃_.toIsomorphism
|
|
|
|
|
∘ obverse'
|
|
|
|
|
∘ inverse' ∘ isoToEquiv
|
|
|
|
|
∘ dropE) iso
|
|
|
|
|
≡⟨ {!!} ⟩ -- obverse' inverse' are inverses
|
|
|
|
|
( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso
|
|
|
|
|
≡⟨ {!!} ⟩ -- should be easy to prove
|
|
|
|
|
-- _≃_.toIsomorphism ∘ isoToEquiv ≡ id
|
|
|
|
|
(addE ∘ dropE) iso
|
|
|
|
|
≡⟨⟩
|
|
|
|
|
iso ∎
|
|
|
|
|
|
|
|
|
|
-- Similar to above.
|
|
|
|
|
recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq
|
|
|
|
|
recto-verso eq = begin
|
|
|
|
|
inverse (obverse eq) ≡⟨ {!!} ⟩
|
|
|
|
|
eq ∎
|
|
|
|
|
|
|
|
|
|
-- Use the fact that being an h-level is a mere proposition.
|
|
|
|
|
-- This is almost provable using `Wishlist.isSetIsProp` - although
|
|
|
|
|
-- this creates homogenous paths.
|
|
|
|
|
isSetEq : (p : A ≡ B) → (λ i → isSet (p i)) [ isSetA ≡ isSetB ]
|
|
|
|
|
isSetEq = {!!}
|
|
|
|
|
|
|
|
|
|
res : hA ≡ hB
|
|
|
|
|
proj₁ (res i) = {!!}
|
|
|
|
|
proj₂ (res i) = isSetEq {!!} i
|
|
|
|
|
univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)
|
|
|
|
|
univalent = {!gradLemma obverse inverse verso-recto recto-verso!}
|
2018-02-21 12:37:07 +00:00
|
|
|
|
|
|
|
|
|
SetsIsCategory : IsCategory SetsRaw
|
2018-03-08 13:44:23 +00:00
|
|
|
|
IsCategory.isAssociative SetsIsCategory = refl
|
|
|
|
|
IsCategory.isIdentity SetsIsCategory {A} {B} = isIdentity {A} {B}
|
|
|
|
|
IsCategory.arrowsAreSets SetsIsCategory {A} {B} = arrowsAreSets {A} {B}
|
|
|
|
|
IsCategory.univalent SetsIsCategory = univalent
|
2018-02-21 12:37:07 +00:00
|
|
|
|
|
|
|
|
|
𝓢𝓮𝓽 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
|
2018-03-08 09:22:21 +00:00
|
|
|
|
|
|
|
|
|
rawProduct : RawProduct 𝓢 0A 0B
|
2018-03-08 09:45:15 +00:00
|
|
|
|
RawProduct.object rawProduct = 0A×0B
|
|
|
|
|
RawProduct.proj₁ rawProduct = Data.Product.proj₁
|
|
|
|
|
RawProduct.proj₂ rawProduct = Data.Product.proj₂
|
2018-03-08 09:22:21 +00:00
|
|
|
|
|
2018-03-08 09:28:05 +00:00
|
|
|
|
isProduct : IsProduct 𝓢 _ _ rawProduct
|
2018-03-14 09:23:23 +00:00
|
|
|
|
IsProduct.ump isProduct {X = X} f g
|
2018-03-08 09:20:29 +00:00
|
|
|
|
= (f &&& g) , lem {0X = X} f g
|
2018-02-21 12:37:07 +00:00
|
|
|
|
|
2018-03-08 09:22:21 +00:00
|
|
|
|
product : Product 𝓢 0A 0B
|
2018-03-08 09:20:29 +00:00
|
|
|
|
Product.raw product = rawProduct
|
|
|
|
|
Product.isProduct product = isProduct
|
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-03-05 10:17:31 +00:00
|
|
|
|
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|
|
|
|
-- Covariant Presheaf
|
|
|
|
|
Representable : Set (ℓa ⊔ lsuc ℓb)
|
|
|
|
|
Representable = Functor ℂ (𝓢𝓮𝓽 ℓb)
|
2018-02-21 12:37:07 +00:00
|
|
|
|
|
2018-03-05 10:17:31 +00:00
|
|
|
|
-- Contravariant Presheaf
|
|
|
|
|
Presheaf : Set (ℓa ⊔ lsuc ℓb)
|
|
|
|
|
Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
|
|
|
|
|
|
|
|
|
|
open Category ℂ
|
2018-01-17 11:16:07 +00:00
|
|
|
|
|
2018-02-21 12:37:07 +00:00
|
|
|
|
-- The "co-yoneda" embedding.
|
2018-03-05 10:17:31 +00:00
|
|
|
|
representable : Category.Object ℂ → Representable
|
|
|
|
|
representable A = record
|
2018-02-21 12:37:07 +00:00
|
|
|
|
{ raw = record
|
2018-03-08 10:03:56 +00:00
|
|
|
|
{ omap = λ B → ℂ [ A , B ] , arrowsAreSets
|
|
|
|
|
; fmap = ℂ [_∘_]
|
2018-02-21 12:37:07 +00:00
|
|
|
|
}
|
|
|
|
|
; 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
|
|
|
|
|
|
|
|
|
-- Alternate name: `yoneda`
|
2018-03-05 10:17:31 +00:00
|
|
|
|
presheaf : Category.Object (opposite ℂ) → Presheaf
|
|
|
|
|
presheaf B = record
|
2018-02-21 12:37:07 +00:00
|
|
|
|
{ raw = record
|
2018-03-08 10:03:56 +00:00
|
|
|
|
{ omap = λ A → ℂ [ A , B ] , arrowsAreSets
|
|
|
|
|
; fmap = λ 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
|
|
|
|
}
|