Mercurial > hg > Members > kono > Proof > category
changeset 760:d17c556b9343
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 20:37:22 +0900 |
| parents | fa6b75fa1d09 |
| children | e7c673eba848 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 6 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 18:44:47 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 20:37:22 2017 +0900 @@ -337,7 +337,7 @@ ) ) ) ) ) (λ f g x → f (g x)) ) ≈⟨⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → ( FMap F (λ k → FMap F k v) o FMap F j ) u )))) (λ f g x → f (g x)) ) - ≈↑⟨ ≡cong ( λ h → ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → h u )))) (λ f g x → f (g x)) )) (distr F ) ⟩ + ≈↑⟨ ≡cong ( λ h → ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → h u )))) (λ (f : (b → c) ) (g : (a → b)) (x : a ) → f (g x)) )) (distr F ) ⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( λ j → ( FMap F (( λ k → FMap F k v) o j ) u ))))) (λ f g x → f (g x)) ) ≈⟨⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) @@ -365,14 +365,15 @@ μ c o (FMap F ((λ x → FMap F x w) o (λ g x₁ → k (g x₁)))) ≈⟨⟩ μ c o (FMap F ((λ x → (FMap F ( k o x ) w)))) - ≈⟨ cdr {_} {_} {_} {_} {_} {μ c} (?) ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {μ c} ( fcong F ( extensionality Sets ( λ x → ≡cong ( λ h → h w ) (distr F ) ))) ⟩ μ c o (FMap F ((λ x → (FMap F k o FMap F x ) w))) ≈⟨⟩ μ c o (FMap F (FMap F k o (λ h → FMap F h w))) - ≈⟨ {!!} ⟩ - μ c o ( FMap F (FMap F k ) o FMap F (λ h → FMap F h w)) ≈⟨⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} {μ c} ( distr F ) ⟩ + μ c o ( FMap F (FMap F k ) o FMap F (λ h → FMap F h w)) + ≈⟨⟩ ( μ c o FMap F (FMap F k )) o FMap F (λ h → FMap F h w) - ≈⟨ {!!} ⟩ + ≈↑⟨ car {_} {_} {_} {_} {_} {FMap F (λ h → FMap F h w)} (nat ( Monad.μ monad )) ⟩ ((( FMap F k o μ b ) o FMap F (λ h → FMap F h w)) ) ∎ ) ))))) ⟩