Mercurial > hg > Members > kono > Proof > category
changeset 736:c1362961132a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 02 Dec 2017 09:18:20 +0900 |
| parents | 84147ef7cada |
| children | a4792945cd9b |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 8 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sat Dec 02 00:30:44 2017 +0900 +++ b/monad→monoidal.agda Sat Dec 02 09:18:20 2017 +0900 @@ -131,16 +131,16 @@ ( λ u → μ a (FMap F (λ k → FMap F k u) (η (a → a) (λ x → x)))) ≈⟨⟩ (λ u → μ a ((FMap F (λ k → FMap F k u) o η (a → a)) (id1 Sets a ))) - ≈⟨ ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans (Monad.η monad ) )))) ⟩ - (λ u → μ a ((η (FObj F a) o FMap F (id1 Sets a)) u ) ) - ≈⟨ ≡cong ( λ h → (λ u → μ a ( ( η (FObj F a) o h) u ))) (IsFunctor.identity (Functor.isFunctor F )) ⟩ - (λ u → μ a ((η (FObj F a) o id1 Sets (FObj F a)) u ) ) - ≈⟨ ≡cong ( λ h → (λ u → μ a ( h u ))) idR ⟩ - (λ u → μ a (η (FObj F a) u)) + ≈⟨ ≡cong ( λ h → λ u → μ a (h u (id1 Sets a) ) ) ( extensionality Sets ( λ x → (IsNTrans.commute (NTrans.isNTrans (Monad.η monad ) )))) ⟩ + (λ u → μ a ( (η (FObj F a) o FMap F ( (id1 Sets a )) ) u ) ) ≈⟨⟩ - μ a o η (FObj F a) + μ a o (η (FObj F a) o FMap F (id1 Sets a)) + ≈⟨ ≡cong ( λ h → (λ u → μ a ( ( η (FObj F a) o h) u ))) (IsFunctor.identity (Functor.isFunctor F )) ⟩ -- cdr cdr + μ a o (η (FObj F a) o id1 Sets (FObj F a)) + ≈⟨ ≡cong ( λ h → (λ u → μ a ( h u ))) idR ⟩ -- cdr idR + μ a o η (FObj F a) ≈⟨ IsMonad.unity1 (Monad.isMonad monad ) ⟩ - id1 Sets (FObj F a) + id1 Sets (FObj F a) ≈⟨⟩ ( λ u → u ) ∎ )