[WIP] Proving other fusion law
Also set up framework for equality principle for monads
This commit is contained in:
parent
a6b01929f0
commit
4c298855e0
|
|
@ -61,12 +61,21 @@ module Monoidal {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
isMonad : IsMonad raw
|
isMonad : IsMonad raw
|
||||||
open IsMonad isMonad public
|
open IsMonad isMonad public
|
||||||
|
|
||||||
|
postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
|
||||||
|
Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
|
||||||
|
Monad.raw (Monad≡ eq i) = eq i
|
||||||
|
Monad.isMonad (Monad≡ {m} {n} eq i) = res i
|
||||||
|
where
|
||||||
|
-- TODO: PathJ nightmare + `propIsMonad`.
|
||||||
|
res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
|
||||||
|
res = {!!}
|
||||||
|
|
||||||
-- "A monad in the Kleisli form" [voe]
|
-- "A monad in the Kleisli form" [voe]
|
||||||
module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
private
|
private
|
||||||
ℓ = ℓa ⊔ ℓb
|
ℓ = ℓa ⊔ ℓb
|
||||||
|
|
||||||
open Category ℂ hiding (IsIdentity)
|
open Category ℂ using (Arrow ; 𝟙 ; Object ; _∘_)
|
||||||
record RawMonad : Set ℓ where
|
record RawMonad : Set ℓ where
|
||||||
field
|
field
|
||||||
RR : Object → Object
|
RR : Object → Object
|
||||||
|
|
@ -87,6 +96,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
--
|
--
|
||||||
pure : {X : Object} → ℂ [ X , RR X ]
|
pure : {X : Object} → ℂ [ X , RR X ]
|
||||||
pure = ζ
|
pure = ζ
|
||||||
|
fmap : ∀ {A B} → ℂ [ A , B ] → ℂ [ RR A , RR B ]
|
||||||
|
fmap f = rr (ζ ∘ f)
|
||||||
-- Why is (>>=) not implementable?
|
-- Why is (>>=) not implementable?
|
||||||
--
|
--
|
||||||
-- (>>=) : m a -> (a -> m b) -> m b
|
-- (>>=) : m a -> (a -> m b) -> m b
|
||||||
|
|
@ -101,25 +112,8 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
→ rr f ∘ ζ ≡ f
|
→ rr f ∘ ζ ≡ f
|
||||||
IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
|
IsDistributive = {X Y Z : Object} (g : ℂ [ Y , RR Z ]) (f : ℂ [ X , RR Y ])
|
||||||
→ rr g ∘ rr f ≡ rr (rr g ∘ f)
|
→ rr g ∘ rr f ≡ rr (rr g ∘ f)
|
||||||
-- I assume `Fusion` is admissable - it certainly looks more like the
|
Fusion = {X Y Z : Object} {g : ℂ [ Y , Z ]} {f : ℂ [ X , Y ]}
|
||||||
-- distributive law for monads I know from Haskell.
|
→ fmap (g ∘ f) ≡ fmap g ∘ fmap f
|
||||||
Fusion = {X Y Z : Object} (g : ℂ [ Y , Z ]) (f : ℂ [ X , Y ])
|
|
||||||
→ rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
|
|
||||||
-- NatDist2Fus : IsNatural → IsDistributive → Fusion
|
|
||||||
-- NatDist2Fus isNatural isDistributive g f =
|
|
||||||
-- let
|
|
||||||
-- ζf = ζ ∘ f
|
|
||||||
-- ζg = ζ ∘ g
|
|
||||||
-- Nζf : rr (ζ ∘ f) ∘ ζ ≡ ζ ∘ f
|
|
||||||
-- Nζf = isNatural ζf
|
|
||||||
-- Nζg : rr (ζ ∘ g) ∘ ζ ≡ ζ ∘ g
|
|
||||||
-- Nζg = isNatural ζg
|
|
||||||
-- ζgf = ζ ∘ g ∘ f
|
|
||||||
-- Nζgf : rr (ζ ∘ g ∘ f) ∘ ζ ≡ ζ ∘ g ∘ f
|
|
||||||
-- Nζgf = isNatural ζgf
|
|
||||||
-- res : rr (ζ ∘ g ∘ f) ≡ rr (ζ ∘ g) ∘ rr (ζ ∘ f)
|
|
||||||
-- res = {!!}
|
|
||||||
-- in res
|
|
||||||
|
|
||||||
record IsMonad (raw : RawMonad) : Set ℓ where
|
record IsMonad (raw : RawMonad) : Set ℓ where
|
||||||
open RawMonad raw public
|
open RawMonad raw public
|
||||||
|
|
@ -127,6 +121,16 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
isIdentity : IsIdentity
|
isIdentity : IsIdentity
|
||||||
isNatural : IsNatural
|
isNatural : IsNatural
|
||||||
isDistributive : IsDistributive
|
isDistributive : IsDistributive
|
||||||
|
fusion : Fusion
|
||||||
|
fusion {g = g} {f} = begin
|
||||||
|
fmap (g ∘ f) ≡⟨⟩
|
||||||
|
rr (ζ ∘ (g ∘ f)) ≡⟨ {!!} ⟩
|
||||||
|
rr (rr (ζ ∘ g) ∘ (ζ ∘ f)) ≡⟨ sym lem ⟩
|
||||||
|
rr (ζ ∘ g) ∘ rr (ζ ∘ f) ≡⟨⟩
|
||||||
|
fmap g ∘ fmap f ∎
|
||||||
|
where
|
||||||
|
lem : rr (ζ ∘ g) ∘ rr (ζ ∘ f) ≡ rr (rr (ζ ∘ g) ∘ (ζ ∘ f))
|
||||||
|
lem = isDistributive (ζ ∘ g) (ζ ∘ f)
|
||||||
|
|
||||||
record Monad : Set ℓ where
|
record Monad : Set ℓ where
|
||||||
field
|
field
|
||||||
|
|
@ -134,6 +138,15 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
isMonad : IsMonad raw
|
isMonad : IsMonad raw
|
||||||
open IsMonad isMonad public
|
open IsMonad isMonad public
|
||||||
|
|
||||||
|
postulate propIsMonad : ∀ {raw} → isProp (IsMonad raw)
|
||||||
|
Monad≡ : {m n : Monad} → Monad.raw m ≡ Monad.raw n → m ≡ n
|
||||||
|
Monad.raw (Monad≡ eq i) = eq i
|
||||||
|
Monad.isMonad (Monad≡ {m} {n} eq i) = res i
|
||||||
|
where
|
||||||
|
-- TODO: PathJ nightmare + `propIsMonad`.
|
||||||
|
res : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
|
||||||
|
res = {!!}
|
||||||
|
|
||||||
-- Problem 2.3
|
-- Problem 2.3
|
||||||
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
private
|
private
|
||||||
|
|
@ -163,69 +176,70 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
Kraw.rr forthRaw = rr
|
Kraw.rr forthRaw = rr
|
||||||
|
|
||||||
module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
|
module _ {raw : M.RawMonad} (m : M.IsMonad raw) where
|
||||||
open M.IsMonad m
|
private
|
||||||
open K.RawMonad (forthRaw raw)
|
open M.IsMonad m
|
||||||
module Kis = K.IsMonad
|
open K.RawMonad (forthRaw raw)
|
||||||
|
module Kis = K.IsMonad
|
||||||
|
|
||||||
isIdentity : IsIdentity
|
isIdentity : IsIdentity
|
||||||
isIdentity {X} = begin
|
isIdentity {X} = begin
|
||||||
rr ζ ≡⟨⟩
|
rr ζ ≡⟨⟩
|
||||||
rr (η X) ≡⟨⟩
|
rr (η X) ≡⟨⟩
|
||||||
μ X ∘ func→ R (η X) ≡⟨ proj₂ isInverse ⟩
|
μ X ∘ func→ R (η X) ≡⟨ proj₂ isInverse ⟩
|
||||||
𝟙 ∎
|
𝟙 ∎
|
||||||
|
|
||||||
module R = Functor R
|
module R = Functor R
|
||||||
isNatural : IsNatural
|
isNatural : IsNatural
|
||||||
isNatural {X} {Y} f = begin
|
isNatural {X} {Y} f = begin
|
||||||
rr f ∘ ζ ≡⟨⟩
|
rr f ∘ ζ ≡⟨⟩
|
||||||
rr f ∘ η X ≡⟨⟩
|
rr f ∘ η X ≡⟨⟩
|
||||||
μ Y ∘ R.func→ f ∘ η X ≡⟨ sym ℂ.isAssociative ⟩
|
μ Y ∘ R.func→ f ∘ η X ≡⟨ sym ℂ.isAssociative ⟩
|
||||||
μ Y ∘ (R.func→ f ∘ η X) ≡⟨ cong (λ φ → μ Y ∘ φ) (sym (ηN f)) ⟩
|
μ Y ∘ (R.func→ f ∘ η X) ≡⟨ cong (λ φ → μ Y ∘ φ) (sym (ηN f)) ⟩
|
||||||
μ Y ∘ (η (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
|
μ Y ∘ (η (R.func* Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩
|
||||||
μ Y ∘ η (R.func* Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
|
μ Y ∘ η (R.func* Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩
|
||||||
𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩
|
𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩
|
||||||
f ∎
|
f ∎
|
||||||
where
|
where
|
||||||
open NaturalTransformation
|
open NaturalTransformation
|
||||||
module ℂ = Category ℂ
|
module ℂ = Category ℂ
|
||||||
ηN : Natural ℂ ℂ F.identity R η
|
ηN : Natural ℂ ℂ F.identity R η
|
||||||
ηN = proj₂ ηNat
|
ηN = proj₂ ηNat
|
||||||
|
|
||||||
isDistributive : IsDistributive
|
isDistributive : IsDistributive
|
||||||
isDistributive {X} {Y} {Z} g f = begin
|
isDistributive {X} {Y} {Z} g f = begin
|
||||||
rr g ∘ rr f ≡⟨⟩
|
rr g ∘ rr f ≡⟨⟩
|
||||||
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ sym lem2 ⟩
|
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ≡⟨ sym lem2 ⟩
|
||||||
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
|
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨⟩
|
||||||
μ Z ∘ R.func→ (rr g ∘ f) ∎
|
μ Z ∘ R.func→ (rr g ∘ f) ∎
|
||||||
where
|
where
|
||||||
-- Proved it in reverse here... otherwise it could be neatly inlined.
|
-- Proved it in reverse here... otherwise it could be neatly inlined.
|
||||||
lem2
|
lem2
|
||||||
: μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
|
: μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f)
|
||||||
≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
|
≡ μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f)
|
||||||
lem2 = begin
|
lem2 = begin
|
||||||
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
|
μ Z ∘ R.func→ (μ Z ∘ R.func→ g ∘ f) ≡⟨ cong (λ φ → μ Z ∘ φ) distrib ⟩
|
||||||
μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
|
μ Z ∘ (R.func→ (μ Z) ∘ R.func→ (R.func→ g) ∘ R.func→ f) ≡⟨⟩
|
||||||
μ Z ∘ (R.func→ (μ Z) ∘ RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
|
μ Z ∘ (R.func→ (μ Z) ∘ RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
|
||||||
(μ Z ∘ R.func→ (μ Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ cong (λ φ → φ ∘ (RR.func→ g ∘ R.func→ f)) lemmm ⟩
|
(μ Z ∘ R.func→ (μ Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ cong (λ φ → φ ∘ (RR.func→ g ∘ R.func→ f)) lemmm ⟩
|
||||||
(μ Z ∘ μ (R.func* Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
|
(μ Z ∘ μ (R.func* Z)) ∘ (RR.func→ g ∘ R.func→ f) ≡⟨ {!!} ⟩ -- ●-solver?
|
||||||
μ Z ∘ μ (R.func* Z) ∘ RR.func→ g ∘ R.func→ f ≡⟨ {!!} ⟩ -- ●-solver + lem4
|
μ Z ∘ μ (R.func* Z) ∘ RR.func→ g ∘ R.func→ f ≡⟨ {!!} ⟩ -- ●-solver + lem4
|
||||||
μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f ≡⟨ sym (Category.isAssociative ℂ) ⟩
|
μ Z ∘ R.func→ g ∘ μ Y ∘ R.func→ f ≡⟨ sym (Category.isAssociative ℂ) ⟩
|
||||||
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
|
μ Z ∘ R.func→ g ∘ (μ Y ∘ R.func→ f) ∎
|
||||||
where
|
where
|
||||||
module RR = Functor F[ R ∘ R ]
|
module RR = Functor F[ R ∘ R ]
|
||||||
distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
|
distrib : ∀ {A B C D} {a : Arrow C D} {b : Arrow B C} {c : Arrow A B}
|
||||||
→ R.func→ (a ∘ b ∘ c)
|
→ R.func→ (a ∘ b ∘ c)
|
||||||
≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
|
≡ R.func→ a ∘ R.func→ b ∘ R.func→ c
|
||||||
distrib = {!!}
|
distrib = {!!}
|
||||||
comm : ∀ {A B C D E}
|
comm : ∀ {A B C D E}
|
||||||
→ {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
|
→ {a : Arrow D E} {b : Arrow C D} {c : Arrow B C} {d : Arrow A B}
|
||||||
→ a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
|
→ a ∘ (b ∘ c ∘ d) ≡ a ∘ b ∘ c ∘ d
|
||||||
comm = {!!}
|
comm = {!!}
|
||||||
μN = proj₂ μNat
|
μN = proj₂ μNat
|
||||||
lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
|
lemmm : μ Z ∘ R.func→ (μ Z) ≡ μ Z ∘ μ (R.func* Z)
|
||||||
lemmm = isAssociative
|
lemmm = isAssociative
|
||||||
lem4 : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
|
lem4 : μ (R.func* Z) ∘ RR.func→ g ≡ R.func→ g ∘ μ Y
|
||||||
lem4 = μN g
|
lem4 = μN g
|
||||||
|
|
||||||
forthIsMonad : K.IsMonad (forthRaw raw)
|
forthIsMonad : K.IsMonad (forthRaw raw)
|
||||||
Kis.isIdentity forthIsMonad = isIdentity
|
Kis.isIdentity forthIsMonad = isIdentity
|
||||||
|
|
@ -233,17 +247,79 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
Kis.isDistributive forthIsMonad = isDistributive
|
Kis.isDistributive forthIsMonad = isDistributive
|
||||||
|
|
||||||
forth : M.Monad → K.Monad
|
forth : M.Monad → K.Monad
|
||||||
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
|
Kleisli.Monad.raw (forth m) = forthRaw (M.Monad.raw m)
|
||||||
Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
|
Kleisli.Monad.isMonad (forth m) = forthIsMonad (M.Monad.isMonad m)
|
||||||
|
|
||||||
|
module _ (m : K.Monad) where
|
||||||
|
private
|
||||||
|
module ℂ = Category ℂ
|
||||||
|
open K.Monad m
|
||||||
|
module Mraw = M.RawMonad
|
||||||
|
open NaturalTransformation ℂ ℂ
|
||||||
|
|
||||||
|
rawR : RawFunctor ℂ ℂ
|
||||||
|
RawFunctor.func* rawR = RR
|
||||||
|
RawFunctor.func→ rawR f = rr (ζ ∘ f)
|
||||||
|
|
||||||
|
isFunctorR : IsFunctor ℂ ℂ rawR
|
||||||
|
IsFunctor.isIdentity isFunctorR = begin
|
||||||
|
rr (ζ ∘ 𝟙) ≡⟨ cong rr (proj₁ ℂ.isIdentity) ⟩
|
||||||
|
rr ζ ≡⟨ isIdentity ⟩
|
||||||
|
𝟙 ∎
|
||||||
|
IsFunctor.isDistributive isFunctorR {f = f} {g} = begin
|
||||||
|
rr (ζ ∘ (g ∘ f)) ≡⟨⟩
|
||||||
|
fmap (g ∘ f) ≡⟨ fusion ⟩
|
||||||
|
fmap g ∘ fmap f ≡⟨⟩
|
||||||
|
rr (ζ ∘ g) ∘ rr (ζ ∘ f) ∎
|
||||||
|
|
||||||
|
R : Functor ℂ ℂ
|
||||||
|
Functor.raw R = rawR
|
||||||
|
Functor.isFunctor R = isFunctorR
|
||||||
|
|
||||||
|
R2 : Functor ℂ ℂ
|
||||||
|
R2 = F[ R ∘ R ]
|
||||||
|
|
||||||
|
ηNat : NaturalTransformation F.identity R
|
||||||
|
ηNat = {!!}
|
||||||
|
|
||||||
|
μNat : NaturalTransformation R2 R
|
||||||
|
μNat = {!!}
|
||||||
|
|
||||||
|
backRaw : M.RawMonad
|
||||||
|
Mraw.R backRaw = R
|
||||||
|
Mraw.ηNat backRaw = ηNat
|
||||||
|
Mraw.μNat backRaw = μNat
|
||||||
|
|
||||||
|
module _ (m : K.Monad) where
|
||||||
|
open K.Monad m
|
||||||
|
open M.RawMonad (backRaw m)
|
||||||
|
module Mis = M.IsMonad
|
||||||
|
|
||||||
|
backIsMonad : M.IsMonad (backRaw m)
|
||||||
|
backIsMonad = {!!}
|
||||||
|
|
||||||
back : K.Monad → M.Monad
|
back : K.Monad → M.Monad
|
||||||
back = {!!}
|
Monoidal.Monad.raw (back m) = backRaw m
|
||||||
|
Monoidal.Monad.isMonad (back m) = backIsMonad m
|
||||||
|
|
||||||
|
|
||||||
|
forthRawEq : (m : K.Monad) → forthRaw (backRaw m) ≡ K.Monad.raw m
|
||||||
|
K.RawMonad.RR (forthRawEq m _) = K.RawMonad.RR (K.Monad.raw m)
|
||||||
|
K.RawMonad.ζ (forthRawEq m _) = K.RawMonad.ζ (K.Monad.raw m)
|
||||||
|
-- stuck
|
||||||
|
K.RawMonad.rr (forthRawEq m i) = {!!}
|
||||||
|
|
||||||
fortheq : (m : K.Monad) → forth (back m) ≡ m
|
fortheq : (m : K.Monad) → forth (back m) ≡ m
|
||||||
fortheq m = {!!}
|
fortheq m = K.Monad≡ (forthRawEq m)
|
||||||
|
|
||||||
|
backRawEq : (m : M.Monad) → backRaw (forth m) ≡ M.Monad.raw m
|
||||||
|
-- stuck
|
||||||
|
M.RawMonad.R (backRawEq m _) = ?
|
||||||
|
M.RawMonad.ηNat (backRawEq m x) = {!!}
|
||||||
|
M.RawMonad.μNat (backRawEq m x) = {!!}
|
||||||
|
|
||||||
backeq : (m : M.Monad) → back (forth m) ≡ m
|
backeq : (m : M.Monad) → back (forth m) ≡ m
|
||||||
backeq = {!!}
|
backeq m = M.Monad≡ (backRawEq m)
|
||||||
|
|
||||||
open import Cubical.GradLemma
|
open import Cubical.GradLemma
|
||||||
eqv : isEquiv M.Monad K.Monad forth
|
eqv : isEquiv M.Monad K.Monad forth
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue