cat/src/Cat/Categories/Cat.agda

419 lines
17 KiB
Agda
Raw Normal View History

2018-02-02 14:33:54 +00:00
-- There is no category of categories in our interpretation
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module Cat.Categories.Cat where
open import Agda.Primitive
open import Cubical
open import Function
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Cat.Category
2018-02-05 15:35:33 +00:00
open import Cat.Category.Functor
open import Cat.Category.Product
open import Cat.Category.Exponential
2018-01-31 13:39:54 +00:00
open import Cat.Equality
open Equality.Data.Product
open Functor
2018-01-30 15:23:36 +00:00
open IsFunctor
2018-02-22 14:31:54 +00:00
open Category using (Object ; 𝟙)
2018-01-25 11:01:37 +00:00
-- The category of categories
2018-01-24 15:38:28 +00:00
module _ ( ' : Level) where
private
2018-01-31 13:39:54 +00:00
module _ {𝔸 𝔹 𝔻 : Category '} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 } {H : Functor 𝔻} where
2018-01-25 11:44:47 +00:00
private
2018-01-31 13:39:54 +00:00
eq* : func* (H ∘f (G ∘f F)) func* ((H ∘f G) ∘f F)
2018-01-25 11:44:47 +00:00
eq* = refl
eq→ : PathP
2018-02-05 15:35:33 +00:00
(λ i {A B : Object 𝔸} 𝔸 [ A , B ] 𝔻 [ eq* i A , eq* i B ])
2018-01-31 13:39:54 +00:00
(func→ (H ∘f (G ∘f F))) (func→ ((H ∘f G) ∘f F))
2018-01-25 11:44:47 +00:00
eq→ = refl
2018-01-31 13:39:54 +00:00
postulate
eqI
2018-02-05 15:35:33 +00:00
: (λ i {A : Object 𝔸} eq→ i (𝟙 𝔸 {A}) 𝟙 𝔻 {eq* i A})
2018-01-31 13:39:54 +00:00
[ (H ∘f (G ∘f F)) .isFunctor .ident
((H ∘f G) ∘f F) .isFunctor .ident
]
eqD
: (λ i {A B C} {f : 𝔸 [ A , B ]} {g : 𝔸 [ B , C ]}
eq→ i (𝔸 [ g f ]) 𝔻 [ eq→ i g eq→ i f ])
[ (H ∘f (G ∘f F)) .isFunctor .distrib
((H ∘f G) ∘f F) .isFunctor .distrib
]
assc : H ∘f (G ∘f F) (H ∘f G) ∘f F
2018-02-22 14:31:54 +00:00
assc = Functor≡ eq* eq→
2018-01-25 11:44:47 +00:00
module _ { 𝔻 : Category '} {F : Functor 𝔻} where
module _ where
private
eq* : (func* F) (func* (identity {C = })) func* F
eq* = refl
-- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
eq→ : PathP
(λ i
2018-02-22 14:31:54 +00:00
{x y : Object } [ x , y ] 𝔻 [ func* F x , func* F y ])
2018-01-25 11:44:47 +00:00
(func→ (F ∘f identity)) (func→ F)
eq→ = refl
postulate
eqI-r
2018-02-05 15:35:33 +00:00
: (λ i {c : Object } (λ _ 𝔻 [ func* F c , func* F c ])
[ func→ F (𝟙 ) 𝟙 𝔻 ])
[(F ∘f identity) .isFunctor .ident F .isFunctor .ident ]
2018-01-25 11:44:47 +00:00
eqD-r : PathP
(λ i
2018-02-05 15:35:33 +00:00
{A B C : Object } {f : [ A , B ]} {g : [ B , C ]}
eq→ i ( [ g f ]) 𝔻 [ eq→ i g eq→ i f ])
2018-01-30 15:23:36 +00:00
((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
2018-01-25 11:44:47 +00:00
ident-r : F ∘f identity F
2018-02-22 14:31:54 +00:00
ident-r = Functor≡ eq* eq→
2018-01-25 11:44:47 +00:00
module _ where
private
postulate
2018-02-22 14:31:54 +00:00
eq* : func* (identity ∘f F) func* F
2018-01-25 11:44:47 +00:00
eq→ : PathP
2018-02-05 15:35:33 +00:00
(λ i {x y : Object } [ x , y ] 𝔻 [ eq* i x , eq* i y ])
2018-02-22 14:31:54 +00:00
(func→ (identity ∘f F)) (func→ F)
2018-02-05 15:35:33 +00:00
eqI : (λ i {A : Object } eq→ i (𝟙 {A}) 𝟙 𝔻 {eq* i A})
[ ((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident) ]
2018-02-05 15:35:33 +00:00
eqD : PathP (λ i {A B C : Object } {f : [ A , B ]} {g : [ B , C ]}
eq→ i ( [ g f ]) 𝔻 [ eq→ i g eq→ i f ])
2018-01-30 15:23:36 +00:00
((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
-- (λ z → eq* i z) (eq→ i)
2018-01-25 11:44:47 +00:00
ident-l : identity ∘f F F
2018-02-22 14:31:54 +00:00
ident-l = Functor≡ eq* eq→
RawCat : RawCategory (lsuc ( ')) ( ')
RawCat =
record
{ Object = Category '
; Arrow = Functor
; 𝟙 = identity
; _∘_ = _∘f_
-- What gives here? Why can I not name the variables directly?
-- ; isCategory = record
-- { assoc = λ {_ _ _ _ F G H} → assc {F = F} {G = G} {H = H}
-- ; ident = ident-r , ident-l
-- }
}
private
open RawCategory
assoc : IsAssociative RawCat
assoc {f = F} {G} {H} = assc {F = F} {G = G} {H = H}
-- TODO: Rename `ident'` to `ident` after changing how names are exposed in Functor.
ident' : IsIdentity RawCat identity
ident' = ident-r , ident-l
-- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors,
-- however, form a groupoid! Therefore there is no (1-)category of
-- categories. There does, however, exist a 2-category of 1-categories.
-- Because of the note above there is not category of categories.
Cat : (unprovable : IsCategory RawCat) Category (lsuc ( ')) ( ')
Category.raw (Cat _) = RawCat
Category.isCategory (Cat unprovable) = unprovable
-- Category.raw Cat _ = RawCat
-- Category.isCategory Cat unprovable = unprovable
-- The following to some extend depends on the category of categories being a
-- category. In some places it may not actually be needed, however.
module _ { ' : Level} (unprovable : IsCategory (RawCat ')) where
2018-01-25 11:44:47 +00:00
module _ ( 𝔻 : Category ') where
2018-01-24 15:38:28 +00:00
private
Catt = Cat ' unprovable
2018-02-05 15:35:33 +00:00
:Object: = Object × Object 𝔻
2018-01-24 15:38:28 +00:00
:Arrow: : :Object: :Object: Set '
2018-02-22 14:31:54 +00:00
:Arrow: (c , d) (c' , d') = [ c , c' ] × 𝔻 [ d , d' ]
2018-01-24 15:38:28 +00:00
:𝟙: : {o : :Object:} :Arrow: o o
2018-02-05 15:35:33 +00:00
:𝟙: = 𝟙 , 𝟙 𝔻
2018-01-24 15:38:28 +00:00
_:⊕:_ :
{a b c : :Object:}
:Arrow: b c
:Arrow: a b
:Arrow: a c
_:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) [ bc∈C ab∈C ] , 𝔻 [ bc∈D ab∈D ]}
2018-01-24 15:38:28 +00:00
2018-02-05 15:35:33 +00:00
:rawProduct: : RawCategory '
RawCategory.Object :rawProduct: = :Object:
RawCategory.Arrow :rawProduct: = :Arrow:
RawCategory.𝟙 :rawProduct: = :𝟙:
RawCategory._∘_ :rawProduct: = _:⊕:_
open RawCategory :rawProduct:
2018-02-05 15:35:33 +00:00
2018-02-22 14:31:54 +00:00
module C = Category
module D = Category 𝔻
2018-02-05 15:35:33 +00:00
postulate
issSet : {A B : RawCategory.Object :rawProduct:} isSet (Arrow A B)
ident' : IsIdentity :𝟙:
ident'
= Σ≡ (fst C.ident) (fst D.ident)
, Σ≡ (snd C.ident) (snd D.ident)
postulate univalent : Univalence.Univalent :rawProduct: ident'
2018-01-24 15:38:28 +00:00
instance
2018-02-05 15:35:33 +00:00
:isCategory: : IsCategory :rawProduct:
IsCategory.assoc :isCategory: = Σ≡ C.assoc D.assoc
IsCategory.ident :isCategory: = ident'
2018-02-22 14:31:54 +00:00
IsCategory.arrowIsSet :isCategory: = issSet
IsCategory.univalent :isCategory: = univalent
2018-01-24 15:38:28 +00:00
:product: : Category '
2018-02-22 14:31:54 +00:00
Category.raw :product: = :rawProduct:
2018-01-24 15:38:28 +00:00
2018-01-31 13:39:54 +00:00
proj₁ : Catt [ :product: , ]
2018-02-22 14:31:54 +00:00
proj₁ = record
{ raw = record { func* = fst ; func→ = fst }
; isFunctor = record { ident = refl ; distrib = refl }
}
2018-01-24 15:38:28 +00:00
2018-01-31 13:39:54 +00:00
proj₂ : Catt [ :product: , 𝔻 ]
2018-02-22 14:31:54 +00:00
proj₂ = record
{ raw = record { func* = snd ; func→ = snd }
; isFunctor = record { ident = refl ; distrib = refl }
}
2018-01-24 15:38:28 +00:00
2018-01-31 13:39:54 +00:00
module _ {X : Object Catt} (x₁ : Catt [ X , ]) (x₂ : Catt [ X , 𝔻 ]) where
2018-01-24 15:38:28 +00:00
open Functor
2018-02-05 15:35:33 +00:00
postulate x : Functor X :product:
-- x = record
-- { func* = λ x → x₁ .func* x , x₂ .func* x
-- ; func→ = λ x → func→ x₁ x , func→ x₂ x
-- ; isFunctor = record
-- { ident = Σ≡ x₁.ident x₂.ident
-- ; distrib = Σ≡ x₁.distrib x₂.distrib
-- }
-- }
-- where
-- open module x₁ = IsFunctor (x₁ .isFunctor)
-- open module x₂ = IsFunctor (x₂ .isFunctor)
-- Turned into postulate after:
-- > commit e8215b2c051062c6301abc9b3f6ec67106259758 (HEAD -> dev, github/dev)
-- > Author: Frederik Hanghøj Iversen <fhi.1990@gmail.com>
-- > Date: Mon Feb 5 14:59:53 2018 +0100
postulate isUniqL : Catt [ proj₁ x ] x₁
-- isUniqL = Functor≡ eq* eq→ {!!}
-- where
-- eq* : (Catt [ proj₁ ∘ x ]) .func* ≡ x₁ .func*
-- eq* = {!refl!}
-- eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → [ eq* i A , eq* i B ])
-- [ (Catt [ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
-- eq→ = refl
-- postulate eqIsF : (Catt [ proj₁ ∘ x ]) .isFunctor ≡ x₁ .isFunctor
2018-01-31 13:39:54 +00:00
-- eqIsF = IsFunctor≡ {!refl!} {!!}
2018-01-24 15:38:28 +00:00
postulate isUniqR : Catt [ proj₂ x ] x₂
2018-01-25 11:44:47 +00:00
-- isUniqR = Functor≡ refl refl {!!} {!!}
2018-01-24 15:38:28 +00:00
isUniq : Catt [ proj₁ x ] x₁ × Catt [ proj₂ x ] x₂
2018-01-24 15:38:28 +00:00
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] (Catt [ proj₁ x ] x₁ × Catt [ proj₂ x ] x₂)
2018-01-24 15:38:28 +00:00
uniq = x , isUniq
2018-01-25 11:44:47 +00:00
instance
isProduct : IsProduct Catt proj₁ proj₂
2018-01-25 11:44:47 +00:00
isProduct = uniq
2018-01-24 15:38:28 +00:00
product : Product { = Catt} 𝔻
2018-01-24 15:38:28 +00:00
product = record
{ obj = :product:
; proj₁ = proj₁
; proj₂ = proj₂
}
module _ { ' : Level} (unprovable : IsCategory (RawCat ')) where
Catt = Cat ' unprovable
2018-01-24 15:38:28 +00:00
instance
hasProducts : HasProducts Catt
hasProducts = record { product = product unprovable }
2018-01-24 15:38:28 +00:00
-- Basically proves that `Cat ` is cartesian closed.
module _ ( : Level) (unprovable : IsCategory (RawCat )) where
2018-01-24 15:38:28 +00:00
private
2018-01-25 11:01:37 +00:00
open Data.Product
2018-01-24 15:38:28 +00:00
open import Cat.Categories.Fun
2018-01-25 11:01:37 +00:00
Cat : Category (lsuc ( )) ( )
Cat = Cat unprovable
2018-01-24 15:38:28 +00:00
module _ ( 𝔻 : Category ) where
private
:obj: : Object Cat
2018-01-24 15:38:28 +00:00
:obj: = Fun { = } {𝔻 = 𝔻}
2018-02-05 15:35:33 +00:00
:func*: : Functor 𝔻 × Object Object 𝔻
2018-02-22 14:31:54 +00:00
:func*: (F , A) = func* F A
2018-02-05 15:35:33 +00:00
module _ {dom cod : Functor 𝔻 × Object } where
2018-01-24 15:38:28 +00:00
private
F : Functor 𝔻
F = proj₁ dom
2018-02-05 15:35:33 +00:00
A : Object
2018-01-24 15:38:28 +00:00
A = proj₂ dom
2018-01-24 15:38:28 +00:00
G : Functor 𝔻
G = proj₁ cod
2018-02-05 15:35:33 +00:00
B : Object
2018-01-24 15:38:28 +00:00
B = proj₂ cod
2018-02-05 15:35:33 +00:00
:func→: : (pobj : NaturalTransformation F G × [ A , B ])
2018-02-22 14:31:54 +00:00
𝔻 [ func* F A , func* G B ]
2018-01-24 15:38:28 +00:00
:func→: ((θ , θNat) , f) = result
where
2018-02-22 14:31:54 +00:00
θA : 𝔻 [ func* F A , func* G A ]
2018-01-24 15:38:28 +00:00
θA = θ A
2018-02-22 14:31:54 +00:00
θB : 𝔻 [ func* F B , func* G B ]
2018-01-24 15:38:28 +00:00
θB = θ B
2018-02-22 14:31:54 +00:00
F→f : 𝔻 [ func* F A , func* F B ]
F→f = func→ F f
G→f : 𝔻 [ func* G A , func* G B ]
G→f = func→ G f
l : 𝔻 [ func* F A , func* G B ]
l = 𝔻 [ θB F→f ]
2018-02-22 14:31:54 +00:00
r : 𝔻 [ func* F A , func* G B ]
r = 𝔻 [ G→f θA ]
2018-01-24 15:38:28 +00:00
-- There are two choices at this point,
-- but I suppose the whole point is that
-- by `θNat f` we have `l ≡ r`
-- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
2018-01-24 15:38:28 +00:00
-- lem = θNat f
2018-02-22 14:31:54 +00:00
result : 𝔻 [ func* F A , func* G B ]
2018-01-24 15:38:28 +00:00
result = l
_×p_ = product unprovable
2018-02-05 15:35:33 +00:00
module _ {c : Functor 𝔻 × Object } where
2018-01-24 15:38:28 +00:00
private
F : Functor 𝔻
F = proj₁ c
2018-02-05 15:35:33 +00:00
C : Object
2018-01-24 15:38:28 +00:00
C = proj₂ c
2018-01-24 15:38:28 +00:00
-- NaturalTransformation F G × .Arrow A B
2018-01-25 11:01:37 +00:00
-- :ident: : :func→: {c} {c} (identityNat F , .𝟙) 𝔻 .𝟙
-- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
2018-01-24 15:38:28 +00:00
-- where
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
2018-01-25 11:01:37 +00:00
-- Unfortunately the equational version has some ambigous arguments.
2018-02-22 14:31:54 +00:00
:ident: : :func→: {c} {c} (identityNat F , 𝟙 {A = proj₂ c}) 𝟙 𝔻
2018-01-25 11:01:37 +00:00
:ident: = begin
2018-02-05 15:35:33 +00:00
:func→: {c} {c} (𝟙 (Product.obj (:obj: ×p )) {c}) ≡⟨⟩
:func→: {c} {c} (identityNat F , 𝟙 ) ≡⟨⟩
2018-02-22 14:31:54 +00:00
𝔻 [ identityTrans F C func→ F (𝟙 )] ≡⟨⟩
𝔻 [ 𝟙 𝔻 func→ F (𝟙 )] ≡⟨ proj₂ 𝔻.ident
func→ F (𝟙 ) ≡⟨ F.ident
2018-02-05 15:35:33 +00:00
𝟙 𝔻
2018-01-25 11:01:37 +00:00
where
2018-02-22 14:31:54 +00:00
open module 𝔻 = Category 𝔻
2018-01-30 15:23:36 +00:00
open module F = IsFunctor (F .isFunctor)
2018-02-23 09:44:23 +00:00
module _ {F×A G×B H×C : Functor 𝔻 × Object } where
F = F×A .proj₁
A = F×A .proj₂
G = G×B .proj₁
B = G×B .proj₂
H = H×C .proj₁
C = H×C .proj₂
-- Not entirely clear what this is at this point:
_P⊕_ = Category._∘_ (Product.obj (:obj: ×p )) {F×A} {G×B} {H×C}
module _
-- NaturalTransformation F G × .Arrow A B
{θ×f : NaturalTransformation F G × [ A , B ]}
{η×g : NaturalTransformation G H × [ B , C ]} where
private
θ : Transformation F G
θ = proj₁ (proj₁ θ×f)
θNat : Natural F G θ
θNat = proj₂ (proj₁ θ×f)
f : [ A , B ]
f = proj₂ θ×f
η : Transformation G H
η = proj₁ (proj₁ η×g)
ηNat : Natural G H η
ηNat = proj₂ (proj₁ η×g)
g : [ B , C ]
g = proj₂ η×g
ηθNT : NaturalTransformation F H
ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat)
ηθ = proj₁ ηθNT
ηθNat = proj₂ ηθNT
:distrib: :
𝔻 [ 𝔻 [ η C θ C ] func→ F ( [ g f ] ) ]
𝔻 [ 𝔻 [ η C func→ G g ] 𝔻 [ θ B func→ F f ] ]
:distrib: = begin
𝔻 [ (ηθ C) func→ F ( [ g f ]) ]
≡⟨ ηθNat ( [ g f ])
𝔻 [ func→ H ( [ g f ]) (ηθ A) ]
≡⟨ cong (λ φ 𝔻 [ φ ηθ A ]) (H.distrib)
𝔻 [ 𝔻 [ func→ H g func→ H f ] (ηθ A) ]
≡⟨ sym assoc
𝔻 [ func→ H g 𝔻 [ func→ H f ηθ A ] ]
≡⟨ cong (λ φ 𝔻 [ func→ H g φ ]) assoc
𝔻 [ func→ H g 𝔻 [ 𝔻 [ func→ H f η A ] θ A ] ]
≡⟨ cong (λ φ 𝔻 [ func→ H g φ ]) (cong (λ φ 𝔻 [ φ θ A ]) (sym (ηNat f)))
𝔻 [ func→ H g 𝔻 [ 𝔻 [ η B func→ G f ] θ A ] ]
≡⟨ cong (λ φ 𝔻 [ func→ H g φ ]) (sym assoc)
𝔻 [ func→ H g 𝔻 [ η B 𝔻 [ func→ G f θ A ] ] ]
≡⟨ assoc
𝔻 [ 𝔻 [ func→ H g η B ] 𝔻 [ func→ G f θ A ] ]
≡⟨ cong (λ φ 𝔻 [ φ 𝔻 [ func→ G f θ A ] ]) (sym (ηNat g))
𝔻 [ 𝔻 [ η C func→ G g ] 𝔻 [ func→ G f θ A ] ]
≡⟨ cong (λ φ 𝔻 [ 𝔻 [ η C func→ G g ] φ ]) (sym (θNat f))
𝔻 [ 𝔻 [ η C func→ G g ] 𝔻 [ θ B func→ F f ] ]
where
open Category 𝔻
module H = IsFunctor (H .isFunctor)
:eval: : Functor ((:obj: ×p ) .Product.obj) 𝔻
:eval: = record
{ raw = record
{ func* = :func*:
; func→ = λ {dom} {cod} :func→: {dom} {cod}
}
; isFunctor = record
{ ident = λ {o} :ident: {o}
; distrib = λ {f u n k y} :distrib: {f} {u} {n} {k} {y}
}
}
module _ (𝔸 : Category ) (F : Functor ((𝔸 ×p ) .Product.obj) 𝔻) where
open HasProducts (hasProducts {} {} unprovable) renaming (_|×|_ to parallelProduct)
postulate
transpose : Functor 𝔸 :obj:
eq : Cat [ :eval: (parallelProduct transpose (𝟙 Cat {A = })) ] F
-- eq : Cat [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Cat {o = })) ] ≡ F
-- eq' : (Cat [ :eval: ∘
-- (record { product = product } HasProducts.|×| transpose)
-- (𝟙 Cat)
-- ])
-- ≡ F
-- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758`
-- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Cat [
-- :eval: (parallelProduct F~ (𝟙 Cat {o = }))] F) catTranspose =
-- transpose , eq
postulate :isExponential: : IsExponential Cat 𝔻 :obj: :eval:
-- :isExponential: : IsExponential Cat 𝔻 :obj: :eval:
-- :isExponential: = {!catTranspose!}
-- where
-- open HasProducts (hasProducts {} {} unprovable) using (_|×|_)
-- :isExponential: = λ 𝔸 F transpose 𝔸 F , eq' 𝔸 F
-- :exponent: : Exponential (Cat ) A B
:exponent: : Exponential Cat 𝔻
:exponent: = record
{ obj = :obj:
; eval = :eval:
; isExponential = :isExponential:
}
hasExponentials : HasExponentials Cat
hasExponentials = record { exponent = :exponent: }