From aa645fb11e9edab11bb925d682f843d8f138bbe7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 12 Mar 2018 14:04:10 +0100 Subject: [PATCH] Move voevodsky's construction to own module --- src/Cat.agda | 1 + src/Cat/Category/Monad.agda | 208 ------------------------ src/Cat/Category/Monad/Voevodsky.agda | 221 ++++++++++++++++++++++++++ 3 files changed, 222 insertions(+), 208 deletions(-) create mode 100644 src/Cat/Category/Monad/Voevodsky.agda diff --git a/src/Cat.agda b/src/Cat.agda index 478b725..86e6879 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -9,6 +9,7 @@ open import Cat.Category.CartesianClosed open import Cat.Category.NaturalTransformation open import Cat.Category.Yoneda open import Cat.Category.Monad +open import Cat.Category.Monad.Voevodsky open import Cat.Categories.Sets open import Cat.Categories.Cat diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 5a8d4c1..257721e 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -389,9 +389,6 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Monad.isMonad (Monad≡ i) = eqIsMonad i -- | The monoidal- and kleisli presentation of monads are equivalent. --- --- This is *not* problem 2.3 in [voe]. --- This is problem 2.3 in [voe]. module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where private module ℂ = Category ℂ @@ -565,208 +562,3 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where Monoidal≃Kleisli : M.Monad ≃ K.Monad Monoidal≃Kleisli = forth , eqv - -module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where - private - ℓ = ℓa ⊔ ℓb - module ℂ = Category ℂ - open ℂ using (Object ; Arrow ; _∘_) - open NaturalTransformation ℂ ℂ - module M = Monoidal ℂ - module K = Kleisli ℂ - - module voe-2-3 (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where - record voe-2-3-1 : Set ℓ where - open M - - field - fmap : Fmap ℂ ℂ omap - join : {A : Object} → ℂ [ omap (omap A) , omap A ] - - Rraw : RawFunctor ℂ ℂ - Rraw = record - { omap = omap - ; fmap = fmap - } - - field - RisFunctor : IsFunctor ℂ ℂ Rraw - - R : EndoFunctor ℂ - R = record - { raw = Rraw - ; isFunctor = RisFunctor - } - - pureT : (X : Object) → Arrow X (omap X) - pureT X = pure {X} - - field - pureN : Natural F.identity R pureT - - pureNT : NaturalTransformation F.identity R - pureNT = pureT , pureN - - joinT : (A : Object) → ℂ [ omap (omap A) , omap A ] - joinT A = join {A} - - field - joinN : Natural F[ R ∘ R ] R joinT - - joinNT : NaturalTransformation F[ R ∘ R ] R - joinNT = joinT , joinN - - rawMnd : RawMonad - rawMnd = record - { R = R - ; pureNT = pureNT - ; joinNT = joinNT - } - - field - isMnd : IsMonad rawMnd - - toMonad : Monad - toMonad = record - { raw = rawMnd - ; isMonad = isMnd - } - - record voe-2-3-2 : Set ℓ where - open K - - field - bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ] - - rawMnd : RawMonad - rawMnd = record - { omap = omap - ; pure = pure - ; bind = bind - } - - field - isMnd : IsMonad rawMnd - - toMonad : Monad - toMonad = record - { raw = rawMnd - ; isMonad = isMnd - } - -module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where - private - module M = Monoidal ℂ - module K = Kleisli ℂ - open voe-2-3 ℂ - - 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.fmap R - ; RisFunctor = Functor.isFunctor R - ; pureN = pureN - ; join = λ {X} → joinT X - ; joinN = joinN - ; isMnd = M.Monad.isMonad m - } - where - raw = M.Monad.raw m - R = M.RawMonad.R raw - pureT = M.RawMonad.pureT raw - pureN = M.RawMonad.pureN raw - joinT = M.RawMonad.joinT raw - joinN = M.RawMonad.joinN raw - - voe-2-3-2-fromMonad : (m : K.Monad) → voe-2-3-2 (K.Monad.omap m) (K.Monad.pure m) - voe-2-3-2-fromMonad m = record - { bind = K.Monad.bind m - ; isMnd = K.Monad.isMonad m - } - -module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where - private - ℓ = ℓa ⊔ ℓb - module ℂ = Category ℂ - open ℂ using (Object ; Arrow) - open NaturalTransformation ℂ ℂ - module M = Monoidal ℂ - module K = Kleisli ℂ - open import Function using (_∘_ ; _$_) - - module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where - open voe-2-3 ℂ - private - Monoidal→Kleisli : M.Monad → K.Monad - Monoidal→Kleisli = proj₁ Monoidal≃Kleisli - - Kleisli→Monoidal : K.Monad → M.Monad - Kleisli→Monoidal = inverse Monoidal≃Kleisli - - forth : voe-2-3-1 omap pure → voe-2-3-2 omap pure - forth = voe-2-3-2-fromMonad ∘ Monoidal→Kleisli ∘ voe-2-3.voe-2-3-1.toMonad - - back : voe-2-3-2 omap pure → voe-2-3-1 omap pure - back = voe-2-3-1-fromMonad ∘ Kleisli→Monoidal ∘ voe-2-3.voe-2-3-2.toMonad - - forthEq : ∀ m → _ ≡ _ - forthEq m = begin - (forth ∘ back) m ≡⟨⟩ - -- In full gory detail: - ( voe-2-3-2-fromMonad - ∘ Monoidal→Kleisli - ∘ voe-2-3.voe-2-3-1.toMonad - ∘ voe-2-3-1-fromMonad - ∘ Kleisli→Monoidal - ∘ voe-2-3.voe-2-3-2.toMonad - ) m ≡⟨⟩ -- fromMonad and toMonad are inverses - ( voe-2-3-2-fromMonad - ∘ Monoidal→Kleisli - ∘ Kleisli→Monoidal - ∘ voe-2-3.voe-2-3-2.toMonad - ) m ≡⟨ u ⟩ - -- Monoidal→Kleisli and Kleisli→Monoidal are inverses - -- I should be able to prove this using congruence and `lem` below. - ( voe-2-3-2-fromMonad - ∘ voe-2-3.voe-2-3-2.toMonad - ) m ≡⟨⟩ - ( voe-2-3-2-fromMonad - ∘ voe-2-3.voe-2-3-2.toMonad - ) m ≡⟨⟩ -- fromMonad and toMonad are inverses - m ∎ - where - lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id - lem = {!!} -- verso-recto Monoidal≃Kleisli - t : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _} - → a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b ≡ a ∘ b - t {a = a} {b} = cong (λ φ → a ∘ φ ∘ b) lem - u : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _} - → {m : _} → (a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b) m ≡ (a ∘ b) m - u {m = m} = cong (λ φ → φ m) t - - backEq : ∀ m → (back ∘ forth) m ≡ m - backEq m = begin - (back ∘ forth) m ≡⟨⟩ - ( voe-2-3-1-fromMonad - ∘ Kleisli→Monoidal - ∘ voe-2-3.voe-2-3-2.toMonad - ∘ voe-2-3-2-fromMonad - ∘ Monoidal→Kleisli - ∘ voe-2-3.voe-2-3-1.toMonad - ) m ≡⟨⟩ -- fromMonad and toMonad are inverses - ( voe-2-3-1-fromMonad - ∘ Kleisli→Monoidal - ∘ Monoidal→Kleisli - ∘ voe-2-3.voe-2-3-1.toMonad - ) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses - ( voe-2-3-1-fromMonad - ∘ voe-2-3.voe-2-3-1.toMonad - ) m ≡⟨⟩ -- fromMonad and toMonad are inverses - m ∎ - where - t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli) - - voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth - voe-isEquiv = gradLemma forth back forthEq backEq - - equiv-2-3 : voe-2-3-1 omap pure ≃ voe-2-3-2 omap pure - equiv-2-3 = forth , voe-isEquiv diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda new file mode 100644 index 0000000..02898a1 --- /dev/null +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -0,0 +1,221 @@ +{-# OPTIONS --cubical --allow-unsolved-metas #-} +module Cat.Category.Monad.Voevodsky where + +open import Agda.Primitive + +open import Data.Product + +open import Cubical +open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) +open import Cubical.GradLemma using (gradLemma) + +open import Cat.Category +open import Cat.Category.Functor as F +open import Cat.Category.NaturalTransformation +open import Cat.Category.Monad +open import Cat.Categories.Fun + +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + private + ℓ = ℓa ⊔ ℓb + module ℂ = Category ℂ + open ℂ using (Object ; Arrow ; _∘_) + open NaturalTransformation ℂ ℂ + module M = Monoidal ℂ + module K = Kleisli ℂ + + module voe-2-3 (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where + record voe-2-3-1 : Set ℓ where + open M + + field + fmap : Fmap ℂ ℂ omap + join : {A : Object} → ℂ [ omap (omap A) , omap A ] + + Rraw : RawFunctor ℂ ℂ + Rraw = record + { omap = omap + ; fmap = fmap + } + + field + RisFunctor : IsFunctor ℂ ℂ Rraw + + R : EndoFunctor ℂ + R = record + { raw = Rraw + ; isFunctor = RisFunctor + } + + pureT : (X : Object) → Arrow X (omap X) + pureT X = pure {X} + + field + pureN : Natural F.identity R pureT + + pureNT : NaturalTransformation F.identity R + pureNT = pureT , pureN + + joinT : (A : Object) → ℂ [ omap (omap A) , omap A ] + joinT A = join {A} + + field + joinN : Natural F[ R ∘ R ] R joinT + + joinNT : NaturalTransformation F[ R ∘ R ] R + joinNT = joinT , joinN + + rawMnd : RawMonad + rawMnd = record + { R = R + ; pureNT = pureNT + ; joinNT = joinNT + } + + field + isMnd : IsMonad rawMnd + + toMonad : Monad + toMonad = record + { raw = rawMnd + ; isMonad = isMnd + } + + record voe-2-3-2 : Set ℓ where + open K + + field + bind : {X Y : Object} → ℂ [ X , omap Y ] → ℂ [ omap X , omap Y ] + + rawMnd : RawMonad + rawMnd = record + { omap = omap + ; pure = pure + ; bind = bind + } + + field + isMnd : IsMonad rawMnd + + toMonad : Monad + toMonad = record + { raw = rawMnd + ; isMonad = isMnd + } + +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where + private + module M = Monoidal ℂ + module K = Kleisli ℂ + open voe-2-3 ℂ + + 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.fmap R + ; RisFunctor = Functor.isFunctor R + ; pureN = pureN + ; join = λ {X} → joinT X + ; joinN = joinN + ; isMnd = M.Monad.isMonad m + } + where + raw = M.Monad.raw m + R = M.RawMonad.R raw + pureT = M.RawMonad.pureT raw + pureN = M.RawMonad.pureN raw + joinT = M.RawMonad.joinT raw + joinN = M.RawMonad.joinN raw + + voe-2-3-2-fromMonad : (m : K.Monad) → voe-2-3-2 (K.Monad.omap m) (K.Monad.pure m) + voe-2-3-2-fromMonad m = record + { bind = K.Monad.bind m + ; isMnd = K.Monad.isMonad m + } + +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where + private + ℓ = ℓa ⊔ ℓb + module ℂ = Category ℂ + open ℂ using (Object ; Arrow) + open NaturalTransformation ℂ ℂ + module M = Monoidal ℂ + module K = Kleisli ℂ + open import Function using (_∘_ ; _$_) + + module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where + open voe-2-3 ℂ + private + Monoidal→Kleisli : M.Monad → K.Monad + Monoidal→Kleisli = proj₁ Monoidal≃Kleisli + + Kleisli→Monoidal : K.Monad → M.Monad + Kleisli→Monoidal = inverse Monoidal≃Kleisli + + forth : voe-2-3-1 omap pure → voe-2-3-2 omap pure + forth = voe-2-3-2-fromMonad ∘ Monoidal→Kleisli ∘ voe-2-3.voe-2-3-1.toMonad + + back : voe-2-3-2 omap pure → voe-2-3-1 omap pure + back = voe-2-3-1-fromMonad ∘ Kleisli→Monoidal ∘ voe-2-3.voe-2-3-2.toMonad + + forthEq : ∀ m → _ ≡ _ + forthEq m = begin + (forth ∘ back) m ≡⟨⟩ + -- In full gory detail: + ( voe-2-3-2-fromMonad + ∘ Monoidal→Kleisli + ∘ voe-2-3.voe-2-3-1.toMonad + ∘ voe-2-3-1-fromMonad + ∘ Kleisli→Monoidal + ∘ voe-2-3.voe-2-3-2.toMonad + ) m ≡⟨⟩ -- fromMonad and toMonad are inverses + ( voe-2-3-2-fromMonad + ∘ Monoidal→Kleisli + ∘ Kleisli→Monoidal + ∘ voe-2-3.voe-2-3-2.toMonad + ) m ≡⟨ u ⟩ + -- Monoidal→Kleisli and Kleisli→Monoidal are inverses + -- I should be able to prove this using congruence and `lem` below. + ( voe-2-3-2-fromMonad + ∘ voe-2-3.voe-2-3-2.toMonad + ) m ≡⟨⟩ + ( voe-2-3-2-fromMonad + ∘ voe-2-3.voe-2-3-2.toMonad + ) m ≡⟨⟩ -- fromMonad and toMonad are inverses + m ∎ + where + lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id + lem = {!!} -- verso-recto Monoidal≃Kleisli + t : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _} + → a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b ≡ a ∘ b + t {a = a} {b} = cong (λ φ → a ∘ φ ∘ b) lem + u : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _} + → {m : _} → (a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b) m ≡ (a ∘ b) m + u {m = m} = cong (λ φ → φ m) t + + backEq : ∀ m → (back ∘ forth) m ≡ m + backEq m = begin + (back ∘ forth) m ≡⟨⟩ + ( voe-2-3-1-fromMonad + ∘ Kleisli→Monoidal + ∘ voe-2-3.voe-2-3-2.toMonad + ∘ voe-2-3-2-fromMonad + ∘ Monoidal→Kleisli + ∘ voe-2-3.voe-2-3-1.toMonad + ) m ≡⟨⟩ -- fromMonad and toMonad are inverses + ( voe-2-3-1-fromMonad + ∘ Kleisli→Monoidal + ∘ Monoidal→Kleisli + ∘ voe-2-3.voe-2-3-1.toMonad + ) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses + ( voe-2-3-1-fromMonad + ∘ voe-2-3.voe-2-3-1.toMonad + ) m ≡⟨⟩ -- fromMonad and toMonad are inverses + m ∎ + where + t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli) + + voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth + voe-isEquiv = gradLemma forth back forthEq backEq + + equiv-2-3 : voe-2-3-1 omap pure ≃ voe-2-3-2 omap pure + equiv-2-3 = forth , voe-isEquiv