Traversables as Graded functors

T.agda

-- 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
    }