Mercurial > hg > Members > kono > Proof > category
changeset 752:e7ace77d7235
connected
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 22:26:01 +0900 |
| parents | 7fd8c4fbafb9 |
| children | b7d804370c1d |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 18 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 21:01:06 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 22:26:01 2017 +0900 @@ -117,7 +117,24 @@ ( μ ( x * ( y * z ) ) o FMap F ( μ ( x * ( y * z ) ))) o (FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b )) ≈⟨ {!!} ⟩ --- monad assoc ( μ ( x * ( y * z ) ) o μ ( FObj F (x * ( y * z ) ))) o (FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b )) - ≈⟨ {!!} ⟩ + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) )} ( cdr {_} {_} {_} {_} {_} { μ ( FObj F (x * ( y * z ) ))} ( begin + FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b ) + ≈⟨⟩ + FMap F ( λ h → ( FMap F (( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ g → h , g))) b ) + ≈⟨ {!!} ⟩ + FMap F ( λ h → ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (FMap F (λ g → h , g))) b ) + ≈⟨⟩ + FMap F ( FMap F ( λ f → ( FMap F (λ x₂ → proj₁ f , proj₂ f , x₂)) c) o (λ h → FMap F (λ g → h , g) b) ) + ≈⟨⟩ + FMap F ( FMap F ( λ f → ( FMap F ((λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ g → f , g))) c) o (λ f → FMap F (λ g → f , g) b) ) + ≈⟨ {!!} ⟩ + FMap F ( FMap F ( λ f → ( FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o FMap F (λ g → f , g)) c) o (λ f → FMap F (λ g → f , g) b) ) + ≈⟨⟩ + FMap F ( FMap F ( FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ f → FMap F (λ g → f , g) c)) o (λ f → FMap F (λ g → f , g) b) ) + ≈⟨ {!!} ⟩ + FMap F ( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ f → FMap F (λ g → f , g) c)) ) o (FMap F (λ f → FMap F (λ g → f , g) b) ) + ∎ + )) ⟩ ( μ ( x * ( y * z )) o μ ( FObj F (x * ( y * z )))) o ( FMap F ( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o (λ f → FMap F (λ g → f , g) c)) ) o (FMap F (λ f → FMap F (λ g → f , g) b) ) ) ≈⟨ {!!} ⟩ -- assoc