Mercurial > hg > Members > kono > Proof > category

changeset 762:96afaa736186

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
connected interchange
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 11 Dec 2017 23:08:25 +0900
parents e7c673eba848
children 37ddc8228832
files monad→monoidal.agda
diffstat 1 files changed, 4 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/monad→monoidal.agda	Mon Dec 11 22:03:32 2017 +0900
+++ b/monad→monoidal.agda	Mon Dec 11 23:08:25 2017 +0900
@@ -421,13 +421,11 @@
              ≈⟨ {!!} ⟩
                  ( λ x → (μ b o (FMap F (λ k → (η b o k ) x))) u )
              ≈⟨ {!!} ⟩
-                 ( λ x → (μ b o ( η (FObj F b) o  FMap F ( {!!} ))) u )
-             ≈⟨ {!!} ⟩
-                 ( λ x → (μ b o ((FMap F (FMap F  (λ f → f x) )) o η (FObj F (a → b) ))) u )
+                 ( λ x → (μ b o ( FMap F ( FMap F   (λ f → f x) )   o FMap F ( η (a → b) ))) u )
              ≈⟨ {!!} ⟩
-                 ( λ x → (((FMap F  (λ f → f x)  o μ (a → b)) o η (FObj F (a → b)))) u )
-             ≈⟨⟩
-                 ( λ x → ((FMap F  (λ f → f x) o (μ (a → b) o η (FObj F (a → b))))) u )
+                 ( λ x → ( (μ b o (FMap F ( FMap F   (λ f → f x) )) )  o FMap F ( η (a → b) )) u )
+             ≈⟨ {!!} ⟩
+                 ( λ x → ((FMap F  (λ f → f x) o (μ (a → b) o FMap F ( η (a → b) )))) u )
              ≈⟨ {!!} ⟩
                  ( λ x → ((FMap F (λ f → f x) o id1 Sets (FObj F (a → b)))) u )
              ≈⟨ {!!} ⟩