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

"re-delegate" projections in new module Category

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-05 12:21:39 +01:00
parent 22a9a71870
commit 8022ed349d
7 changed files with 77 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -16,11 +16,11 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
module _ (F G : Functor ℂ 𝔻) where
-- What do you call a non-natural tranformation?
Transformation : Set (ℓc ⊔ ℓd')
Transformation = (C : ℂ .Object) → 𝔻 [ 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}
= {A B : Object ℂ}
→ (f : ℂ [ A , B ])
→ 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
@ -34,7 +34,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
NaturalTransformation≡ : {α β : NaturalTransformation F G}
→ (eq₁ : α .proj₁ ≡ β .proj₁)
→ (eq₂ : PathP
(λ i → {A B : ℂ .Object} (f : ℂ [ A , B ])
(λ i → {A B : Object ℂ} (f : ℂ [ A , B ])
→ 𝔻 [ eq₁ i B ∘ F .func→ f ]
≡ 𝔻 [ G .func→ f ∘ eq₁ i A ])
(α .proj₂) (β .proj₂))
@ -42,14 +42,14 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i
identityTrans : (F : Functor ℂ 𝔻) → Transformation F F
identityTrans F C = 𝔻 .𝟙
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 ⟩
𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.ident ⟩
F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩
𝔻 [ F→ f ∘ 𝔻 .𝟙 ] ≡⟨⟩
𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩
𝔻 [ F→ f ∘ identityTrans F A ] ∎
where
F→ = F .func→

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

@ -39,10 +39,10 @@ module _ {ℓ : Level} where
proj₁ lem = refl
proj₂ lem = refl
instance
isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} proj₁ proj₂
isProduct : {A B : Object Sets} → 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 : Object Sets) → Product {ℂ = Sets} A B
product A B = record { obj = A × B ; proj₁ = proj₁ ; proj₂ = proj₂ ; isProduct = isProduct }
instance
@ -56,8 +56,8 @@ Representable {ℓ' = ℓ'} ℂ = Functor ℂ (Sets {ℓ'})
-- The "co-yoneda" embedding.
representable : ∀ {ℓ ℓ'} {ℂ : Category ℓ ℓ'} → Category.Object ℂ → Representable ℂ
representable {ℂ = ℂ} A = record
{ func* = λ B → ℂ .Arrow A B
; func→ = ℂ ._∘_
{ func* = λ B → ℂ [ A , B ]
; func→ = ℂ [_∘_]
; isFunctor = record
{ ident = funExt λ _ → proj₂ ident
; distrib = funExt λ x → sym assoc
@ -73,8 +73,8 @@ Presheaf {ℓ' = ℓ'} ℂ = Functor (Opposite ℂ) (Sets {ℓ'})
-- Alternate name: `yoneda`
presheaf : {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} → Category.Object (Opposite ℂ) → Presheaf ℂ
presheaf {ℂ = ℂ} B = record
{ func* = λ A → ℂ .Arrow A B
; func→ = λ f g → ℂ ._∘_ g f
{ func* = λ A → ℂ [ A , B ]
; func→ = λ f g → ℂ [ g ∘ f ]
; isFunctor = record
{ ident = funExt λ x → proj₁ ident
; distrib = funExt λ x → assoc

69
src/Cat/Category.agda
View file

@ -114,27 +114,34 @@ Category ℓa ℓb = Σ (RawCategory ℓa ℓb) IsCategory
module Category {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
raw = fst ℂ
open RawCategory raw public
isCategory = snd ℂ
open RawCategory
private
module ℂ = RawCategory raw
-- _∈_ : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → (ℂ .fst .Object → Set ℓb) → Set (ℓa ⊔ ℓb)
-- A ∈ ℂ =
Object : Set ℓa
Object = ℂ.Object
Obj : ∀ {ℓa ℓb} → Category ℓa ℓb → Set ℓa
Obj ℂ = ℂ .fst .Object
Arrow = ℂ.Arrow
_[_,_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → (A : Obj ℂ) → (B : Obj ℂ) → Set ℓ'
ℂ [ A , B ] = ℂ .fst .Arrow A B
𝟙 = ℂ.𝟙
_[_∘_] : ∀ {ℓ ℓ'} → (ℂ : Category ℓ ℓ') → {A B C : Obj ℂ} → (g : ℂ [ B , C ]) → (f : ℂ [ A , B ]) → ℂ [ A , C ]
ℂ [ g ∘ f ] = ℂ .fst ._∘_ g f
_∘_ = ℂ._∘_
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where
_[_,_] : (A : Object) → (B : Object) → Set ℓb
_[_,_] = ℂ.Arrow
_[_∘_] : {A B C : Object} → (g : ℂ.Arrow B C) → (f : ℂ.Arrow A B) → ℂ.Arrow A C
_[_∘_] = ℂ._∘_
open Category using ( Object ; _[_,_] ; _[_∘_])
-- open RawCategory
module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Object ℂ} where
IsProduct : (π₁ : ℂ [ obj , A ]) (π₂ : ℂ [ obj , B ]) → Set (ℓ ⊔ ℓ')
IsProduct π₁ π₂
= ∀ {X : Obj ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
= ∀ {X : Object ℂ} (x₁ : ℂ [ X , A ]) (x₂ : ℂ [ X , B ])
→ ∃![ x ] (ℂ [ π₁ ∘ x ] ≡ x₁ × ℂ [ π₂ ∘ x ] ≡ x₂)
-- Tip from Andrea; Consider this style for efficiency:
@ -144,10 +151,10 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {A B obj : Obj ℂ} where
-- isProduct : ∀ {X : ℂ .Object} (x₁ : ℂ .Arrow X A) (x₂ : ℂ .Arrow X B)
-- → ∃![ x ] (ℂ ._⊕_ π₁ x ≡ x₁ × ℂ. _⊕_ π₂ x ≡ x₂)
record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Set (ℓ ⊔ ℓ') where
record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : Set (ℓ ⊔ ℓ') where
no-eta-equality
field
obj : Obj ℂ
obj : Object ℂ
proj₁ : ℂ [ obj , A ]
proj₂ : ℂ [ obj , B ]
{{isProduct}} : IsProduct ℂ proj₁ proj₂
@ -158,15 +165,15 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Obj ℂ) : Se
record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
field
product : ∀ (A B : Obj ℂ) → Product {ℂ = ℂ} A B
product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B
open Product
objectProduct : (A B : Obj ℂ) → Obj ℂ
objectProduct : (A B : Object ℂ) → Object ℂ
objectProduct A B = Product.obj (product A B)
-- The product mentioned in awodey in Def 6.1 is not the regular product of arrows.
-- It's a "parallel" product
parallelProduct : {A A' B B' : Obj ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
parallelProduct : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ]
→ ℂ [ 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₁ ])
@ -209,30 +216,30 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}}
open HasProducts hasProducts
open Product hiding (obj)
private
_×p_ : (A B : Obj ℂ) → Obj ℂ
_×p_ : (A B : Object ℂ) → Object ℂ
_×p_ A B = Product.obj (product A B)
module _ (B C : Obj ℂ) where
IsExponential : (Cᴮ : Obj ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : Obj ℂ) (f : ℂ [ A ×p B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.raw ℂ .𝟙)] ≡ f)
module _ (B C : Object ℂ) where
IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ')
IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ])
→ ∃![ f~ ] (ℂ [ eval ∘ parallelProduct f~ (Category.𝟙 ℂ)] ≡ f)
record Exponential : Set (ℓ ⊔ ℓ') where
field
-- obj ≡ Cᴮ
obj : Obj ℂ
obj : Object ℂ
eval : ℂ [ obj ×p B , C ]
{{isExponential}} : IsExponential obj eval
-- If I make this an instance-argument then the instance resolution
-- algorithm goes into an infinite loop. Why?
exponentialsHaveProducts : HasProducts ℂ
exponentialsHaveProducts = hasProducts
transpose : (A : Obj ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ]
transpose A f = fst (isExponential A f)
record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where
field
exponent : (A B : Obj ℂ) → Exponential ℂ A B
exponent : (A B : Object ℂ) → Exponential ℂ A B
record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where
field
@ -242,15 +249,15 @@ record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
unique = isContr
IsInitial : Obj ℂ → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Obj ℂ} → unique (ℂ [ I , X ])
IsInitial : Object ℂ → Set (ℓa ⊔ ℓb)
IsInitial I = {X : Object ℂ} → unique (ℂ [ I , X ])
IsTerminal : Obj ℂ → Set (ℓa ⊔ ℓb)
IsTerminal : Object ℂ → Set (ℓa ⊔ ℓb)
-- ∃![ ? ] ?
IsTerminal T = {X : Obj ℂ} → unique (ℂ [ X , T ])
IsTerminal T = {X : Object ℂ} → unique (ℂ [ X , T ])
Initial : Set (ℓa ⊔ ℓb)
Initial = Σ (Obj ℂ) IsInitial
Initial = Σ (Object ℂ) IsInitial
Terminal : Set (ℓa ⊔ ℓb)
Terminal = Σ (Obj ℂ) IsTerminal
Terminal = Σ (Object ℂ) IsTerminal

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

@ -12,23 +12,23 @@ module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
open module ℂ = Category ℂ
postulate
Path : ( a b : Obj ℂ ) → Set ℓ'
emptyPath : (o : Obj ℂ) → Path o o
concatenate : {a b c : Obj ℂ} → Path b c → Path a b → Path a c
Path : (a b : ℂ.Object) → Set ℓ'
emptyPath : (o : ℂ.Object) → Path o o
concatenate : {a b c : ℂ.Object} → Path b c → Path a b → Path a c
private
module _ {A B C D : Obj ℂ} {r : Path A B} {q : Path B C} {p : Path C D} where
module _ {A B C D : ℂ.Object} {r : Path A B} {q : Path B C} {p : Path C D} where
postulate
p-assoc : concatenate {A} {C} {D} p (concatenate {A} {B} {C} q r)
≡ concatenate {A} {B} {D} (concatenate {B} {C} {D} p q) r
module _ {A B : Obj ℂ} {p : Path A B} where
module _ {A B : ℂ.Object} {p : Path A B} where
postulate
ident-r : concatenate {A} {A} {B} p (emptyPath A) ≡ p
ident-l : concatenate {A} {B} {B} (emptyPath B) p ≡ p
RawFree : RawCategory ℓ ℓ'
RawFree = record
{ Object = Obj ℂ
{ Object = ℂ.Object
; Arrow = Path
; 𝟙 = λ {o} → emptyPath o
; _∘_ = λ {a b c} → concatenate {a} {b} {c}

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

@ -12,7 +12,7 @@ open import Cat.Categories.Sets
open import Cat.Equality
open Equality.Data.Product
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : ℂ .Category.Object } {X : ℂ .Category.Object} (f : ℂ .Category.Arrow A B) where
module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} { A B : Category.Object ℂ } {X : Category.Object ℂ} (f : Category.Arrow ℂ A B) where
open Category ℂ
open IsCategory (isCategory)

14
src/Cat/CwF.agda
View file

@ -17,20 +17,20 @@ module _ {ℓa ℓb : Level} where
-- "A base category"
ℂ : Category ℓa ℓb
-- It's objects are called contexts
Contexts = ℂ .Object
Contexts = Object ℂ
-- It's arrows are called substitutions
Substitutions = ℂ .Arrow
Substitutions = Arrow ℂ
field
-- A functor T
T : Functor (Opposite ℂ) (Fam ℓa ℓb)
-- Empty context
[] : Terminal ℂ
Type : (Γ : ℂ .Object) → Set ℓa
Type : (Γ : Object ℂ) → Set ℓa
Type Γ = proj₁ (T .func* Γ)
module _ {Γ : ℂ .Object} {A : Type Γ} where
module _ {Γ : Object ℂ} {A : Type Γ} where
module _ {A B : ℂ .Object} {γ : ℂ [ A , B ]} where
module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
(λ f →
{x : proj₁ (func* T B)} →
@ -44,8 +44,8 @@ module _ {ℓa ℓb : Level} where
record ContextComprehension : Set (ℓa ⊔ ℓb) where
field
Γ&A : ℂ .Object
proj1 : ℂ .Arrow Γ&A Γ
Γ&A : Object ℂ
proj1 : ℂ [ Γ&A , Γ ]
-- proj2 : ????
-- if γ : ℂ [ A , B ]

26
src/Cat/Functor.agda
View file

@ -10,20 +10,20 @@ open Category hiding (_∘_)
module _ {ℓc ℓc' ℓd ℓd'} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
record IsFunctor
(func* : Obj ℂ → Obj 𝔻)
(func→ : {A B : Obj ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
(func* : Object ℂ → Object 𝔻)
(func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ])
: Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
field
ident : {c : Obj ℂ} → func→ (ℂ .𝟙 {c}) ≡ 𝔻 .𝟙 {func* c}
ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
-- TODO: Avoid use of ugly explicit arguments somehow.
-- This guy managed to do it:
-- https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda
distrib : {A B C : ℂ .Object} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
→ func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
record Functor : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where
field
func* : ℂ .Object → 𝔻 .Object
func* : Object ℂ → Object 𝔻
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
{{isFunctor}} : IsFunctor func* func→
@ -33,11 +33,11 @@ open Functor
module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
IsFunctor≡
: {func* : ℂ .Object → 𝔻 .Object}
{func→ : {A B : ℂ .Object} → ℂ .Arrow A B → 𝔻 .Arrow (func* A) (func* B)}
: {func* : Object ℂ → Object 𝔻}
{func→ : {A B : Object ℂ} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]}
{F G : IsFunctor ℂ 𝔻 func* func→}
→ (eqI
: (λ i → ∀ {A} → func→ (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {func* A})
: (λ i → ∀ {A} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A})
[ F .ident ≡ G .ident ])
→ (eqD :
(λ i → ∀ {A B C} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
@ -61,7 +61,7 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
F→ = F .func→
G* = G .func*
G→ = G .func→
module _ {a0 a1 a2 : A .Object} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
dist = begin
@ -77,10 +77,10 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
; func→ = F→ ∘ G→
; isFunctor = record
{ ident = begin
(F→ ∘ G→) (A .𝟙) ≡⟨ refl ⟩
F→ (G→ (A .𝟙)) ≡⟨ cong F→ (G .isFunctor .ident)⟩
F→ (B .𝟙) ≡⟨ F .isFunctor .ident ⟩
C .𝟙 ∎
(F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩
F→ (𝟙 B) ≡⟨ F .isFunctor .ident ⟩
𝟙 C ∎
; distrib = dist
}
}