Created
September 12, 2022 19:01
-
-
Save Lysxia/c400ccee1e1c437e37682f39df2f6946 to your computer and use it in GitHub Desktop.
Traversables as Graded functors
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Traversables as Graded functors | |
| -- Graded functors as functors that commute with grading | |
| -- | |
| -- Graded endofunctors on KleisliApp are Traversables | |
| -- | |
| -- Laws omitted. | |
| module T where | |
| open import Level | |
| open import Function.Base as Function using (case_of_) | |
| open import Data.Unit.Base using (⊤; tt) | |
| open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym) | |
| open import Data.Product using (_×_; _,_; proj₁; proj₂; Σ; ∃; Σ-syntax; ∃-syntax) | |
| variable | |
| ℓ : Level | |
| -- * Categories and functors | |
| record Cat ℓ : Set (suc ℓ) where | |
| field | |
| obj : Set ℓ | |
| _⇒_ : obj -> obj -> Set ℓ | |
| id : {A : obj} → A ⇒ A | |
| _∙_ : {A B C : obj} → B ⇒ C → A ⇒ B → A ⇒ C | |
| -- laws (...) | |
| record Functor (ℂ 𝔻 : Cat ℓ) : Set ℓ where | |
| open Cat ℂ renaming (obj to C; _⇒_ to _⇒ᶜ_) | |
| open Cat 𝔻 renaming (obj to D; _⇒_ to _⇒ᴰ_) | |
| field | |
| omap : C -> D | |
| fmap : {A B : C} → A ⇒ᶜ B → omap A ⇒ᴰ omap B | |
| -- laws (...) | |
| _∘_ : {ℂ 𝔻 𝔼 : Cat ℓ} → Functor 𝔻 𝔼 → Functor ℂ 𝔻 → Functor ℂ 𝔼 | |
| 𝔾 ∘ 𝔽 = record | |
| { omap = G Function.∘ F | |
| ; fmap = Gmap Function.∘ Fmap } | |
| where | |
| open Functor 𝔽 renaming (omap to F; fmap to Fmap) | |
| open Functor 𝔾 renaming (omap to G; fmap to Gmap) | |
| -- * Graded categories and functors | |
| -- Graded categories: categories indexed by a grade | |
| record Graded (𝔾 : Cat ℓ) : Set (suc ℓ) where | |
| field | |
| ℂ : Cat ℓ | |
| grade : Functor ℂ 𝔾 | |
| -- Graded functors: functors that commute with grade | |
| record GradedFunctor {𝔾 : Cat ℓ} (𝓒 𝓓 : Graded 𝔾) : Set ℓ where | |
| open Graded 𝓒 renaming (grade to 𝓒-grade) | |
| open Graded 𝓓 renaming (ℂ to 𝔻; grade to 𝓓-grade) | |
| field | |
| 𝔽 : Functor ℂ 𝔻 | |
| grade : 𝓓-grade ∘ 𝔽 ≡ 𝓒-grade | |
| -- * From graded functors to traversables | |
| -- KleisliApp-G : Graded category of applicative maps (with homsets A ⇒ B = ∃[ F ] Applicative F × (A -> F B)) | |
| -- Traversable : Traversable functors | |
| -- EndoKA-Traversable : Graded endofunctors on KleisliApp-G are Traversables | |
| -- ** Applicative functors | |
| record Applicative (F : Set → Set) : Set₁ where | |
| field | |
| pure : {A : Set} → A → F A | |
| ap : {A B : Set} → F (A → B) → F A → F B | |
| open Applicative | |
| Identity : Set → Set | |
| Identity A = A | |
| Applicative-Identity : Applicative Identity | |
| Applicative-Identity = record | |
| { pure = λ x → x | |
| ; ap = λ f x → f x | |
| } | |
| Applicative-∘ : ∀ {F G} → Applicative F → Applicative G → Applicative (F Function.∘ G) | |
| Applicative-∘ 𝔽 𝔾 = record | |
| { pure = λ x → pure 𝔽 (pure 𝔾 x) | |
| ; ap = λ f → ap 𝔽 (ap 𝔽 (pure 𝔽 (ap 𝔾)) f) | |
| } | |
| -- ** The graded cateogory KleisliApp | |
| KleisliApp : Cat (suc zero) | |
| KleisliApp = record | |
| { obj = Set | |
| ; _⇒_ = λ A B → ∃[ F ] Applicative F × (A → F B) | |
| ; id = _ , Applicative-Identity , λ x → x | |
| ; _∙_ = λ{ (_ , 𝔾 , g) (_ , 𝔽 , f) → (_ , Applicative-∘ 𝔽 𝔾 , λ x → ap 𝔽 (pure 𝔽 g) (f x)) } | |
| } | |
| Endo : Cat (suc zero) | |
| Endo = record | |
| { obj = Lift (suc zero) ⊤ | |
| ; _⇒_ = λ _ _ → ∃[ F ] Applicative F | |
| ; id = _ , Applicative-Identity | |
| ; _∙_ = λ{ (_ , 𝔾) (_ , 𝔽) → _ , Applicative-∘ 𝔾 𝔽 } } | |
| KleisliApp-grade : Functor KleisliApp Endo | |
| KleisliApp-grade = record | |
| { omap = λ _ → lift tt | |
| ; fmap = λ{ (_ , 𝔽 , _) → _ , 𝔽 } | |
| } | |
| KleisliApp-G : Graded Endo | |
| KleisliApp-G = record | |
| { ℂ = KleisliApp | |
| ; grade = KleisliApp-grade | |
| } | |
| -- ** Traversables | |
| record Traversable : Set₁ where | |
| field | |
| T : Set → Set | |
| traverse : ∀ {F} → Applicative F → ∀ {A B} → (A → F B) → T A → F (T B) | |
| -- ** Graded endofunctors on KleisliApp are Traversables | |
| data _≡≡_ {ℓ} {A : Set ℓ} (a : A) : ∀ {B : Set ℓ} → B → Set where | |
| refl : a ≡≡ a | |
| hcong : ∀ {ℓ} {A : Set ℓ} {B : A → Set ℓ} (f : (a : A) → B a) → ∀ {a b : A} → a ≡ b → f a ≡≡ f b | |
| hcong _ refl = refl | |
| module _ {ℓ} {𝔾 : Cat ℓ} {𝓒 𝓓 : Graded 𝔾} (𝓕 : GradedFunctor 𝓒 𝓓) where | |
| open Graded 𝓒 renaming (grade to 𝓒-grade) | |
| open Graded 𝓓 using () renaming (grade to 𝓓-grade) | |
| open GradedFunctor 𝓕 renaming (grade to 𝓣-grade) | |
| open Cat ℂ | |
| grade-eq : | |
| ∀ {A B} (f : A ⇒ B) → | |
| Functor.fmap 𝓒-grade f ≡≡ Functor.fmap 𝓓-grade (Functor.fmap 𝔽 f) | |
| grade-eq f = hcong (λ (GF : Functor ℂ 𝔾) → Functor.fmap GF f) (sym 𝓣-grade) | |
| module _ (𝓣 : GradedFunctor KleisliApp-G KleisliApp-G) where | |
| open GradedFunctor 𝓣 renaming (𝔽 to 𝕋; grade to 𝓣-grade) | |
| open Functor 𝕋 renaming (omap to T; fmap to Tmap) | |
| EndoKA-traverse : ∀ {F} → Applicative F → ∀ {A B} → (A → F B) → T A → F (T B) | |
| EndoKA-traverse 𝔽 f with Functor.fmap 𝕋 (_ , 𝔽 , f) | grade-eq 𝓣 (_ , 𝔽 , f) | |
| ... | _ , _ , g | refl = g | |
| EndoKA-Traversable : Traversable | |
| EndoKA-Traversable = record | |
| { T = Functor.omap 𝕋 | |
| ; traverse = EndoKA-traverse | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment