From e43bee6d9fc63564a81c4bd94bd003b9f8fa5a29 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 8 Mar 2018 00:36:38 +0100 Subject: [PATCH] Feels really close --- src/Cat/Category/Monad.agda | 120 +++++++++--------------------------- 1 file changed, 28 insertions(+), 92 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 5fefe1e..c0c42bf 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -695,31 +695,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where open import Function using (_∘_ ; _$_) module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where - open voe-2-3 ℂ omap pure - -- 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`. + open voe-2-3 ℂ private Monoidal→Kleisli : M.Monad → K.Monad 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 = inverse Monoidal≃Kleisli - forth : voe-2-3-1 → voe-2-3-2 - forth = voe-2-3-2-fromMonad ∘ Monoidal→Kleisli ∘ voe-2-3-1.toMonad + 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 → voe-2-3-1 - back = voe-2-3-1-fromMonad ∘ Kleisli→Monoidal ∘ voe-2-3-2.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 - Voe-2-3-1-inverse = (toMonad ∘ fromMonad) ≡ Function.id - where - 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 + forthEq : ∀ m → _ ≡ _ + forthEq m = begin (forth ∘ back) m ≡⟨⟩ -- In full gory detail: - ( voe-2-3-2-fromMonad + ( 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 + ) 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 ⟩ + ) 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 ≡⟨⟩ - ( voe-2-3-2-fromMonad - ∘ voe-2-3.voe-2-3-2.toMonad - ) m ≡⟨⟩ -- fromMonad and toMonad are inverses + ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where 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 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 = begin (back ∘ forth) m ≡⟨⟩ - ( voe-2-3-1-fromMonad + ( voe-2-3-1-fromMonad ∘ Kleisli→Monoidal - ∘ voe-2-3-2.toMonad + ∘ voe-2-3.voe-2-3-2.toMonad ∘ voe-2-3-2-fromMonad ∘ Monoidal→Kleisli - ∘ voe-2-3-1.toMonad - ) m ≡⟨ {!!} ⟩ -- fromMonad and toMonad are inverses - ( voe-2-3-1-fromMonad + ∘ 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-1.toMonad - ) m ≡⟨ {!!} ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses - ( voe-2-3-1-fromMonad - ∘ voe-2-3-1.toMonad - ) m ≡⟨ {!!} ⟩ -- fromMonad and toMonad are inverses + ∘ 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 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 - 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