Tidy up
This commit is contained in:
parent
0cebe1e866
commit
485703c85e
|
|
@ -7,6 +7,7 @@ open import Data.Product
|
||||||
|
|
||||||
open import Cubical
|
open import Cubical
|
||||||
open import Cubical.NType.Properties using (lemPropF ; lemSig)
|
open import Cubical.NType.Properties using (lemPropF ; lemSig)
|
||||||
|
open import Cubical.GradLemma using (gradLemma)
|
||||||
|
|
||||||
open import Cat.Category
|
open import Cat.Category
|
||||||
open import Cat.Category.Functor as F
|
open import Cat.Category.Functor as F
|
||||||
|
|
@ -357,25 +358,27 @@ module Kleisli {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
isMonad : IsMonad raw
|
isMonad : IsMonad raw
|
||||||
open IsMonad isMonad public
|
open IsMonad isMonad public
|
||||||
|
|
||||||
module _ (raw : RawMonad) where
|
private
|
||||||
open RawMonad raw
|
module _ (raw : RawMonad) where
|
||||||
propIsIdentity : isProp IsIdentity
|
open RawMonad raw
|
||||||
propIsIdentity x y i = ℂ.arrowsAreSets _ _ x y i
|
propIsIdentity : isProp IsIdentity
|
||||||
propIsNatural : isProp IsNatural
|
propIsIdentity x y i = ℂ.arrowsAreSets _ _ x y i
|
||||||
propIsNatural x y i = λ f
|
propIsNatural : isProp IsNatural
|
||||||
→ ℂ.arrowsAreSets _ _ (x f) (y f) i
|
propIsNatural x y i = λ f
|
||||||
propIsDistributive : isProp IsDistributive
|
→ ℂ.arrowsAreSets _ _ (x f) (y f) i
|
||||||
propIsDistributive x y i = λ g f
|
propIsDistributive : isProp IsDistributive
|
||||||
→ ℂ.arrowsAreSets _ _ (x g f) (y g f) i
|
propIsDistributive x y i = λ g f
|
||||||
|
→ ℂ.arrowsAreSets _ _ (x g f) (y g f) i
|
||||||
|
|
||||||
|
open IsMonad
|
||||||
|
propIsMonad : (raw : _) → isProp (IsMonad raw)
|
||||||
|
IsMonad.isIdentity (propIsMonad raw x y i)
|
||||||
|
= propIsIdentity raw (isIdentity x) (isIdentity y) i
|
||||||
|
IsMonad.isNatural (propIsMonad raw x y i)
|
||||||
|
= propIsNatural raw (isNatural x) (isNatural y) i
|
||||||
|
IsMonad.isDistributive (propIsMonad raw x y i)
|
||||||
|
= propIsDistributive raw (isDistributive x) (isDistributive y) i
|
||||||
|
|
||||||
open IsMonad
|
|
||||||
propIsMonad : (raw : _) → isProp (IsMonad raw)
|
|
||||||
IsMonad.isIdentity (propIsMonad raw x y i)
|
|
||||||
= propIsIdentity raw (isIdentity x) (isIdentity y) i
|
|
||||||
IsMonad.isNatural (propIsMonad raw x y i)
|
|
||||||
= propIsNatural raw (isNatural x) (isNatural y) i
|
|
||||||
IsMonad.isDistributive (propIsMonad raw x y i)
|
|
||||||
= propIsDistributive raw (isDistributive x) (isDistributive y) i
|
|
||||||
module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
|
module _ {m n : Monad} (eq : Monad.raw m ≡ Monad.raw n) where
|
||||||
private
|
private
|
||||||
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
|
eqIsMonad : (λ i → IsMonad (eq i)) [ Monad.isMonad m ≡ Monad.isMonad n ]
|
||||||
|
|
@ -400,7 +403,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
open M.RawMonad m
|
open M.RawMonad m
|
||||||
|
|
||||||
forthRaw : K.RawMonad
|
forthRaw : K.RawMonad
|
||||||
K.RawMonad.omap forthRaw = Romap
|
K.RawMonad.omap forthRaw = Romap
|
||||||
K.RawMonad.pure forthRaw = pureT _
|
K.RawMonad.pure forthRaw = pureT _
|
||||||
K.RawMonad.bind forthRaw = bind
|
K.RawMonad.bind forthRaw = bind
|
||||||
|
|
||||||
|
|
@ -413,63 +416,58 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
K.IsMonad.isDistributive forthIsMonad = MI.isDistributive
|
K.IsMonad.isDistributive forthIsMonad = MI.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
|
module _ (m : K.Monad) where
|
||||||
private
|
open K.Monad m
|
||||||
open K.Monad m
|
|
||||||
module MR = M.RawMonad
|
|
||||||
module MI = M.IsMonad
|
|
||||||
|
|
||||||
backRaw : M.RawMonad
|
backRaw : M.RawMonad
|
||||||
MR.R backRaw = R
|
M.RawMonad.R backRaw = R
|
||||||
MR.pureNT backRaw = pureNT
|
M.RawMonad.pureNT backRaw = pureNT
|
||||||
MR.joinNT backRaw = joinNT
|
M.RawMonad.joinNT backRaw = joinNT
|
||||||
|
|
||||||
private
|
private
|
||||||
open MR backRaw
|
open M.RawMonad backRaw
|
||||||
module R = Functor (MR.R backRaw)
|
module R = Functor (M.RawMonad.R backRaw)
|
||||||
|
|
||||||
backIsMonad : M.IsMonad backRaw
|
backIsMonad : M.IsMonad backRaw
|
||||||
MI.isAssociative backIsMonad {X} = begin
|
M.IsMonad.isAssociative backIsMonad {X} = begin
|
||||||
joinT X ∘ R.func→ (joinT X) ≡⟨⟩
|
joinT X ∘ R.func→ (joinT X) ≡⟨⟩
|
||||||
join ∘ fmap (joinT X) ≡⟨⟩
|
join ∘ fmap (joinT X) ≡⟨⟩
|
||||||
join ∘ fmap join ≡⟨ isNaturalForeign ⟩
|
join ∘ fmap join ≡⟨ isNaturalForeign ⟩
|
||||||
join ∘ join ≡⟨⟩
|
join ∘ join ≡⟨⟩
|
||||||
joinT X ∘ joinT (R.func* X) ∎
|
joinT X ∘ joinT (R.func* X) ∎
|
||||||
MI.isInverse backIsMonad {X} = inv-l , inv-r
|
M.IsMonad.isInverse backIsMonad {X} = inv-l , inv-r
|
||||||
where
|
where
|
||||||
inv-l = begin
|
inv-l = begin
|
||||||
joinT X ∘ pureT (R.func* X) ≡⟨⟩
|
joinT X ∘ pureT (R.func* X) ≡⟨⟩
|
||||||
join ∘ pure ≡⟨ proj₁ isInverse ⟩
|
join ∘ pure ≡⟨ proj₁ isInverse ⟩
|
||||||
𝟙 ∎
|
𝟙 ∎
|
||||||
inv-r = begin
|
inv-r = begin
|
||||||
joinT X ∘ R.func→ (pureT X) ≡⟨⟩
|
joinT X ∘ R.func→ (pureT X) ≡⟨⟩
|
||||||
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
|
join ∘ fmap pure ≡⟨ proj₂ isInverse ⟩
|
||||||
𝟙 ∎
|
𝟙 ∎
|
||||||
|
|
||||||
back : K.Monad → M.Monad
|
back : K.Monad → M.Monad
|
||||||
Monoidal.Monad.raw (back m) = backRaw m
|
Monoidal.Monad.raw (back m) = backRaw m
|
||||||
Monoidal.Monad.isMonad (back m) = backIsMonad m
|
Monoidal.Monad.isMonad (back m) = backIsMonad m
|
||||||
|
|
||||||
-- I believe all the proofs here should be `refl`.
|
|
||||||
module _ (m : K.Monad) where
|
module _ (m : K.Monad) where
|
||||||
open K.Monad m
|
open K.Monad m
|
||||||
-- open K.RawMonad (K.Monad.raw m)
|
|
||||||
bindEq : ∀ {X Y}
|
bindEq : ∀ {X Y}
|
||||||
→ K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y}
|
→ K.RawMonad.bind (forthRaw (backRaw m)) {X} {Y}
|
||||||
≡ K.RawMonad.bind (K.Monad.raw m)
|
≡ K.RawMonad.bind (K.Monad.raw m)
|
||||||
bindEq {X} {Y} = begin
|
bindEq {X} {Y} = begin
|
||||||
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
|
K.RawMonad.bind (forthRaw (backRaw m)) ≡⟨⟩
|
||||||
(λ f → joinT Y ∘ func→ R f) ≡⟨⟩
|
(λ f → join ∘ fmap f) ≡⟨⟩
|
||||||
(λ f → join ∘ fmap f) ≡⟨⟩
|
(λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩
|
||||||
(λ f → bind (f >>> pure) >>> bind 𝟙) ≡⟨ funExt lem ⟩
|
(λ f → bind f) ≡⟨⟩
|
||||||
(λ f → bind f) ≡⟨⟩
|
bind ∎
|
||||||
bind ∎
|
|
||||||
where
|
where
|
||||||
joinT = proj₁ joinNT
|
lem : (f : Arrow X (omap Y))
|
||||||
lem : (f : Arrow X (omap Y)) → bind (f >>> pure) >>> bind 𝟙 ≡ bind f
|
→ bind (f >>> pure) >>> bind 𝟙
|
||||||
|
≡ bind f
|
||||||
lem f = begin
|
lem f = begin
|
||||||
bind (f >>> pure) >>> bind 𝟙
|
bind (f >>> pure) >>> bind 𝟙
|
||||||
≡⟨ isDistributive _ _ ⟩
|
≡⟨ isDistributive _ _ ⟩
|
||||||
|
|
@ -481,13 +479,9 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
|
≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩
|
||||||
bind f ∎
|
bind f ∎
|
||||||
|
|
||||||
_&_ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A → (A → B) → B
|
|
||||||
x & f = f x
|
|
||||||
|
|
||||||
forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
|
forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m
|
||||||
K.RawMonad.omap (forthRawEq _) = omap
|
K.RawMonad.omap (forthRawEq _) = omap
|
||||||
K.RawMonad.pure (forthRawEq _) = pure
|
K.RawMonad.pure (forthRawEq _) = pure
|
||||||
-- stuck
|
|
||||||
K.RawMonad.bind (forthRawEq i) = bindEq i
|
K.RawMonad.bind (forthRawEq i) = bindEq i
|
||||||
|
|
||||||
fortheq : (m : K.Monad) → forth (back m) ≡ m
|
fortheq : (m : K.Monad) → forth (back m) ≡ m
|
||||||
|
|
@ -543,14 +537,13 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
|
||||||
[ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
|
[ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
|
||||||
backRawEq : backRaw (forth m) ≡ M.Monad.raw m
|
backRawEq : backRaw (forth m) ≡ M.Monad.raw m
|
||||||
-- stuck
|
-- stuck
|
||||||
M.RawMonad.R (backRawEq i) = Req i
|
M.RawMonad.R (backRawEq i) = Req i
|
||||||
M.RawMonad.pureNT (backRawEq i) = {!!} -- pureNTEq i
|
M.RawMonad.pureNT (backRawEq i) = {!!} -- pureNTEq i
|
||||||
M.RawMonad.joinNT (backRawEq i) = {!!}
|
M.RawMonad.joinNT (backRawEq i) = {!!}
|
||||||
|
|
||||||
backeq : (m : M.Monad) → back (forth m) ≡ m
|
backeq : (m : M.Monad) → back (forth m) ≡ m
|
||||||
backeq m = M.Monad≡ (backRawEq m)
|
backeq m = M.Monad≡ (backRawEq m)
|
||||||
|
|
||||||
open import Cubical.GradLemma
|
|
||||||
eqv : isEquiv M.Monad K.Monad forth
|
eqv : isEquiv M.Monad K.Monad forth
|
||||||
eqv = gradLemma forth back fortheq backeq
|
eqv = gradLemma forth back fortheq backeq
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue