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

Implement representable functors

This commit is contained in:
Frederik Hanghøj Iversen 2018-01-17 12:10:18 +01:00
parent 7090c2c6bf
commit 902b953ad0
2 changed files with 10 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/Cat/Categories/Sets.agda
View File

@ -25,22 +25,8 @@ Sets {ℓ} = record
; ident = funExt (λ x → refl) , funExt (λ x → refl)
}
module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ}} where
private
C-Obj = Object ℂ
_+_ = Arrow ℂ
RepFunctor : Functor ℂ Sets
RepFunctor =
record
{ func* = λ A → (B : C-Obj) → Hom {ℂ = ℂ} A B
; func→ = λ { {c} {c'} f g → {!HomFromArrow {ℂ = {!!}} c' g!} }
; ident = {!!}
; distrib = {!!}
}
Hom0 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'})
Hom0 {ℂ = ℂ} A = record
representable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor ℂ (Sets {ℓ'})
representable {ℂ = ℂ} A = record
{ func* = λ B → ℂ.Arrow A B
; func→ = λ f g → f ℂ.⊕ g
; ident = funExt λ _ → snd ℂ.ident
@ -49,12 +35,12 @@ Hom0 {ℂ = ℂ} A = record
where
open module ℂ = Category ℂ
Hom1 : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object ℂ → Functor (Opposite ℂ) (Sets {ℓ'})
Hom1 {ℂ = ℂ} B = record
coRepresentable : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → Category.Object (Opposite ℂ) → Functor (Opposite ℂ) (Sets {ℓ'})
coRepresentable {ℂ = ℂ} B = record
{ func* = λ A → ℂ.Arrow A B
; func→ = λ f g → {!!} ℂ.⊕ {!!}
; ident = {!!}
; distrib = {!!}
; func→ = λ f g → g ℂ.⊕ f
; ident = funExt λ x → fst ℂ.ident
; distrib = funExt λ x → ℂ.assoc
}
where
open module ℂ = Category ℂ

6
src/Cat/Category.agda
View File

@ -128,8 +128,8 @@ Opposite ℂ =
where
open module ℂ = Category ℂ
Hom : {ℓ ℓ' : Level} → {ℂ : Category {ℓ} {ℓ'}} → (A B : Object ℂ) → Set ℓ'
Hom {ℂ = ℂ} A B = Arrow ℂ A B
Hom : {ℓ ℓ' : Level} → (ℂ : Category {ℓ} {ℓ'}) → (A B : Object ℂ) → Set ℓ'
Hom ℂ A B = Arrow ℂ A B
module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
private
@ -138,5 +138,5 @@ module _ {ℓ ℓ' : Level} {ℂ : Category {ℓ} {ℓ'}} where
_+_ = _⊕_ ℂ
HomFromArrow : (A : Obj) → {B B' : Obj} → (g : Arr B B')
→ Hom {ℂ = ℂ} A B → Hom {ℂ = ℂ} A B'
→ Hom ℂ A B → Hom ℂ A B'
HomFromArrow _A g = λ f → g + f