Mercurial > hg > Members > kono > Proof > category
changeset 759:fa6b75fa1d09
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 18:44:47 +0900 |
| parents | 74d197dd8a68 |
| children | d17c556b9343 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 26 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Mon Dec 11 17:33:29 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 18:44:47 2017 +0900 @@ -319,61 +319,63 @@ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( μ ((a → b) → a → c) o (FMap F (λ k → FMap F k u) o η ((b → c) → (a → b) → a → c)) ) ) ) ) ) (λ f g x → f (g x)) ) - ≈⟨ {!!} ⟩ -- nat η + ≈⟨ ≡cong ( λ h → ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( μ ((a → b) → a → c) o h ) ) ) ) ) (λ f g x → f (g x)) )) (nat ( Monad.η monad)) ⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( μ ((a → b) → a → c) o (η (FObj F ((a → b) → a → c)) o (λ k → FMap F k u) ) ) ) ) ) ) (λ f g x → f (g x)) ) - ≈⟨ {!!} ⟩ -- assoc + ≈⟨⟩ -- assoc ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( ( μ ((a → b) → a → c) o η (FObj F ((a → b) → a → c)) ) o (λ k → FMap F k u) ) ) ) ) ) (λ f g x → f (g x)) ) - ≈⟨ {!!} ⟩ + ≈⟨ ≡cong ( λ h → ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( h o (λ k → FMap F k u) ) ) ) ) ) (λ f g x → f (g x)) ) ) ( IsMonad.unity1 ( Monad.isMonad monad )) ⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( id1 Sets (FObj (Monad.T monad) ((a → b) → a → c)) o (λ k → FMap F k u) ) ) ) ) ) (λ f g x → f (g x)) ) - ≈⟨ {!!} ⟩ -- idR + ≈⟨ ≡cong ( λ h → ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o h ) ) ) ) (λ f g x → f (g x)) )) (idL {_} {_} {λ k → FMap F k u} ) ⟩ ( λ w → ( μ c o (FMap F (λ k → FMap F k w) o ( μ (a → c) o ( FMap F (λ k → FMap F k v) o ( λ k → FMap F k u ) ) ) ) ) (λ 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 ) ⟩ ( λ 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 ) ≈⟨⟩ ( λ 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 ) - ≈⟨ {!!} ⟩ -- nat μ + ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} {μ c} ( car {_} {_} {_} {_} {_} { FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)))} (nat (Monad.μ monad)) )))) ⟩ ( λ w → ( μ c o ((μ (FObj F c) o FMap F (FMap F (λ k → FMap F k w) ) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) )))) u ) ≈⟨⟩ -- assoc ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) ) o ( FMap F ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (cdr {_} {_} {_} {_} {_} { μ c} (cdr {_} {_} {_} {_} {_} {μ (FObj F c)} ( distr F ))))) ⟩ ( λ w → ( μ c o (μ (FObj F c) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) ))))) u ) ≈⟨⟩ ( λ w → (( μ c o μ (FObj F c) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) - ≈⟨ {!!} ⟩ -- Monad assoc + ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → h u ) (car {_} {_} {_} {_} {_} {( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )} (IsMonad.assoc (Monad.isMonad monad )) ) )) ⟩ ( λ w → (( μ c o (FMap F ( μ c )) ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) )) u ) ≈⟨⟩ ( λ w → ( μ c o (FMap F ( μ c ) o ( FMap F (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) - ≈⟨ {!!} ⟩ + ≈↑⟨ extensionality Sets (λ w → ( ≡cong ( λ h → ( μ c o h) u ) (distr F) )) ⟩ ( λ w → ( μ c o (FMap F ( μ c o (FMap F (λ k → FMap F k w) o ((λ k → FMap F k v) o (λ f g x → f (g x)) )) ))) u ) ≈⟨⟩ ( λ w → ( μ c o (FMap F (λ x → ( μ c o (FMap F (λ k → FMap F k w) o (FMap F (λ g x₁ → x (g x₁))))) v ))) u ) - ≈⟨ {!!} ⟩ - ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F ((λ x → FMap F x w) o (λ g x₁ → k (g x₁))))) v ))) u ) - ≈⟨⟩ - ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F ((λ x → (FMap F ( k o x ) w)))) ) v ))) u ) - ≈⟨ {!!} ⟩ - ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F ((λ x → (FMap F k o FMap F x ) w))) ) v ))) u ) - ≈⟨⟩ - ( λ w → ( μ c o (FMap F (λ k → ( μ c o (FMap F (FMap F k o (λ h → FMap F h w))) ) v ))) u ) - ≈⟨ {!!} ⟩ - ( λ w → ( μ c o (FMap F (λ k → (( μ c o ( FMap F (FMap F k ) o FMap F (λ h → FMap F h w))) ) v ))) u ) - ≈⟨⟩ - ( λ w → ( μ c o (FMap F (λ k → ((( μ c o FMap F (FMap F k )) o FMap F (λ h → FMap F h w)) ) v ))) u ) - ≈⟨ {!!} ⟩ - ( λ w → ( μ c o (FMap F (λ k → ((( FMap F k o μ b ) o FMap F (λ h → FMap F h w)) ) v ))) u ) - ≈⟨⟩ + ≈⟨ extensionality Sets (λ w → ( ≡cong ( λ h → ( μ c o h ) u ) (fcong F ( extensionality Sets (λ k → ≡cong ( λ h → h v ) ( begin + μ c o (FMap F (λ x → FMap F x w) o (FMap F (λ g x₁ → k (g x₁)))) + ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ c} ( distr F ) ⟩ + μ 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} (?) ⟩ + μ 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)) ≈⟨⟩ + ( μ c o FMap F (FMap F k )) o FMap F (λ h → FMap F h w) + ≈⟨ {!!} ⟩ + ((( FMap F k o μ b ) o FMap F (λ h → FMap F h w)) ) + ∎ ) + ))))) ⟩ ( λ w → ( μ c o (FMap F (λ k → ( FMap F k o ( μ b o FMap F (λ h → FMap F h w)) ) v ))) u ) ≈⟨⟩ ( λ w → μ c (FMap F (λ k → FMap F k (μ b (FMap F (λ h → FMap F h w) v))) u) )