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

Chain reexport things in Functor

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-02-23 12:21:16 +01:00
parent 885fd8fa69
commit e46edf1f68
1 changed files with 6 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Cat/Category/Functor.agda
View file

@ -24,7 +24,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ] func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
record IsFunctor (F : RawFunctor) : 𝓤 where record IsFunctor (F : RawFunctor) : 𝓤 where
open RawFunctor F open RawFunctor F public
field field
ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c} ident : {c : Object ℂ} → func→ (𝟙 ℂ {c}) ≡ 𝟙 𝔻 {func* c}
distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]} distrib : {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
@ -35,16 +35,8 @@ module _ {ℓc ℓc' ℓd ℓd'}
raw : RawFunctor raw : RawFunctor
{{isFunctor}} : IsFunctor raw {{isFunctor}} : IsFunctor raw
private open IsFunctor isFunctor public
module R = RawFunctor raw
func* : Object ℂ → Object 𝔻
func* = R.func*
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
func→ = R.func→
open IsFunctor
open Functor open Functor
module _ module _
@ -108,8 +100,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ]
dist = begin dist = begin
(F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩
F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (G .isFunctor .distrib)⟩ F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (distrib G) ⟩
F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ F .isFunctor .distrib ⟩ F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ distrib F ⟩
C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
_∘fr_ : RawFunctor A C _∘fr_ : RawFunctor A C
@ -120,8 +112,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
isFunctor' = record isFunctor' = record
{ ident = begin { ident = begin
(F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩
F→ (G→ (𝟙 A)) ≡⟨ cong F→ (G .isFunctor .ident)⟩ F→ (G→ (𝟙 A)) ≡⟨ cong F→ (ident G)⟩
F→ (𝟙 B) ≡⟨ F .isFunctor .ident ⟩ F→ (𝟙 B) ≡⟨ ident F ⟩
𝟙 C ∎ 𝟙 C ∎
; distrib = dist ; distrib = dist
} }