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

Move the category of functors

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-01-22 14:44:25 +01:00
parent 9fdf6b589b
commit fd03049c92
2 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Cat.agda
View file

@ -1,13 +1,13 @@
module Cat where module Cat where
import Cat.Categories.Sets import Cat.Cubical
import Cat.Categories.Cat import Cat.Category
import Cat.Categories.Rel import Cat.Functor
import Cat.Category.Pathy import Cat.Category.Pathy
import Cat.Category.Bij import Cat.Category.Bij
import Cat.Category.Free import Cat.Category.Free
import Cat.Category.Properties import Cat.Category.Properties
import Cat.Category import Cat.Categories.Sets
import Cat.Cubical import Cat.Categories.Cat
import Cat.Functor import Cat.Categories.Rel
import Cat.Naturality import Cat.Categories.Fun

7
src/Cat/Naturality.agda → src/Cat/Categories/Fun.agda
View file

@ -1,5 +1,5 @@
{-# OPTIONS --allow-unsolved-metas #-} {-# OPTIONS --allow-unsolved-metas #-}
module Cat.Naturality where module Cat.Categories.Fun where
open import Agda.Primitive open import Agda.Primitive
open import Cubical open import Cubical
@ -93,8 +93,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat
; ident = λ {A B} → :ident: {A} {B} ; ident = λ {A B} → :ident: {A} {B}
} }
aCat : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd')) -- Functor categories. Objects are functors, arrows are natural transformations.
aCat = record Fun : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd'))
Fun = record
{ Object = Functor ℂ 𝔻 { Object = Functor ℂ 𝔻
; Arrow = NaturalTranformation ; Arrow = NaturalTranformation
; 𝟙 = λ {F} → identityNat F ; 𝟙 = λ {F} → identityNat F