cat/src/Cat/Category/Functor.agda

142 lines
4.2 KiB
Agda
Raw Normal View History

{-# OPTIONS --cubical #-}
2018-02-05 13:59:53 +00:00
module Cat.Category.Functor where
2018-01-08 21:54:53 +00:00
open import Agda.Primitive
open import Cubical
open import Function
open import Cat.Category
2018-02-23 11:41:15 +00:00
open Category hiding (_∘_ ; raw ; IsIdentity)
2018-01-30 15:23:36 +00:00
module _ {c c' d d'}
( : Category c c')
(𝔻 : Category d d')
where
private
= c c' d d'
𝓤 = Set
record RawFunctor : 𝓤 where
field
func* : Object Object 𝔻
func→ : {A B} [ A , B ] 𝔻 [ func* A , func* B ]
2018-02-23 11:41:15 +00:00
IsIdentity : Set _
IsIdentity = {A : Object } func→ (𝟙 {A}) 𝟙 𝔻 {func* A}
IsDistributive : Set _
IsDistributive = {A B C : Object } {f : [ A , B ]} {g : [ B , C ]}
func→ ( [ g f ]) 𝔻 [ func→ g func→ f ]
record IsFunctor (F : RawFunctor) : 𝓤 where
2018-02-23 11:21:16 +00:00
open RawFunctor F public
2018-01-30 15:23:36 +00:00
field
2018-02-23 11:53:35 +00:00
isIdentity : IsIdentity
isDistributive : IsDistributive
2018-01-30 15:23:36 +00:00
record Functor : Set (c c' d d') where
field
raw : RawFunctor
{{isFunctor}} : IsFunctor raw
2018-02-23 11:21:16 +00:00
open IsFunctor isFunctor public
open Functor
module _
{a b : Level}
{ 𝔻 : Category a b}
2018-02-23 09:36:59 +00:00
(F : RawFunctor 𝔻)
where
private
2018-02-23 15:41:17 +00:00
module 𝔻 = Category 𝔻
2018-02-20 13:08:47 +00:00
propIsFunctor : isProp (IsFunctor _ _ F)
propIsFunctor isF0 isF1 i = record
2018-02-23 11:51:44 +00:00
{ isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i
2018-02-23 11:53:35 +00:00
; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i
}
where
module isF0 = IsFunctor isF0
module isF1 = IsFunctor isF1
-- Alternate version of above where `F` is indexed by an interval
module _
{a b : Level}
{ 𝔻 : Category a b}
{F : I RawFunctor 𝔻}
where
private
2018-02-23 15:41:17 +00:00
module 𝔻 = Category 𝔻
IsProp' : { : Level} (A : I Set ) Set
IsProp' A = (a0 : A i0) (a1 : A i1) A [ a0 a1 ]
2018-01-30 15:23:36 +00:00
IsFunctorIsProp' : IsProp' λ i IsFunctor _ _ (F i)
IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor 𝔻}
2018-02-23 09:36:59 +00:00
(\ F propIsFunctor F) (\ i F i)
where
2018-02-16 10:36:44 +00:00
open import Cubical.NType.Properties using (lemPropF)
2018-01-30 15:23:36 +00:00
module _ { ' : Level} { 𝔻 : Category '} where
Functor≡ : {F G : Functor 𝔻}
(eq* : func* F func* G)
2018-01-31 13:39:54 +00:00
(eq→ : (λ i {x y} [ x , y ] 𝔻 [ eq* i x , eq* i y ])
[ func→ F func→ G ])
F G
Functor≡ {F} {G} eq* eq→ i = record
{ raw = eqR i
; isFunctor = eqIsF i
}
where
eqR : raw F raw G
eqR i = record { func* = eq* i ; func→ = eq→ i }
eqIsF : (λ i IsFunctor 𝔻 (eqR i)) [ isFunctor F isFunctor G ]
eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
module _ { ' : Level} {A B C : Category '} (F : Functor B C) (G : Functor A B) where
2018-01-08 21:54:53 +00:00
private
F* = func* F
F→ = func→ F
G* = func* G
G→ = func→ G
module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where
2018-01-08 21:54:53 +00:00
dist : (F→ G→) (A [ α1 α0 ]) C [ (F→ G→) α1 (F→ G→) α0 ]
2018-01-08 21:54:53 +00:00
dist = begin
(F→ G→) (A [ α1 α0 ]) ≡⟨ refl
2018-02-23 11:53:35 +00:00
F→ (G→ (A [ α1 α0 ])) ≡⟨ cong F→ (isDistributive G)
F→ (B [ G→ α1 G→ α0 ]) ≡⟨ isDistributive F
C [ (F→ G→) α1 (F→ G→) α0 ]
2018-01-08 21:54:53 +00:00
_∘fr_ : RawFunctor A C
RawFunctor.func* _∘fr_ = F* G*
RawFunctor.func→ _∘fr_ = F→ G→
instance
isFunctor' : IsFunctor A C _∘fr_
isFunctor' = record
2018-02-23 11:49:41 +00:00
{ isIdentity = begin
(F→ G→) (𝟙 A) ≡⟨ refl
2018-02-23 11:49:41 +00:00
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)
F→ (𝟙 B) ≡⟨ isIdentity F
𝟙 C
2018-02-23 11:53:35 +00:00
; isDistributive = dist
2018-01-30 15:23:36 +00:00
}
_∘f_ : Functor A C
raw _∘f_ = _∘fr_
2018-01-08 21:54:53 +00:00
-- The identity functor
identity : { '} {C : Category '} Functor C C
identity = record
{ raw = record
{ func* = λ x x
; func→ = λ x x
}
2018-01-30 15:23:36 +00:00
; isFunctor = record
2018-02-23 11:49:41 +00:00
{ isIdentity = refl
2018-02-23 11:53:35 +00:00
; isDistributive = refl
2018-01-30 15:23:36 +00:00
}
}