Move voevodsky's construction to own module
This commit is contained in:
parent
c0cf6789cd
commit
aa645fb11e
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
221
src/Cat/Category/Monad/Voevodsky.agda
Normal file
221
src/Cat/Category/Monad/Voevodsky.agda
Normal file
|
|
@ -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
|
||||
Loading…
Reference in a new issue