From 5ad506a09f842e75daad93ad03642b6862466633 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 8 Mar 2018 11:03:56 +0100 Subject: [PATCH] Rename func* and func-> to omap and fmap respectively --- src/Cat/Categories/Cat.agda | 92 ++++++++++---------- src/Cat/Categories/CwF.agda | 18 ++-- src/Cat/Categories/Sets.agda | 8 +- src/Cat/Category/Functor.agda | 46 +++++----- src/Cat/Category/Monad.agda | 93 ++++++++++----------- src/Cat/Category/NaturalTransformation.agda | 22 ++--- src/Cat/Category/Yoneda.agda | 6 +- 7 files changed, 142 insertions(+), 143 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 121d83d..5e9ba24 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -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} diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda index 4b9ce32..ea369ef 100644 --- a/src/Cat/Categories/CwF.agda +++ b/src/Cat/Categories/CwF.agda @@ -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 : {!!}) → {!!} diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index ac6bd72..6f9ade2 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -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 diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 6724dee..fc23c2e 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -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 diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 6ce46bb..f020383 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -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 diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 525933a..dea2e50 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -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) diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 88b0bbd..0e19c04 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -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