cat/src/Cat/Categories/Cat.agda

352 lines
14 KiB
Agda
Raw Normal View History

{-# 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
open import Cat.Functor
2018-01-21 14:03:00 +00:00
-- Tip from Andrea:
-- Use co-patterns - they help with showing more understandable types in goals.
lift-eq : {} {A B : Set } {a a' : A} {b b' : B} a a' b b' (a , b) (a' , b')
fst (lift-eq a b i) = a i
snd (lift-eq a b i) = b i
2018-01-21 14:03:00 +00:00
eqpair : {a b} {A : Set a} {B : Set b} {a a' : A} {b b' : B}
a a' b b' (a , b) (a' , b')
eqpair eqa eqb i = eqa i , eqb i
open Functor
open Category
2018-01-25 11:01:37 +00:00
module _ { ' : Level} {A B : Category '} where
lift-eq-functors : {f g : Functor A B}
2018-01-21 18:23:24 +00:00
(eq* : f .func* g .func*)
(eq→ : PathP (λ i {x y} A .Arrow x y B .Arrow (eq* i x) (eq* i y))
(f .func→) (g .func→))
-- → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g)
-- Use PathP
-- directly to show heterogeneous equalities by using previous
-- equalities (i.e. continuous paths) to create new continuous paths.
(eqI : PathP (λ i {c : A .Object} eq→ i (A .𝟙 {c}) B .𝟙 {eq* i c})
(ident f) (ident g))
(eqD : PathP (λ i { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
2018-01-21 18:23:24 +00:00
eq→ i (A ._⊕_ a' a) B ._⊕_ (eq→ i a') (eq→ i a))
(distrib f) (distrib g))
f g
lift-eq-functors eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }
-- The category of categories
2018-01-24 15:38:28 +00:00
module _ ( ' : Level) where
private
module _ {A B C D : Category '} {f : Functor A B} {g : Functor B C} {h : Functor C D} where
2018-01-21 18:23:24 +00:00
eq* : func* (h ∘f (g ∘f f)) func* ((h ∘f g) ∘f f)
eq* = refl
eq→ : PathP
(λ i {x y : A .Object} A .Arrow x y D .Arrow (eq* i x) (eq* i y))
(func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f))
eq→ = refl
id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D
id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D
postulate eqI : PathP
(λ i {c : A .Object} eq→ i (A .𝟙 {c}) D .𝟙 {eq* i c})
(ident ((h ∘f (g ∘f f))))
(ident ((h ∘f g) ∘f f))
postulate eqD : PathP (λ i { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''}
eq→ i (A ._⊕_ a' a) D ._⊕_ (eq→ i a') (eq→ i a))
(distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f))
-- eqD = {!!}
assc : h ∘f (g ∘f f) (h ∘f g) ∘f f
assc = lift-eq-functors eq* eq→ eqI eqD
module _ {A B : Category '} {f : Functor A B} where
lem : (func* f) (func* (identity {C = A})) func* f
lem = refl
-- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f
lemmm : PathP
(λ i
{x y : Object A} Arrow A x y Arrow B (func* f x) (func* f y))
(func→ (f ∘f identity)) (func→ f)
lemmm = refl
postulate lemz : PathP (λ i {c : A .Object} PathP (λ _ Arrow B (func* f c) (func* f c)) (func→ f (A .𝟙)) (B .𝟙))
(ident (f ∘f identity)) (ident f)
-- lemz = {!!}
postulate ident-r : f ∘f identity f
-- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!}
postulate ident-l : identity ∘f f f
-- ident-l = lift-eq-functors lem lemmm {!refl!} {!!}
2018-01-21 14:23:40 +00:00
Cat : Category (lsuc ( ')) ( ')
Cat =
record
{ Object = Category '
; Arrow = Functor
; 𝟙 = identity
; _⊕_ = _∘f_
-- What gives here? Why can I not name the variables directly?
2018-01-21 18:23:24 +00:00
; isCategory = record
{ assoc = λ {_ _ _ _ f g h} assc {f = f} {g = g} {h = h}
; ident = ident-r , ident-l
}
}
2018-01-24 15:38:28 +00:00
module _ { ' : Level} where
Catt = Cat '
module _ (C D : Category ') where
private
:Object: = C .Object × D .Object
:Arrow: : :Object: :Object: Set '
:Arrow: (c , d) (c' , d') = Arrow C c c' × Arrow D d d'
:𝟙: : {o : :Object:} :Arrow: o o
:𝟙: = C .𝟙 , D .𝟙
_:⊕:_ :
{a b c : :Object:}
:Arrow: b c
:Arrow: a b
:Arrow: a c
_:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) (C ._⊕_) bc∈C ab∈C , D ._⊕_ bc∈D ab∈D}
instance
:isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
:isCategory: = record
{ assoc = eqpair C.assoc D.assoc
; ident
= eqpair (fst C.ident) (fst D.ident)
, eqpair (snd C.ident) (snd D.ident)
}
where
open module C = IsCategory (C .isCategory)
open module D = IsCategory (D .isCategory)
:product: : Category '
:product: = record
{ Object = :Object:
; Arrow = :Arrow:
; 𝟙 = :𝟙:
; _⊕_ = _:⊕:_
}
2018-01-24 15:38:28 +00:00
proj₁ : Arrow Catt :product: C
proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl }
proj₂ : Arrow Catt :product: D
proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl }
module _ {X : Object Catt} (x₁ : Arrow Catt X C) (x₂ : Arrow Catt X D) where
open Functor
-- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D)
-- ident' {c = c} = lift-eq (ident x₁) (ident x₂)
x : Functor X :product:
x = record
{ func* = λ x (func* x₁) x , (func* x₂) x
; func→ = λ x func→ x₁ x , func→ x₂ x
; ident = lift-eq (ident x₁) (ident x₂)
; distrib = lift-eq (distrib x₁) (distrib x₂)
}
-- Need to "lift equality of functors"
-- If I want to do this like I do it for pairs it's gonna be a pain.
postulate isUniqL : (Catt proj₁) x x₁
-- isUniqL = lift-eq-functors refl refl {!!} {!!}
postulate isUniqR : (Catt proj₂) x x₂
-- isUniqR = lift-eq-functors refl refl {!!} {!!}
isUniq : (Catt proj₁) x x₁ × (Catt proj₂) x x₂
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] ((Catt proj₁) x x₁ × (Catt proj₂) x x₂)
uniq = x , isUniq
instance
isProduct : IsProduct Catt proj₁ proj₂
isProduct = uniq
product : Product { = Catt} C D
product = record
{ obj = :product:
; proj₁ = proj₁
; proj₂ = proj₂
}
2018-01-24 15:38:28 +00:00
module _ { ' : Level} where
open Category
instance
2018-01-25 11:01:37 +00:00
hasProducts : HasProducts (Cat ')
hasProducts = record { product = product }
2018-01-24 15:38:28 +00:00
-- Basically proves that `Cat ` is cartesian closed.
2018-01-25 11:01:37 +00:00
module _ ( : Level) where
2018-01-24 15:38:28 +00:00
private
2018-01-25 11:01:37 +00:00
open Data.Product
open Category
2018-01-24 15:38:28 +00:00
open import Cat.Categories.Fun
open Functor
2018-01-25 11:01:37 +00:00
Cat : Category (lsuc ( )) ( )
Cat = Cat
2018-01-24 15:38:28 +00:00
module _ ( 𝔻 : Category ) where
private
2018-01-25 11:01:37 +00:00
_𝔻⊕_ = 𝔻 ._⊕_
_⊕_ = ._⊕_
2018-01-24 15:38:28 +00:00
:obj: : Cat .Object
:obj: = Fun { = } {𝔻 = 𝔻}
2018-01-24 15:38:28 +00:00
:func*: : Functor 𝔻 × .Object 𝔻 .Object
:func*: (F , A) = F .func* A
2018-01-24 15:38:28 +00:00
module _ {dom cod : Functor 𝔻 × .Object} where
private
F : Functor 𝔻
F = proj₁ dom
A : .Object
A = proj₂ dom
2018-01-24 15:38:28 +00:00
G : Functor 𝔻
G = proj₁ cod
B : .Object
B = proj₂ cod
2018-01-24 15:38:28 +00:00
:func→: : (pobj : NaturalTransformation F G × .Arrow A B)
𝔻 .Arrow (F .func* A) (G .func* B)
:func→: ((θ , θNat) , f) = result
where
θA : 𝔻 .Arrow (F .func* A) (G .func* A)
θA = θ A
θB : 𝔻 .Arrow (F .func* B) (G .func* B)
θB = θ B
F→f : 𝔻 .Arrow (F .func* A) (F .func* B)
F→f = F .func→ f
G→f : 𝔻 .Arrow (G .func* A) (G .func* B)
G→f = G .func→ f
l : 𝔻 .Arrow (F .func* A) (G .func* B)
l = θB 𝔻⊕ F→f
r : 𝔻 .Arrow (F .func* A) (G .func* B)
r = G→f 𝔻⊕ θA
-- 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
-- lem = θNat f
result : 𝔻 .Arrow (F .func* A) (G .func* B)
result = l
2018-01-24 15:38:28 +00:00
_×p_ = product
2018-01-24 15:38:28 +00:00
module _ {c : Functor 𝔻 × .Object} where
private
F : Functor 𝔻
F = proj₁ c
C : .Object
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.
:ident: : :func→: {c} {c} (identityNat F , .𝟙 {o = proj₂ c}) 𝔻 .𝟙
:ident: = begin
:func→: {c} {c} ((:obj: ×p ) .Product.obj .𝟙 {c}) ≡⟨⟩
:func→: {c} {c} (identityNat F , .𝟙) ≡⟨⟩
(identityTrans F C 𝔻⊕ F .func→ ( .𝟙)) ≡⟨⟩
𝔻 .𝟙 𝔻⊕ F .func→ ( .𝟙) ≡⟨ proj₂ 𝔻.ident
F .func→ ( .𝟙) ≡⟨ F .ident
𝔻 .𝟙
where
open module 𝔻 = IsCategory (𝔻 .isCategory)
2018-01-24 15:38:28 +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⊕_ = (:obj: ×p ) .Product.obj ._⊕_ {F×A} {G×B} {H×C}
module _
-- NaturalTransformation F G × .Arrow A B
2018-01-25 11:01:37 +00:00
{θ×f : NaturalTransformation F G × .Arrow A B}
{η×g : NaturalTransformation G H × .Arrow B C} where
private
θ : Transformation F G
θ = proj₁ (proj₁ θ×f)
θNat : Natural F G θ
θNat = proj₂ (proj₁ θ×f)
f : .Arrow A B
f = proj₂ θ×f
η : Transformation G H
η = proj₁ (proj₁ η×g)
ηNat : Natural G H η
ηNat = proj₂ (proj₁ η×g)
g : .Arrow B C
g = proj₂ η×g
ηθNT : NaturalTransformation F H
ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
ηθ = proj₁ ηθNT
ηθNat = proj₂ ηθNT
2018-01-24 15:38:28 +00:00
:distrib: :
2018-01-25 11:01:37 +00:00
(η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f)
(η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
2018-01-24 15:38:28 +00:00
:distrib: = begin
2018-01-25 11:01:37 +00:00
(ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f) ≡⟨ ηθNat (g ℂ⊕ f)
H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A) ≡⟨ cong (λ φ φ 𝔻⊕ ηθ A) (H .distrib)
(H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A) ≡⟨ sym assoc
H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A)) ≡⟨⟩
H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A)) ≡⟨ cong (λ φ H .func→ g 𝔻⊕ φ) assoc
H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A) ≡⟨ cong (λ φ H .func→ g 𝔻⊕ φ) (cong (λ φ φ 𝔻⊕ θ A) (sym (ηNat f)))
H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A) ≡⟨ cong (λ φ H .func→ g 𝔻⊕ φ) (sym assoc)
H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ assoc
(H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g))
(η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A) ≡⟨ cong (λ φ (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f))
(η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
2018-01-24 15:38:28 +00:00
where
2018-01-25 11:01:37 +00:00
open IsCategory (𝔻 .isCategory)
2018-01-24 15:38:28 +00:00
:eval: : Functor ((:obj: ×p ) .Product.obj) 𝔻
:eval: = record
{ func* = :func*:
; func→ = λ {dom} {cod} :func→: {dom} {cod}
; ident = λ {o} :ident: {o}
; distrib = λ {f u n k y} :distrib: {f} {u} {n} {k} {y}
}
module _ (𝔸 : Category ) (F : Functor ((𝔸 ×p ) .Product.obj) 𝔻) where
2018-01-25 11:01:37 +00:00
open HasProducts (hasProducts {} {}) using (parallelProduct)
2018-01-24 15:38:28 +00:00
postulate
transpose : Functor 𝔸 :obj:
eq : Cat ._⊕_ :eval: (parallelProduct transpose (Cat .𝟙 {o = })) F
catTranspose : ∃![ F~ ] (Cat ._⊕_ :eval: (parallelProduct F~ (Cat .𝟙 {o = })) F)
catTranspose = transpose , eq
-- :isExponential: : IsExponential Cat A B :obj: {!:eval:!}
:isExponential: : IsExponential Cat 𝔻 :obj: :eval:
:isExponential: = catTranspose
-- :exponent: : Exponential (Cat ) A B
:exponent: : Exponential Cat 𝔻
:exponent: = record
{ obj = :obj:
; eval = :eval:
; isExponential = :isExponential:
}
2018-01-25 11:01:37 +00:00
hasExponentials : HasExponentials (Cat )
hasExponentials = record { exponent = :exponent: }