fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Use alternative syntax for arrow composition

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-01-30 19:19:16 +01:00
parent e33911ad9e
commit 255b0236f9
9 changed files with 124 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

77
src/Cat/Categories/Cat.agda
View file

@ -22,7 +22,7 @@ eqpair eqa eqb i = eqa i , eqb i
open Functor
open IsFunctor
open Category
open Category hiding (_∘_)
-- The category of categories
module _ (ℓ ℓ' : Level) where
@ -40,7 +40,7 @@ module _ (ℓ ℓ' : Level) where
((h ∘f (g ∘f f)) .isFunctor .ident)
(((h ∘f g) ∘f f) .isFunctor .ident)
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))
→ eq→ i (A [ a' ∘ a ]) ≡ D [ eq→ i a' ∘ eq→ i a ])
((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
@ -64,7 +64,7 @@ module _ (ℓ ℓ' : Level) where
eqD-r : PathP
(λ i →
{A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} →
eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
((F ∘f identity) .isFunctor .distrib) (F .isFunctor .distrib)
ident-r : F ∘f identity ≡ F
ident-r = Functor≡ eq* eq→ eqI-r eqD-r
@ -78,7 +78,7 @@ module _ (ℓ ℓ' : Level) where
eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A})
((identity ∘f F) .isFunctor .ident) (F .isFunctor .ident)
eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C}
→ eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f))
→ eq→ i (ℂ [ g ∘ f ]) ≡ 𝔻 [ eq→ i g ∘ eq→ i f ])
((identity ∘f F) .isFunctor .distrib) (F .isFunctor .distrib)
ident-l : identity ∘f F ≡ F
ident-l = Functor≡ eq* eq→ eqI eqD
@ -89,7 +89,7 @@ module _ (ℓ ℓ' : Level) where
{ Object = Category ℓ ℓ'
; Arrow = Functor
; 𝟙 = identity
; _⊕_ = _∘f_
; _∘_ = _∘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}
@ -112,7 +112,7 @@ module _ {ℓ ℓ' : Level} where
: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}
_:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]}
instance
:isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_
@ -131,7 +131,7 @@ module _ {ℓ ℓ' : Level} where
{ Object = :Object:
; Arrow = :Arrow:
; 𝟙 = :𝟙:
; _⊕_ = _:⊕:_
; _∘_ = _:⊕:_
}
proj₁ : Arrow Catt :product: ℂ
@ -161,16 +161,16 @@ module _ {ℓ ℓ' : Level} where
-- 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₁
postulate isUniqL : Catt [ proj₁ ∘ x ] ≡ x₁
-- isUniqL = Functor≡ refl refl {!!} {!!}
postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂
postulate isUniqR : Catt [ proj₂ ∘ x ] ≡ x₂
-- isUniqR = Functor≡ refl refl {!!} {!!}
isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂
isUniq : Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂
isUniq = isUniqL , isUniqR
uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂)
uniq : ∃![ x ] (Catt [ proj₁ ∘ x ] ≡ x₁ × Catt [ proj₂ ∘ x ] ≡ x₂)
uniq = x , isUniq
instance
@ -199,9 +199,6 @@ module _ (ℓ : Level) where
Catℓ = Cat ℓ ℓ
module _ (ℂ 𝔻 : Category ℓ ℓ) where
private
_𝔻⊕_ = 𝔻 ._⊕_
_ℂ⊕_ = ℂ ._⊕_
:obj: : Cat ℓ ℓ .Object
:obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻}
@ -233,13 +230,13 @@ module _ (ℓ : Level) where
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
l = 𝔻 [ θB ∘ F→f ]
r : 𝔻 .Arrow (F .func* A) (G .func* B)
r = G→f 𝔻⊕ θA
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 : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
-- lem = θNat f
result : 𝔻 .Arrow (F .func* A) (G .func* B)
result = l
@ -257,15 +254,14 @@ module _ (ℓ : Level) where
-- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
-- :ident: = trans (proj₂ 𝔻.ident) (F .ident)
-- where
-- _𝔻⊕_ = 𝔻 ._⊕_
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
-- 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 ⟩
𝔻 [ identityTrans F C ∘ F .func→ (ℂ .𝟙)] ≡⟨⟩
𝔻 [ 𝔻 .𝟙 ∘ F .func→ (ℂ .𝟙)] ≡⟨ proj₂ 𝔻.ident ⟩
F .func→ (ℂ .𝟙) ≡⟨ F.ident ⟩
𝔻 .𝟙 ∎
where
@ -280,7 +276,7 @@ module _ (ℓ : Level) where
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}
_P⊕_ = (:obj: ×p ℂ) .Product.obj .Category._∘_ {F×A} {G×B} {H×C}
module _
-- NaturalTransformation F G × ℂ .Arrow A B
{θ×f : NaturalTransformation F G × ℂ .Arrow A B}
@ -300,26 +296,33 @@ module _ (ℓ : Level) where
g = proj₂ η×g
ηθNT : NaturalTransformation F H
ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat)
ηθNT = Fun .Category._∘_ {F} {G} {H} (η , ηNat) (θ , θNat)
ηθ = proj₁ ηθNT
ηθNat = proj₂ ηθNT
:distrib: :
(η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f)
≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F .func→ ( ℂ [ g ∘ f ] ) ]
≡ 𝔻 [ 𝔻 [ η C ∘ G .func→ g ] ∘ 𝔻 [ θ B ∘ F .func→ f ] ]
:distrib: = begin
(ηθ 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) ∎
𝔻 [ (ηθ 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 ] ]
≡⟨ 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 ] ] ∎
where
open IsCategory (𝔻 .isCategory)
open module H = IsFunctor (H .isFunctor)
@ -339,9 +342,9 @@ module _ (ℓ : Level) where
postulate
transpose : Functor 𝔸 :obj:
eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F
eq : Catℓ [ :eval: ∘ (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ] ≡ F
catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F)
catTranspose : ∃![ F~ ] (Catℓ [ :eval: ∘ (parallelProduct F~ (Catℓ .𝟙 {o = ℂ}))] ≡ F )
catTranspose = transpose , eq
:isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval:

