Feels really close

This commit is contained in:
Frederik Hanghøj Iversen 2018-03-08 00:36:38 +01:00
parent c8fef1d2b5
commit e43bee6d9f

View file

@ -695,31 +695,7 @@ module _ {a b : Level} { : Category a b} where
open import Function using (_∘_ ; _$_) open import Function using (_∘_ ; _$_)
module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where module _ (omap : Omap ) (pure : {X : Object} Arrow X (omap X)) where
open voe-2-3 omap pure open voe-2-3
-- Idea:
-- We want to prove
--
-- voe-2-3-1 ≃ voe-2-3-2
--
-- By using the equivalence we have already constructed.
--
-- We can construct `forth` by composing `forth0`, `forth1` and `forth2`:
--
-- forth0 : voe-2-3-1 → M.Monad
--
-- Where the we will naturally pick `omap` and `pure` as the corresponding
-- fields in M.Monad
--
-- `forth1` will be the equivalence we have already constructed.
--
-- forth1 : M.Monad ≃ K.Monad
--
-- `forth2` is the straight-forward isomporphism:
--
-- forth1 : K.Monad → voe-2-3-2
--
-- NB! This may not be so straightforward since the index of `voe-2-3-2` is
-- given before `K.Monad`.
private private
Monoidal→Kleisli : M.Monad K.Monad Monoidal→Kleisli : M.Monad K.Monad
Monoidal→Kleisli = proj₁ Monoidal≃Kleisli Monoidal→Kleisli = proj₁ Monoidal≃Kleisli
@ -727,57 +703,36 @@ module _ {a b : Level} { : Category a b} where
Kleisli→Monoidal : K.Monad M.Monad Kleisli→Monoidal : K.Monad M.Monad
Kleisli→Monoidal = inverse Monoidal≃Kleisli Kleisli→Monoidal = inverse Monoidal≃Kleisli
forth : voe-2-3-1 voe-2-3-2 forth : voe-2-3-1 omap pure voe-2-3-2 omap pure
forth = voe-2-3-2-fromMonad Monoidal→Kleisli voe-2-3-1.toMonad forth = voe-2-3-2-fromMonad Monoidal→Kleisli voe-2-3.voe-2-3-1.toMonad
back : voe-2-3-2 voe-2-3-1 back : voe-2-3-2 omap pure voe-2-3-1 omap pure
back = voe-2-3-1-fromMonad Kleisli→Monoidal voe-2-3-2.toMonad back = voe-2-3-1-fromMonad Kleisli→Monoidal voe-2-3.voe-2-3-2.toMonad
Voe-2-3-1-inverse = (toMonad fromMonad) Function.id forthEq : m _ _
where forthEq m = begin
fromMonad : (m : M.Monad) voe-2-3.voe-2-3-1 (M.Monad.Romap m) (λ {X} M.Monad.pureT m X)
fromMonad = voe-2-3-1-fromMonad
toMonad : {omap} {pure : {X : Object} Arrow X (omap X)} voe-2-3.voe-2-3-1 omap pure M.Monad
toMonad = voe-2-3.voe-2-3-1.toMonad
-- voe-2-3-1-inverse : (voe-2-3.voe-2-3-1.toMonad ∘ voe-2-3-1-fromMonad) ≡ Function.id
voe-2-3-1-inverse : Voe-2-3-1-inverse
voe-2-3-1-inverse = refl
Voe-2-3-2-inverse = (toMonad fromMonad) Function.id
where
fromMonad : (m : K.Monad) voe-2-3.voe-2-3-2 (K.Monad.omap m) (K.Monad.pure m)
fromMonad = voe-2-3-2-fromMonad
toMonad : {omap} {pure : {X : Object} Arrow X (omap X)} voe-2-3.voe-2-3-2 omap pure K.Monad
toMonad = voe-2-3.voe-2-3-2.toMonad
voe-2-3-2-inverse : Voe-2-3-2-inverse
voe-2-3-2-inverse = refl
forthEq' : m _ _
forthEq' m = begin
(forth back) m ≡⟨⟩ (forth back) m ≡⟨⟩
-- In full gory detail: -- In full gory detail:
( voe-2-3-2-fromMonad ( voe-2-3-2-fromMonad
Monoidal→Kleisli Monoidal→Kleisli
voe-2-3.voe-2-3-1.toMonad voe-2-3.voe-2-3-1.toMonad
voe-2-3-1-fromMonad voe-2-3-1-fromMonad
Kleisli→Monoidal Kleisli→Monoidal
voe-2-3.voe-2-3-2.toMonad voe-2-3.voe-2-3-2.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( voe-2-3-2-fromMonad ( voe-2-3-2-fromMonad
Monoidal→Kleisli Monoidal→Kleisli
Kleisli→Monoidal Kleisli→Monoidal
voe-2-3.voe-2-3-2.toMonad voe-2-3.voe-2-3-2.toMonad
) m ≡⟨ u ) m ≡⟨ u
-- Monoidal→Kleisli and Kleisli→Monoidal are inverses -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
-- I should be able to prove this using congruence and `lem` below. -- 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-2-fromMonad
voe-2-3.voe-2-3-2.toMonad voe-2-3.voe-2-3-2.toMonad
) m ≡⟨⟩ ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( voe-2-3-2-fromMonad
voe-2-3.voe-2-3-2.toMonad
) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m m
where where
lem : Monoidal→Kleisli Kleisli→Monoidal Function.id lem : Monoidal→Kleisli Kleisli→Monoidal Function.id
@ -789,49 +744,30 @@ module _ {a b : Level} { : Category a b} where
{m : _} (a (Monoidal→Kleisli Kleisli→Monoidal) b) m (a b) m {m : _} (a (Monoidal→Kleisli Kleisli→Monoidal) b) m (a b) m
u {m = m} = cong (λ φ φ m) t u {m = m} = cong (λ φ φ m) t
forthEq : m (forth back) m m
forthEq m = begin
(forth back) m ≡⟨⟩
-- In full gory detail:
( voe-2-3-2-fromMonad
Monoidal→Kleisli
voe-2-3-1.toMonad
voe-2-3-1-fromMonad
Kleisli→Monoidal
voe-2-3-2.toMonad
) m ≡⟨ {!!} -- fromMonad and toMonad are inverses
( voe-2-3-2-fromMonad
Monoidal→Kleisli
Kleisli→Monoidal
voe-2-3-2.toMonad
) m ≡⟨ {!!} -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
( voe-2-3-2-fromMonad
voe-2-3-2.toMonad
) m ≡⟨ {!!} -- fromMonad and toMonad are inverses
m
backEq : m (back forth) m m backEq : m (back forth) m m
backEq m = begin backEq m = begin
(back forth) m ≡⟨⟩ (back forth) m ≡⟨⟩
( voe-2-3-1-fromMonad ( voe-2-3-1-fromMonad
Kleisli→Monoidal Kleisli→Monoidal
voe-2-3-2.toMonad voe-2-3.voe-2-3-2.toMonad
voe-2-3-2-fromMonad voe-2-3-2-fromMonad
Monoidal→Kleisli Monoidal→Kleisli
voe-2-3-1.toMonad voe-2-3.voe-2-3-1.toMonad
) m ≡⟨ {!!} -- fromMonad and toMonad are inverses ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
( voe-2-3-1-fromMonad ( voe-2-3-1-fromMonad
Kleisli→Monoidal Kleisli→Monoidal
Monoidal→Kleisli Monoidal→Kleisli
voe-2-3-1.toMonad voe-2-3.voe-2-3-1.toMonad
) m ≡⟨ {!!} -- Monoidal→Kleisli and Kleisli→Monoidal are inverses ) m ≡⟨ cong (λ φ φ m) t -- Monoidal→Kleisli and Kleisli→Monoidal are inverses
( voe-2-3-1-fromMonad ( voe-2-3-1-fromMonad
voe-2-3-1.toMonad voe-2-3.voe-2-3-1.toMonad
) m ≡⟨ {!!} -- fromMonad and toMonad are inverses ) m ≡⟨⟩ -- fromMonad and toMonad are inverses
m 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 voe-2-3-2 forth voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth
voe-isEquiv = gradLemma forth back forthEq backEq voe-isEquiv = gradLemma forth back forthEq backEq
equiv-2-3 : voe-2-3-1 voe-2-3-2 equiv-2-3 : voe-2-3-1 omap pure voe-2-3-2 omap pure
equiv-2-3 = forth , voe-isEquiv equiv-2-3 = forth , voe-isEquiv