Rename func* and func-> to omap and fmap respectively
This commit is contained in:
parent
2fcc583646
commit
5ad506a09f
|
|
@ -17,7 +17,7 @@ open import Cat.Category.NaturalTransformation
|
|||
open import Cat.Equality
|
||||
open Equality.Data.Product
|
||||
|
||||
open Functor using (func→ ; func*)
|
||||
open Functor using (fmap ; omap)
|
||||
open Category using (Object ; 𝟙)
|
||||
|
||||
-- The category of categories
|
||||
|
|
@ -104,13 +104,13 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
|
|||
|
||||
proj₁ : Functor obj ℂ
|
||||
proj₁ = record
|
||||
{ raw = record { func* = fst ; func→ = fst }
|
||||
{ raw = record { omap = fst ; fmap = fst }
|
||||
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
|
||||
}
|
||||
|
||||
proj₂ : Functor obj 𝔻
|
||||
proj₂ = record
|
||||
{ raw = record { func* = snd ; func→ = snd }
|
||||
{ raw = record { omap = snd ; fmap = snd }
|
||||
; isFunctor = record { isIdentity = refl ; isDistributive = refl }
|
||||
}
|
||||
|
||||
|
|
@ -119,8 +119,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
|
|||
x : Functor X obj
|
||||
x = record
|
||||
{ raw = record
|
||||
{ func* = λ x → x₁.func* x , x₂.func* x
|
||||
; func→ = λ x → x₁.func→ x , x₂.func→ x
|
||||
{ omap = λ x → x₁.omap x , x₂.omap x
|
||||
; fmap = λ x → x₁.fmap x , x₂.fmap x
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = Σ≡ x₁.isIdentity x₂.isIdentity
|
||||
|
|
@ -175,8 +175,8 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
Categoryℓ = Category ℓ ℓ
|
||||
open Fun ℂ 𝔻 renaming (identity to idN)
|
||||
private
|
||||
:func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
|
||||
:func*: (F , A) = func* F A
|
||||
:omap: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻
|
||||
:omap: (F , A) = omap F A
|
||||
|
||||
prodObj : Categoryℓ
|
||||
prodObj = Fun
|
||||
|
|
@ -193,28 +193,28 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
B : Object ℂ
|
||||
B = proj₂ cod
|
||||
|
||||
:func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
|
||||
→ 𝔻 [ func* F A , func* G B ]
|
||||
:func→: ((θ , θNat) , f) = result
|
||||
:fmap: : (pobj : NaturalTransformation F G × ℂ [ A , B ])
|
||||
→ 𝔻 [ omap F A , omap G B ]
|
||||
:fmap: ((θ , θNat) , f) = result
|
||||
where
|
||||
θA : 𝔻 [ func* F A , func* G A ]
|
||||
θA : 𝔻 [ omap F A , omap G A ]
|
||||
θA = θ A
|
||||
θB : 𝔻 [ func* F B , func* G B ]
|
||||
θB : 𝔻 [ omap F B , omap G B ]
|
||||
θB = θ B
|
||||
F→f : 𝔻 [ func* F A , func* F B ]
|
||||
F→f = func→ F f
|
||||
G→f : 𝔻 [ func* G A , func* G B ]
|
||||
G→f = func→ G f
|
||||
l : 𝔻 [ func* F A , func* G B ]
|
||||
F→f : 𝔻 [ omap F A , omap F B ]
|
||||
F→f = fmap F f
|
||||
G→f : 𝔻 [ omap G A , omap G B ]
|
||||
G→f = fmap G f
|
||||
l : 𝔻 [ omap F A , omap G B ]
|
||||
l = 𝔻 [ θB ∘ F→f ]
|
||||
r : 𝔻 [ func* F A , func* G B ]
|
||||
r : 𝔻 [ omap F A , omap G B ]
|
||||
r = 𝔻 [ G→f ∘ θA ]
|
||||
-- There are two choices at this point,
|
||||
-- but I suppose the whole point is that
|
||||
-- by `θNat f` we have `l ≡ r`
|
||||
-- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ]
|
||||
-- lem : 𝔻 [ θ B ∘ F .fmap f ] ≡ 𝔻 [ G .fmap f ∘ θ A ]
|
||||
-- lem = θNat f
|
||||
result : 𝔻 [ func* F A , func* G B ]
|
||||
result : 𝔻 [ omap F A , omap G B ]
|
||||
result = l
|
||||
|
||||
open CatProduct renaming (obj to _×p_) using ()
|
||||
|
|
@ -227,19 +227,19 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
C = proj₂ c
|
||||
|
||||
-- NaturalTransformation F G × ℂ .Arrow A B
|
||||
-- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
|
||||
-- :ident: : :fmap: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙
|
||||
-- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity)
|
||||
-- where
|
||||
-- open module 𝔻 = IsCategory (𝔻 .isCategory)
|
||||
-- Unfortunately the equational version has some ambigous arguments.
|
||||
|
||||
:ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
|
||||
:ident: : :fmap: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻
|
||||
:ident: = begin
|
||||
:func→: {c} {c} (𝟙 (prodObj ×p ℂ) {c}) ≡⟨⟩
|
||||
:func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩
|
||||
𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩
|
||||
𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
|
||||
func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩
|
||||
:fmap: {c} {c} (𝟙 (prodObj ×p ℂ) {c}) ≡⟨⟩
|
||||
:fmap: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩
|
||||
𝔻 [ identityTrans F C ∘ fmap F (𝟙 ℂ)] ≡⟨⟩
|
||||
𝔻 [ 𝟙 𝔻 ∘ fmap F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩
|
||||
fmap F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩
|
||||
𝟙 𝔻 ∎
|
||||
where
|
||||
open module 𝔻 = Category 𝔻
|
||||
|
|
@ -279,28 +279,28 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
ηθNat = proj₂ ηθNT
|
||||
|
||||
:isDistributive: :
|
||||
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ]
|
||||
≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ]
|
||||
𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ fmap F ( ℂ [ g ∘ f ] ) ]
|
||||
≡ 𝔻 [ 𝔻 [ η C ∘ fmap G g ] ∘ 𝔻 [ θ B ∘ fmap F f ] ]
|
||||
:isDistributive: = begin
|
||||
𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ]
|
||||
𝔻 [ (ηθ C) ∘ fmap F (ℂ [ g ∘ f ]) ]
|
||||
≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩
|
||||
𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
|
||||
𝔻 [ fmap H (ℂ [ g ∘ f ]) ∘ (ηθ A) ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩
|
||||
𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ]
|
||||
𝔻 [ 𝔻 [ fmap H g ∘ fmap H f ] ∘ (ηθ A) ]
|
||||
≡⟨ sym isAssociative ⟩
|
||||
𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩
|
||||
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
|
||||
𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩
|
||||
𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ]
|
||||
𝔻 [ fmap H g ∘ 𝔻 [ fmap H f ∘ ηθ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ fmap H g ∘ φ ]) isAssociative ⟩
|
||||
𝔻 [ fmap H g ∘ 𝔻 [ 𝔻 [ fmap H f ∘ η A ] ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ fmap H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩
|
||||
𝔻 [ fmap H g ∘ 𝔻 [ 𝔻 [ η B ∘ fmap G f ] ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ fmap H g ∘ φ ]) (sym isAssociative) ⟩
|
||||
𝔻 [ fmap H g ∘ 𝔻 [ η B ∘ 𝔻 [ fmap G f ∘ θ A ] ] ]
|
||||
≡⟨ isAssociative ⟩
|
||||
𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩
|
||||
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩
|
||||
𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎
|
||||
𝔻 [ 𝔻 [ fmap H g ∘ η B ] ∘ 𝔻 [ fmap G f ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ fmap G f ∘ θ A ] ]) (sym (ηNat g)) ⟩
|
||||
𝔻 [ 𝔻 [ η C ∘ fmap G g ] ∘ 𝔻 [ fmap G f ∘ θ A ] ]
|
||||
≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ fmap G g ] ∘ φ ]) (sym (θNat f)) ⟩
|
||||
𝔻 [ 𝔻 [ η C ∘ fmap G g ] ∘ 𝔻 [ θ B ∘ fmap F f ] ] ∎
|
||||
where
|
||||
open Category 𝔻
|
||||
module H = Functor H
|
||||
|
|
@ -309,8 +309,8 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where
|
|||
-- :eval: : Functor (prodObj ×p ℂ) 𝔻
|
||||
eval = record
|
||||
{ raw = record
|
||||
{ func* = :func*:
|
||||
; func→ = λ {dom} {cod} → :func→: {dom} {cod}
|
||||
{ omap = :omap:
|
||||
; fmap = λ {dom} {cod} → :fmap: {dom} {cod}
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = λ {o} → :ident: {o}
|
||||
|
|
|
|||
|
|
@ -28,20 +28,20 @@ module _ {ℓa ℓb : Level} where
|
|||
private
|
||||
module T = Functor T
|
||||
Type : (Γ : Object ℂ) → Set ℓa
|
||||
Type Γ = proj₁ (proj₁ (T.func* Γ))
|
||||
Type Γ = proj₁ (proj₁ (T.omap Γ))
|
||||
|
||||
module _ {Γ : Object ℂ} {A : Type Γ} where
|
||||
|
||||
-- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where
|
||||
-- k : Σ (proj₁ (func* T B) → proj₁ (func* T A))
|
||||
-- k : Σ (proj₁ (omap T B) → proj₁ (omap T A))
|
||||
-- (λ f →
|
||||
-- {x : proj₁ (func* T B)} →
|
||||
-- proj₂ (func* T B) x → proj₂ (func* T A) (f x))
|
||||
-- k = T.func→ γ
|
||||
-- k₁ : proj₁ (func* T B) → proj₁ (func* T A)
|
||||
-- {x : proj₁ (omap T B)} →
|
||||
-- proj₂ (omap T B) x → proj₂ (omap T A) (f x))
|
||||
-- k = T.fmap γ
|
||||
-- k₁ : proj₁ (omap T B) → proj₁ (omap T A)
|
||||
-- k₁ = proj₁ k
|
||||
-- k₂ : ({x : proj₁ (func* T B)} →
|
||||
-- proj₂ (func* T B) x → proj₂ (func* T A) (k₁ x))
|
||||
-- k₂ : ({x : proj₁ (omap T B)} →
|
||||
-- proj₂ (omap T B) x → proj₂ (omap T A) (k₁ x))
|
||||
-- k₂ = proj₂ k
|
||||
|
||||
record ContextComprehension : Set (ℓa ⊔ ℓb) where
|
||||
|
|
@ -51,7 +51,7 @@ module _ {ℓa ℓb : Level} where
|
|||
-- proj2 : ????
|
||||
|
||||
-- if γ : ℂ [ A , B ]
|
||||
-- then T .func→ γ (written T[γ]) interpret substitutions in types and terms respectively.
|
||||
-- then T .fmap γ (written T[γ]) interpret substitutions in types and terms respectively.
|
||||
-- field
|
||||
-- ump : {Δ : ℂ .Object} → (γ : ℂ [ Δ , Γ ])
|
||||
-- → (a : {!!}) → {!!}
|
||||
|
|
|
|||
|
|
@ -97,8 +97,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
representable : Category.Object ℂ → Representable
|
||||
representable A = record
|
||||
{ raw = record
|
||||
{ func* = λ B → ℂ [ A , B ] , arrowsAreSets
|
||||
; func→ = ℂ [_∘_]
|
||||
{ omap = λ B → ℂ [ A , B ] , arrowsAreSets
|
||||
; fmap = ℂ [_∘_]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = funExt λ _ → proj₂ isIdentity
|
||||
|
|
@ -110,8 +110,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
presheaf : Category.Object (opposite ℂ) → Presheaf
|
||||
presheaf B = record
|
||||
{ raw = record
|
||||
{ func* = λ A → ℂ [ A , B ] , arrowsAreSets
|
||||
; func→ = λ f g → ℂ [ g ∘ f ]
|
||||
{ omap = λ A → ℂ [ A , B ] , arrowsAreSets
|
||||
; fmap = λ f g → ℂ [ g ∘ f ]
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = funExt λ x → proj₁ isIdentity
|
||||
|
|
|
|||
|
|
@ -24,39 +24,39 @@ module _ {ℓc ℓc' ℓd ℓd'}
|
|||
→ ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
|
||||
record RawFunctor : 𝓤 where
|
||||
field
|
||||
func* : Object ℂ → Object 𝔻
|
||||
func→ : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ func* A , func* B ]
|
||||
omap : Object ℂ → Object 𝔻
|
||||
fmap : ∀ {A B} → ℂ [ A , B ] → 𝔻 [ omap A , omap B ]
|
||||
|
||||
IsIdentity : Set _
|
||||
IsIdentity = {A : Object ℂ} → func→ (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {func* A}
|
||||
IsIdentity = {A : Object ℂ} → fmap (𝟙 ℂ {A}) ≡ 𝟙 𝔻 {omap A}
|
||||
|
||||
IsDistributive : Set _
|
||||
IsDistributive = {A B C : Object ℂ} {f : ℂ [ A , B ]} {g : ℂ [ B , C ]}
|
||||
→ func→ (ℂ [ g ∘ f ]) ≡ 𝔻 [ func→ g ∘ func→ f ]
|
||||
→ fmap (ℂ [ g ∘ f ]) ≡ 𝔻 [ fmap g ∘ fmap f ]
|
||||
|
||||
-- | Equality principle for raw functors
|
||||
--
|
||||
-- The type of `func→` depend on the value of `func*`. We can wrap this up
|
||||
-- The type of `fmap` depend on the value of `omap`. We can wrap this up
|
||||
-- into an equality principle for this type like is done for e.g. `Σ` using
|
||||
-- `pathJ`.
|
||||
module _ {x y : RawFunctor} where
|
||||
open RawFunctor
|
||||
private
|
||||
P : (omap : Omap) → (eq : func* x ≡ omap) → Set _
|
||||
P : (omap' : Omap) → (eq : omap x ≡ omap') → Set _
|
||||
P y eq = (fmap' : Fmap y) → (λ i → Fmap (eq i))
|
||||
[ func→ x ≡ fmap' ]
|
||||
[ fmap x ≡ fmap' ]
|
||||
module _
|
||||
(eq : (λ i → Omap) [ func* x ≡ func* y ])
|
||||
(kk : P (func* x) refl)
|
||||
(eq : (λ i → Omap) [ omap x ≡ omap y ])
|
||||
(kk : P (omap x) refl)
|
||||
where
|
||||
private
|
||||
p : P (func* y) eq
|
||||
p = pathJ P kk (func* y) eq
|
||||
eq→ : (λ i → Fmap (eq i)) [ func→ x ≡ func→ y ]
|
||||
eq→ = p (func→ y)
|
||||
p : P (omap y) eq
|
||||
p = pathJ P kk (omap y) eq
|
||||
eq→ : (λ i → Fmap (eq i)) [ fmap x ≡ fmap y ]
|
||||
eq→ = p (fmap y)
|
||||
RawFunctor≡ : x ≡ y
|
||||
func* (RawFunctor≡ i) = eq i
|
||||
func→ (RawFunctor≡ i) = eq→ i
|
||||
omap (RawFunctor≡ i) = eq i
|
||||
fmap (RawFunctor≡ i) = eq→ i
|
||||
|
||||
record IsFunctor (F : RawFunctor) : 𝓤 where
|
||||
open RawFunctor F public
|
||||
|
|
@ -124,10 +124,10 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
|
|||
|
||||
module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where
|
||||
private
|
||||
F* = func* F
|
||||
F→ = func→ F
|
||||
G* = func* G
|
||||
G→ = func→ G
|
||||
F* = omap F
|
||||
F→ = fmap F
|
||||
G* = omap G
|
||||
G→ = fmap G
|
||||
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 ]
|
||||
|
|
@ -138,8 +138,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
|
|||
C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎
|
||||
|
||||
_∘fr_ : RawFunctor A C
|
||||
RawFunctor.func* _∘fr_ = F* ∘ G*
|
||||
RawFunctor.func→ _∘fr_ = F→ ∘ G→
|
||||
RawFunctor.omap _∘fr_ = F* ∘ G*
|
||||
RawFunctor.fmap _∘fr_ = F→ ∘ G→
|
||||
instance
|
||||
isFunctor' : IsFunctor A C _∘fr_
|
||||
isFunctor' = record
|
||||
|
|
@ -158,8 +158,8 @@ module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : F
|
|||
identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C
|
||||
identity = record
|
||||
{ raw = record
|
||||
{ func* = λ x → x
|
||||
; func→ = λ x → x
|
||||
{ omap = λ x → x
|
||||
; fmap = λ x → x
|
||||
}
|
||||
; isFunctor = record
|
||||
{ isIdentity = refl
|
||||
|
|
|
|||
|
|
@ -39,8 +39,8 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
joinN : Natural F[ R ∘ R ] R joinT
|
||||
joinN = proj₂ joinNT
|
||||
|
||||
Romap = Functor.func* R
|
||||
Rfmap = Functor.func→ R
|
||||
Romap = Functor.omap R
|
||||
Rfmap = Functor.fmap R
|
||||
|
||||
bind : {X Y : Object} → ℂ [ X , Romap Y ] → ℂ [ Romap X , Romap Y ]
|
||||
bind {X} {Y} f = joinT Y ∘ Rfmap f
|
||||
|
|
@ -69,10 +69,10 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
|
||||
isNatural : IsNatural
|
||||
isNatural {X} {Y} f = begin
|
||||
joinT Y ∘ R.func→ f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩
|
||||
joinT Y ∘ (R.func→ f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
|
||||
joinT Y ∘ (pureT (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
|
||||
joinT Y ∘ pureT (R.func* Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
|
||||
joinT Y ∘ R.fmap f ∘ pureT X ≡⟨ sym ℂ.isAssociative ⟩
|
||||
joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩
|
||||
joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
|
||||
joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
|
||||
𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩
|
||||
f ∎
|
||||
|
||||
|
|
@ -81,36 +81,36 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
where
|
||||
module R² = Functor F[ R ∘ R ]
|
||||
distrib3 : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
|
||||
→ R.func→ (a ∘ b ∘ c)
|
||||
≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
|
||||
→ R.fmap (a ∘ b ∘ c)
|
||||
≡ R.fmap a ∘ R.fmap b ∘ R.fmap c
|
||||
distrib3 {a = a} {b} {c} = begin
|
||||
R.func→ (a ∘ b ∘ c) ≡⟨ R.isDistributive ⟩
|
||||
R.func→ (a ∘ b) ∘ R.func→ c ≡⟨ cong (_∘ _) R.isDistributive ⟩
|
||||
R.func→ a ∘ R.func→ b ∘ R.func→ c ∎
|
||||
R.fmap (a ∘ b ∘ c) ≡⟨ R.isDistributive ⟩
|
||||
R.fmap (a ∘ b) ∘ R.fmap c ≡⟨ cong (_∘ _) R.isDistributive ⟩
|
||||
R.fmap a ∘ R.fmap b ∘ R.fmap c ∎
|
||||
aux = begin
|
||||
joinT Z ∘ R.func→ (joinT Z ∘ R.func→ g ∘ f)
|
||||
joinT Z ∘ R.fmap (joinT Z ∘ R.fmap g ∘ f)
|
||||
≡⟨ cong (λ φ → joinT Z ∘ φ) distrib3 ⟩
|
||||
joinT Z ∘ (R.func→ (joinT Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f)
|
||||
joinT Z ∘ (R.fmap (joinT Z) ∘ R.fmap (R.fmap g) ∘ R.fmap f)
|
||||
≡⟨⟩
|
||||
joinT Z ∘ (R.func→ (joinT Z) ∘ R².func→ g ∘ R.func→ f)
|
||||
joinT Z ∘ (R.fmap (joinT Z) ∘ R².fmap g ∘ R.fmap f)
|
||||
≡⟨ cong (_∘_ (joinT Z)) (sym ℂ.isAssociative) ⟩
|
||||
joinT Z ∘ (R.func→ (joinT Z) ∘ (R².func→ g ∘ R.func→ f))
|
||||
joinT Z ∘ (R.fmap (joinT Z) ∘ (R².fmap g ∘ R.fmap f))
|
||||
≡⟨ ℂ.isAssociative ⟩
|
||||
(joinT Z ∘ R.func→ (joinT Z)) ∘ (R².func→ g ∘ R.func→ f)
|
||||
≡⟨ cong (λ φ → φ ∘ (R².func→ g ∘ R.func→ f)) isAssociative ⟩
|
||||
(joinT Z ∘ joinT (R.func* Z)) ∘ (R².func→ g ∘ R.func→ f)
|
||||
(joinT Z ∘ R.fmap (joinT Z)) ∘ (R².fmap g ∘ R.fmap f)
|
||||
≡⟨ cong (λ φ → φ ∘ (R².fmap g ∘ R.fmap f)) isAssociative ⟩
|
||||
(joinT Z ∘ joinT (R.omap Z)) ∘ (R².fmap g ∘ R.fmap f)
|
||||
≡⟨ ℂ.isAssociative ⟩
|
||||
joinT Z ∘ joinT (R.func* Z) ∘ R².func→ g ∘ R.func→ f
|
||||
joinT Z ∘ joinT (R.omap Z) ∘ R².fmap g ∘ R.fmap f
|
||||
≡⟨⟩
|
||||
((joinT Z ∘ joinT (R.func* Z)) ∘ R².func→ g) ∘ R.func→ f
|
||||
≡⟨ cong (_∘ R.func→ f) (sym ℂ.isAssociative) ⟩
|
||||
(joinT Z ∘ (joinT (R.func* Z) ∘ R².func→ g)) ∘ R.func→ f
|
||||
≡⟨ cong (λ φ → φ ∘ R.func→ f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩
|
||||
(joinT Z ∘ (R.func→ g ∘ joinT Y)) ∘ R.func→ f
|
||||
≡⟨ cong (_∘ R.func→ f) ℂ.isAssociative ⟩
|
||||
joinT Z ∘ R.func→ g ∘ joinT Y ∘ R.func→ f
|
||||
((joinT Z ∘ joinT (R.omap Z)) ∘ R².fmap g) ∘ R.fmap f
|
||||
≡⟨ cong (_∘ R.fmap f) (sym ℂ.isAssociative) ⟩
|
||||
(joinT Z ∘ (joinT (R.omap Z) ∘ R².fmap g)) ∘ R.fmap f
|
||||
≡⟨ cong (λ φ → φ ∘ R.fmap f) (cong (_∘_ (joinT Z)) (joinN g)) ⟩
|
||||
(joinT Z ∘ (R.fmap g ∘ joinT Y)) ∘ R.fmap f
|
||||
≡⟨ cong (_∘ R.fmap f) ℂ.isAssociative ⟩
|
||||
joinT Z ∘ R.fmap g ∘ joinT Y ∘ R.fmap f
|
||||
≡⟨ sym (Category.isAssociative ℂ) ⟩
|
||||
joinT Z ∘ R.func→ g ∘ (joinT Y ∘ R.func→ f)
|
||||
joinT Z ∘ R.fmap g ∘ (joinT Y ∘ R.fmap f)
|
||||
∎
|
||||
|
||||
record Monad : Set ℓ where
|
||||
|
|
@ -235,8 +235,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
-- | This formulation gives rise to the following endo-functor.
|
||||
private
|
||||
rawR : RawFunctor ℂ ℂ
|
||||
RawFunctor.func* rawR = omap
|
||||
RawFunctor.func→ rawR = fmap
|
||||
RawFunctor.omap rawR = omap
|
||||
RawFunctor.fmap rawR = fmap
|
||||
|
||||
isFunctorR : IsFunctor ℂ ℂ rawR
|
||||
IsFunctor.isIdentity isFunctorR = begin
|
||||
|
|
@ -269,18 +269,18 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
pureT A = pure
|
||||
pureN : Natural R⁰ R pureT
|
||||
pureN {A} {B} f = begin
|
||||
pureT B ∘ R⁰.func→ f ≡⟨⟩
|
||||
pureT B ∘ R⁰.fmap f ≡⟨⟩
|
||||
pure ∘ f ≡⟨ sym (isNatural _) ⟩
|
||||
bind (pure ∘ f) ∘ pure ≡⟨⟩
|
||||
fmap f ∘ pure ≡⟨⟩
|
||||
R.func→ f ∘ pureT A ∎
|
||||
R.fmap f ∘ pureT A ∎
|
||||
joinT : Transformation R² R
|
||||
joinT C = join
|
||||
joinN : Natural R² R joinT
|
||||
joinN f = begin
|
||||
join ∘ R².func→ f ≡⟨⟩
|
||||
bind 𝟙 ∘ R².func→ f ≡⟨⟩
|
||||
R².func→ f >>> bind 𝟙 ≡⟨⟩
|
||||
join ∘ R².fmap f ≡⟨⟩
|
||||
bind 𝟙 ∘ R².fmap f ≡⟨⟩
|
||||
R².fmap f >>> bind 𝟙 ≡⟨⟩
|
||||
fmap (fmap f) >>> bind 𝟙 ≡⟨⟩
|
||||
fmap (bind (f >>> pure)) >>> bind 𝟙 ≡⟨⟩
|
||||
bind (bind (f >>> pure) >>> pure) >>> bind 𝟙
|
||||
|
|
@ -300,9 +300,9 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
≡⟨ sym (isDistributive _ _) ⟩
|
||||
bind 𝟙 >>> bind (f >>> pure) ≡⟨⟩
|
||||
bind 𝟙 >>> fmap f ≡⟨⟩
|
||||
bind 𝟙 >>> R.func→ f ≡⟨⟩
|
||||
R.func→ f ∘ bind 𝟙 ≡⟨⟩
|
||||
R.func→ f ∘ join ∎
|
||||
bind 𝟙 >>> R.fmap f ≡⟨⟩
|
||||
R.fmap f ∘ bind 𝟙 ≡⟨⟩
|
||||
R.fmap f ∘ join ∎
|
||||
|
||||
pureNT : NaturalTransformation R⁰ R
|
||||
proj₁ pureNT = pureT
|
||||
|
|
@ -396,7 +396,6 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
|||
private
|
||||
module ℂ = Category ℂ
|
||||
open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_)
|
||||
open Functor using (func* ; func→)
|
||||
module M = Monoidal ℂ
|
||||
module K = Kleisli ℂ
|
||||
|
||||
|
|
@ -434,19 +433,19 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
|||
|
||||
backIsMonad : M.IsMonad backRaw
|
||||
M.IsMonad.isAssociative backIsMonad {X} = begin
|
||||
joinT X ∘ R.func→ (joinT X) ≡⟨⟩
|
||||
joinT X ∘ R.fmap (joinT X) ≡⟨⟩
|
||||
join ∘ fmap (joinT X) ≡⟨⟩
|
||||
join ∘ fmap join ≡⟨ isNaturalForeign ⟩
|
||||
join ∘ join ≡⟨⟩
|
||||
joinT X ∘ joinT (R.func* X) ∎
|
||||
joinT X ∘ joinT (R.omap X) ∎
|
||||
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
|
||||
where
|
||||
inv-l = begin
|
||||
joinT X ∘ pureT (R.func* X) ≡⟨⟩
|
||||
joinT X ∘ pureT (R.omap X) ≡⟨⟩
|
||||
join ∘ pure ≡⟨ proj₁ isInverse ⟩
|
||||
𝟙 ∎
|
||||
inv-r = begin
|
||||
joinT X ∘ R.func→ (pureT X) ≡⟨⟩
|
||||
joinT X ∘ R.fmap (pureT X) ≡⟨⟩
|
||||
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
|
||||
𝟙 ∎
|
||||
|
||||
|
|
@ -526,8 +525,8 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
|||
)
|
||||
|
||||
rawEq : Functor.raw KM.R ≡ Functor.raw R
|
||||
RawFunctor.func* (rawEq i) = omapEq i
|
||||
RawFunctor.func→ (rawEq i) = fmapEq i
|
||||
RawFunctor.omap (rawEq i) = omapEq i
|
||||
RawFunctor.fmap (rawEq i) = fmapEq i
|
||||
|
||||
Req : M.RawMonad.R (backRaw (forth m)) ≡ R
|
||||
Req = Functor≡ rawEq
|
||||
|
|
@ -586,8 +585,8 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
|
||||
Rraw : RawFunctor ℂ ℂ
|
||||
Rraw = record
|
||||
{ func* = omap
|
||||
; func→ = fmap
|
||||
{ omap = omap
|
||||
; fmap = fmap
|
||||
}
|
||||
|
||||
field
|
||||
|
|
@ -663,7 +662,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
|||
|
||||
voe-2-3-1-fromMonad : (m : M.Monad) → voe-2-3-1 (M.Monad.Romap m) (λ {X} → M.Monad.pureT m X)
|
||||
voe-2-3-1-fromMonad m = record
|
||||
{ fmap = Functor.func→ R
|
||||
{ fmap = Functor.fmap R
|
||||
; RisFunctor = Functor.isFunctor R
|
||||
; pureN = pureN
|
||||
; join = λ {X} → joinT X
|
||||
|
|
|
|||
|
|
@ -46,13 +46,13 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
|
|||
module G = Functor G
|
||||
-- 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.omap C , G.omap C ]
|
||||
|
||||
Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd'))
|
||||
Natural θ
|
||||
= {A B : Object ℂ}
|
||||
→ (f : ℂ [ A , B ])
|
||||
→ 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ]
|
||||
→ 𝔻 [ θ B ∘ F.fmap f ] ≡ 𝔻 [ G.fmap f ∘ θ A ]
|
||||
|
||||
NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd')
|
||||
NaturalTransformation = Σ Transformation Natural
|
||||
|
|
@ -78,7 +78,7 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
|
|||
𝔻 [ F→ f ∘ identityTrans F A ] ∎
|
||||
where
|
||||
module F = Functor F
|
||||
F→ = F.func→
|
||||
F→ = F.fmap
|
||||
|
||||
identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F
|
||||
identity F = identityTrans F , identityNatural F
|
||||
|
|
@ -94,14 +94,14 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level}
|
|||
NT[_∘_] : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H
|
||||
proj₁ NT[ (θ , _) ∘ (η , _) ] = T[ θ ∘ η ]
|
||||
proj₂ NT[ (θ , θNat) ∘ (η , ηNat) ] {A} {B} f = begin
|
||||
𝔻 [ T[ θ ∘ η ] B ∘ F.func→ f ] ≡⟨⟩
|
||||
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym 𝔻.isAssociative ⟩
|
||||
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
|
||||
𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
|
||||
𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
|
||||
𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
|
||||
𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
|
||||
𝔻 [ H.func→ f ∘ T[ θ ∘ η ] A ] ∎
|
||||
𝔻 [ T[ θ ∘ η ] B ∘ F.fmap f ] ≡⟨⟩
|
||||
𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.fmap f ] ≡⟨ sym 𝔻.isAssociative ⟩
|
||||
𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.fmap f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩
|
||||
𝔻 [ θ B ∘ 𝔻 [ G.fmap f ∘ η A ] ] ≡⟨ 𝔻.isAssociative ⟩
|
||||
𝔻 [ 𝔻 [ θ B ∘ G.fmap f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩
|
||||
𝔻 [ 𝔻 [ H.fmap f ∘ θ A ] ∘ η A ] ≡⟨ sym 𝔻.isAssociative ⟩
|
||||
𝔻 [ H.fmap f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩
|
||||
𝔻 [ H.fmap f ∘ T[ θ ∘ η ] A ] ∎
|
||||
|
||||
module _ {F G : Functor ℂ 𝔻} where
|
||||
transformationIsSet : isSet (Transformation F G)
|
||||
|
|
|
|||
|
|
@ -42,9 +42,9 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where
|
|||
fmapNT = fmap , fmapNatural
|
||||
|
||||
rawYoneda : RawFunctor ℂ Fun
|
||||
RawFunctor.func* rawYoneda = prshf
|
||||
RawFunctor.func→ rawYoneda = fmapNT
|
||||
open RawFunctor rawYoneda
|
||||
RawFunctor.omap rawYoneda = prshf
|
||||
RawFunctor.fmap rawYoneda = fmapNT
|
||||
open RawFunctor rawYoneda hiding (fmap)
|
||||
|
||||
isIdentity : IsIdentity
|
||||
isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq
|
||||
|
|
|
|||
Loading…
Reference in a new issue