51
src/Cat/Categories/Fun.agda
View file

@ -10,19 +10,19 @@ open import Cat.Category
open import Cat.Functor
module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where
open Category
open Category hiding ( _∘_ ; Arrow )
open Functor
module _ (F G : Functor ℂ 𝔻) where
-- What do you call a non-natural tranformation?
Transformation : Set (ℓc ⊔ ℓd')
Transformation = (C : ℂ .Object) → 𝔻 .Arrow (F .func* C) (G .func* C)
Transformation = (C : ℂ .Object) → 𝔻 [ F .func* C , G .func* C ]
Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
Natural θ
= {A B : ℂ .Object}
→ (f : ℂ .Arrow A B)
→ 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
NaturalTransformation = Σ Transformation Natural
@ -30,18 +30,28 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
-- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
-- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A)
module _ {F G : Functor ℂ 𝔻} where
NaturalTransformation≡ : {α β : NaturalTransformation F G}
→ (eq₁ : α .proj₁ ≡ β .proj₁)
→ (eq₂ : PathP
(λ i → {A B : ℂ .Object} (f : ℂ [ A , B ])
→ 𝔻 [ eq₁ i B ∘ F .func→ f ]
≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
(α .proj₂) (β .proj₂))
→ α ≡ β
NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝔻 .𝟙
identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F)
identityNatural F {A = A} {B = B} f = begin
identityTrans F B 𝔻⊕ F→ f ≡⟨⟩
𝔻 .𝟙 𝔻⊕ F→ f ≡⟨ proj₂ 𝔻.ident ⟩
𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩
𝔻 [ 𝔻 .𝟙 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩
F→ f 𝔻⊕ 𝔻 .𝟙 ≡⟨⟩
F→ f 𝔻⊕ identityTrans F A ∎
𝔻 [ F→ f ∘ 𝔻 .𝟙 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
_𝔻⊕_ = 𝔻 ._⊕_
F→ = F .func→
open module 𝔻 = IsCategory (𝔻 .isCategory)
@ -50,21 +60,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
module _ {F G H : Functor ℂ 𝔻} where
private
_𝔻⊕_ = 𝔻 ._⊕_
_∘nt_ : Transformation G H → Transformation F G → Transformation F H
(θ ∘nt η) C = θ C 𝔻⊕ η C
(θ ∘nt η) C = 𝔻 [ θ C ∘ η C ]
NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η
proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin
((θ ∘nt η) B) 𝔻⊕ (F .func→ f) ≡⟨⟩
(θ B 𝔻⊕ η B) 𝔻⊕ (F .func→ f) ≡⟨ sym assoc ⟩
θ B 𝔻⊕ (η B 𝔻⊕ (F .func→ f)) ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩
θ B 𝔻⊕ ((G .func→ f) 𝔻⊕ η A) ≡⟨ assoc ⟩
(θ B 𝔻⊕ (G .func→ f)) 𝔻⊕ η A ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩
(((H .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A) ≡⟨ sym assoc ⟩
((H .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A)) ≡⟨⟩
((H .func→ f) 𝔻⊕ ((θ ∘nt η) A)) ∎
𝔻 [ (θ ∘nt η) B ∘ F .func→ f ] ≡⟨⟩
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F .func→ f ] ≡⟨ sym assoc ⟩
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F .func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
𝔻 [ θ B ∘ 𝔻 [ G .func→ f ∘ η A ] ] ≡⟨ assoc ⟩
𝔻 [ 𝔻 [ θ B ∘ G .func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
𝔻 [ 𝔻 [ H .func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym assoc ⟩
𝔻 [ H .func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
𝔻 [ H .func→ f ∘ (θ ∘nt η) A ] ∎
where
open IsCategory (𝔻 .isCategory)
NatComp = _:⊕:_
@ -100,7 +109,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
{ Object = Functor ℂ 𝔻
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identityNat F
; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H}
; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H}
}
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
@ -112,5 +121,5 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
{ Object = Presheaf ℂ
; Arrow = NaturalTransformation
; 𝟙 = λ {F} → identityNat F
; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H}
}

2
src/Cat/Categories/Rel.agda
View file

@ -159,6 +159,6 @@ Rel = record
{ Object = Set
; Arrow = λ S R → Subset (S × R)
; 𝟙 = λ {S} → Diag S
; _⊕_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
; _∘_ = λ {A B C} S R → λ {( a , c ) → Σ[ b ∈ B ] ( (a , b) ∈ R × (b , c) ∈ S )}
; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r }
}

18
src/Cat/Categories/Sets.agda
View file

@ -3,7 +3,6 @@ module Cat.Categories.Sets where
open import Cubical
open import Agda.Primitive
open import Data.Product
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Cat.Category
open import Cat.Functor
@ -15,7 +14,7 @@ module _ {ℓ : Level} where
{ Object = Set ℓ
; Arrow = λ T U → T → U
; 𝟙 = id
; _⊕_ = _∘′_
; _∘_ = _∘′_
; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) }
}
where
@ -26,16 +25,15 @@ module _ {ℓ : Level} where
_&&&_ : (X → A × B)
_&&&_ x = f x , g x
module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where
_S⊕_ = Sets ._⊕_
lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g
lem : Sets [ proj₁ ∘ (f &&& g)] ≡ f × Sets [ proj₂ ∘ (f &&& g)] ≡ g
proj₁ lem = refl
proj₂ lem = refl
instance
isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd
isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂
isProduct f g = f &&& g , lem f g
product : (A B : Sets .Object) → Product {ℂ = Sets} A B
product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct }
product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
instance
SetsHasProducts : HasProducts Sets
@ -49,9 +47,9 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
{ func* = λ B → ℂ .Arrow A B
; func→ = ℂ ._⊕_
; func→ = ℂ ._∘_
; isFunctor = record
{ ident = funExt λ _ → snd ident
{ ident = funExt λ _ → proj₂ ident
; distrib = funExt λ x → sym assoc
}
}
@ -66,9 +64,9 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ func* = λ A → ℂ .Arrow A B
; func→ = λ f g → ℂ ._⊕_ g f
; func→ = λ f g → ℂ ._∘_ g f
; isFunctor = record
{ ident = funExt λ x → fst ident
{ ident = funExt λ x → proj₁ ident
; distrib = funExt λ x → assoc
}
}

30
src/Cat/Category.agda
View file

@ -10,7 +10,7 @@ open import Data.Product renaming
; ∃! to ∃!≈
)
open import Data.Empty
open import Function
import Function
open import Cubical
∃! : ∀ {a b} {A : Set a}
@ -43,9 +43,9 @@ record Category (ℓ ℓ' : Level) : Set (lsuc (ℓ' ⊔ ℓ)) where
Object : Set ℓ
Arrow : Object → Object → Set ℓ'
𝟙 : {o : Object} → Arrow o o
_⊕_ : { a b c : Object } → Arrow b c → Arrow a b → Arrow a c
{{isCategory}} : IsCategory Object Arrow 𝟙 _⊕_
infixl 45 _⊕_
_∘_ : {A B C : Object} → Arrow B C → Arrow A B → Arrow A C
{{isCategory}} : IsCategory Object Arrow 𝟙 _∘_
infixl 10 _∘_
domain : { a b : Object } → Arrow a b → Object
domain {a = a} _ = a
codomain : { a b : Object } → Arrow a b → Object
@ -57,18 +57,18 @@ _[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : ℂ .Object) →
_[_,_] = Arrow
_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : ℂ .Object} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
_[_∘_] = _⊕_
_[_∘_] = _∘_
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
module _ { A B : ℂ .Object } where
Isomorphism : (f : ℂ .Arrow A B) → Set ℓ'
Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ ._⊕_ g f ≡ ℂ .𝟙 × ℂ ._⊕_ f g ≡ ℂ .𝟙
Isomorphism f = Σ[ g ∈ ℂ .Arrow B A ] ℂ [ g ∘ f ] ≡ ℂ .𝟙 × ℂ [ f ∘ g ] ≡ ℂ .𝟙
Epimorphism : {X : ℂ .Object } → (f : ℂ .Arrow A B) → Set ℓ'
Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ ._⊕_ g₀ f ≡ ℂ ._⊕_ g₁ f → g₀ ≡ g₁
Epimorphism {X} f = ( g₀ g₁ : ℂ .Arrow B X ) → ℂ [ g₀ ∘ f ] ≡ ℂ [ g₁ ∘ f ] → g₀ ≡ g₁
Monomorphism : {X : ℂ .Object} → (f : ℂ .Arrow A B) → Set ℓ'
Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ ._⊕_ f g₀ ≡ ℂ ._⊕_ f g₁ → g₀ ≡ g₁
Monomorphism {X} f = ( g₀ g₁ : ℂ .Arrow X A ) → ℂ [ f ∘ g₀ ] ≡ ℂ [ f ∘ g₁ ] → g₀ ≡ g₁
-- Isomorphism of objects
_≅_ : (A B : Object ℂ) → Set ℓ'
@ -78,7 +78,7 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} whe
IsProduct : (π₁ : Arrow ℂ obj A) (π₂ : Arrow ℂ obj B) → Set (ℓ ⊔ ℓ')
IsProduct π₁ π₂
= ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
→ ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ ._⊕_ π₂ x ≡ x₂)
→ ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)
-- Tip from Andrea; Consider this style for efficiency:
-- record IsProduct {ℓ ℓ' : Level} (ℂ : Category {ℓ} {ℓ'})
@ -112,17 +112,17 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔
parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B'
→ ℂ .Arrow (objectProduct A B) (objectProduct A' B')
parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B')
(ℂ ._⊕_ a ((product A B) .proj₁))
(ℂ ._⊕_ b ((product A B) .proj₂))
(ℂ [ a ∘ (product A B) .proj₁ ])
(ℂ [ b ∘ (product A B) .proj₂ ])
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
Opposite : Category ℓ ℓ'
Opposite =
record
{ Object = ℂ .Object
; Arrow = flip (ℂ .Arrow)
; Arrow = Function.flip (ℂ .Arrow)
; 𝟙 = ℂ .𝟙
; _⊕_ = flip (ℂ ._⊕_)
; _∘_ = Function.flip (ℂ ._∘_)
; isCategory = record { assoc = sym assoc ; ident = swap ident }
}
where
@ -145,7 +145,7 @@ Hom ℂ A B = Arrow ℂ A B
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where
HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B')
→ Hom ℂ A B → Hom ℂ A B'
HomFromArrow _A = _⊕_ ℂ
HomFromArrow _A = ℂ ._∘_
module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where
open HasProducts hasProducts
@ -157,7 +157,7 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
module _ (B C : ℂ .Category.Object) where
IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C)
→ ∃![ f~ ] (ℂ ._⊕_ eval (parallelProduct f~ (ℂ .𝟙)) ≡ f)
→ ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (ℂ .𝟙)] ≡ f)
record Exponential : Set (ℓ ⊔ ℓ') where
field

2
src/Cat/Category/Free.agda
View file

@ -31,6 +31,6 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
{ Object = Obj
; Arrow = Path
; 𝟙 = λ {o} → emptyPath o
; _⊕_ = λ {a b c} → concatenate {a} {b} {c}
; _∘_ = λ {a b c} → concatenate {a} {b} {c}
; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l }
}

