fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Voe: gone back to equational reasoning, as it's fairly cheap now.

Browse source
This commit is contained in:
Andrea Vezzosi 2018-05-16 10:50:56 +02:00
parent 9f7a13b5da
commit 47c881ba2a
1 changed files with 29 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/Cat/Category/Monad/Voevodsky.agda
View file

@ -141,10 +141,19 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
back = §1-fromMonad ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad
forthEq : ∀ m → (forth ∘ back) m ≡ m
forthEq m = trans
(trans (cong-d (§2-fromMonad ∘ Monoidal→Kleisli) (lemmaz (Kleisli→Monoidal (§2-3.§2.toMonad m))))
(cong-d (\ φ → §2-fromMonad (φ (§2-3.§2.toMonad m))) re-ve))
lemma
forthEq m = begin
§2-fromMonad
(Monoidal→Kleisli
(§2-3.§1.toMonad
(§1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad m)))))
≡⟨ cong-d (§2-fromMonad ∘ Monoidal→Kleisli) (lemmaz (Kleisli→Monoidal (§2-3.§2.toMonad m))) ⟩
§2-fromMonad
((Monoidal→Kleisli ∘ Kleisli→Monoidal)
(§2-3.§2.toMonad m))
≡⟨ (cong-d (\ φ → §2-fromMonad (φ (§2-3.§2.toMonad m))) re-ve) ⟩
(§2-fromMonad ∘ §2-3.§2.toMonad) m
≡⟨ lemma ⟩
m ∎
where
lemma : (§2-fromMonad ∘ §2-3.§2.toMonad) m ≡ m
§2-3.§2.bind (lemma i) = §2-3.§2.bind m
@ -154,10 +163,23 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
M.Monad.isMonad (lemmaz m i) = M.Monad.isMonad m
backEq : ∀ m → (back ∘ forth) m ≡ m
backEq m = trans (cong-d (§1-fromMonad ∘ Kleisli→Monoidal) (lemma (Monoidal→Kleisli (§2-3.§1.toMonad m))))
(trans (cong-d (\ φ → §1-fromMonad (φ (§2-3.§1.toMonad m))) ve-re)
lemmaz)
backEq m = begin
§1-fromMonad
(Kleisli→Monoidal
(§2-3.§2.toMonad
(§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
≡⟨ cong-d (§1-fromMonad ∘ Kleisli→Monoidal) (lemma (Monoidal→Kleisli (§2-3.§1.toMonad m))) ⟩
§1-fromMonad
((Kleisli→Monoidal ∘ Monoidal→Kleisli)
(§2-3.§1.toMonad m))
≡⟨ (cong-d (\ φ → §1-fromMonad (φ (§2-3.§1.toMonad m))) ve-re) ⟩
§1-fromMonad (§2-3.§1.toMonad m)
≡⟨ lemmaz ⟩
m ∎
where
-- having eta equality on causes roughly the same work as checking this proof of foo,
-- which is quite expensive because it ends up reducing complex terms.
-- rhs = §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))
-- foo : §1-fromMonad (Kleisli→Monoidal (§2-3.§2.toMonad (§2-fromMonad (Monoidal→Kleisli (§2-3.§1.toMonad m)))))
-- ≡ §1-fromMonad (Kleisli→Monoidal ((Monoidal→Kleisli (§2-3.§1.toMonad m))))