42
src/Cat/Category/Properties.agda
View file

@ -15,27 +15,26 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Obje
open IsCategory (isCategory)
iso-is-epi : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq =
begin
iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin
g₀ ≡⟨ sym (proj₁ ident) ⟩
g₀ ⊕ 𝟙 ≡⟨ cong (_⊕_ g₀) (sym right-inv) ⟩
g₀ ⊕ (f ⊕ f-) ≡⟨ assoc ⟩
(g₀ ⊕ f) ⊕ f- ≡⟨ cong (λ φ → φ ⊕ f-) eq ⟩
(g₁ ⊕ f) ⊕ f- ≡⟨ sym assoc ⟩
g₁ ⊕ (f ⊕ f-) ≡⟨ cong (_⊕_ g₁) right-inv ⟩
g₁ ⊕ 𝟙 ≡⟨ proj₁ ident ⟩
g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩
g₀ ∘ (f ∘ f-) ≡⟨ assoc ⟩
(g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩
(g₁ ∘ f) ∘ f- ≡⟨ sym assoc ⟩
g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩
g₁ ∘ 𝟙 ≡⟨ proj₁ ident ⟩
g₁ ∎
iso-is-mono : Isomorphism {ℂ = ℂ} f → Monomorphism {ℂ = ℂ} {X = X} f
iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq =
begin
g₀ ≡⟨ sym (proj₂ ident) ⟩
𝟙 ⊕ g₀ ≡⟨ cong (λ φ → φ ⊕ g₀) (sym left-inv) ⟩
(f- ⊕ f) ⊕ g₀ ≡⟨ sym assoc ⟩
f- ⊕ (f ⊕ g₀) ≡⟨ cong (_⊕_ f-) eq ⟩
f- ⊕ (f ⊕ g₁) ≡⟨ assoc ⟩
(f- ⊕ f) ⊕ g₁ ≡⟨ cong (λ φ → φ ⊕ g₁) left-inv ⟩
𝟙 ⊕ g₁ ≡⟨ proj₂ ident ⟩
𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩
(f- ∘ f) ∘ g₀ ≡⟨ sym assoc ⟩
f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩
f- ∘ (f ∘ g₁) ≡⟨ assoc ⟩
(f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩
𝟙 ∘ g₁ ≡⟨ proj₂ ident ⟩
g₁ ∎
iso-is-epi-mono : Isomorphism {ℂ = ℂ} f → Epimorphism {ℂ = ℂ} {X = X} f × Monomorphism {ℂ = ℂ} {X = X} f
@ -71,17 +70,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
module _ {A B : ℂ .Object} (f : ℂ .Arrow A B) where
:func→: : NaturalTransformation (prshf A) (prshf B)
:func→: = (λ C x → (ℂ ._⊕_ f x)) , λ f₁ → funExt λ x → lem
:func→: = (λ C x → ℂ [ f ∘ x ]) , λ f₁ → funExt λ x → lem
where
lem = (ℂ .isCategory) .IsCategory.assoc
module _ {c : ℂ .Object} where
eqTrans : (:func→: (ℂ .𝟙 {c})) .proj₁ ≡ (Fun .𝟙 {o = prshf c}) .proj₁
eqTrans = funExt λ x → funExt λ x → ℂ .isCategory .IsCategory.ident .proj₂
eqNat : (i : I) → Natural (prshf c) (prshf c) (eqTrans i)
eqNat i f = {!!}
eqNat
: PathP (λ i → {A B : ℂ .Object} (f : Opposite ℂ .Arrow A B)
→ Sets [ eqTrans i B ∘ prshf c .Functor.func→ f ]
≡ Sets [ prshf c .Functor.func→ f ∘ eqTrans i A ])
((:func→: (ℂ .𝟙 {c})) .proj₂) ((Fun .𝟙 {o = prshf c}) .proj₂)
eqNat = λ i f i' x₁ → {!ℂ ._⊕_ ? ?!}
-- eqNat i f = {!!}
-- Sets ._⊕_ (eq₁ i B) (prshf A .func→ f) ≡ Sets ._⊕_ (prshf B .func→ f) (eq₁ i A)
:ident: : (:func→: (ℂ .𝟙 {c})) ≡ (Fun .𝟙 {o = prshf c})
:ident: i = eqTrans i , eqNat i
:ident: = NaturalTransformation≡ eqTrans eqNat
yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = Sets {ℓ}})
yoneda = record

6
src/Cat/Cubical.agda
View file

@ -18,7 +18,7 @@ open import Cat.Functor
-- categorical version of CTT
module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open Category
open Category hiding (_∘_)
open Functor
open import Function
open import Cubical
@ -53,7 +53,7 @@ module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
{ Object = Obj
; Arrow = Arr
; 𝟙 = one
; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c}
; _∘_ = λ {a b c} → _:⊕:_ {a} {b} {c}
}
Contexts = ℂ .Object
@ -96,6 +96,6 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where
{ Object = Ns → Bool
; Arrow = Mor
; 𝟙 = {!!}
; _⊕_ = {!!}
; _∘_ = {!!}
; isCategory = {!!}
}

2
src/Cat/Functor.agda
View file

@ -6,7 +6,7 @@ open import Function
open import Cat.Category
open Category
open Category hiding (_∘_)
module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
record IsFunctor