Mercurial > hg > Members > kono > Proof > category
changeset 751:7fd8c4fbafb9
FMap remains
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 21:01:06 +0900 |
| parents | b45587696acf |
| children | e7ace77d7235 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 53 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 17:55:28 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 21:01:06 2017 +0900 @@ -94,13 +94,63 @@ ≈⟨⟩ ( λ a → μ ( x * ( y * z ) ) (FMap F (λ f → FMap F (λ g → f , g) (μ (y * z ) (FMap F (λ f₁ → FMap F (λ g → f₁ , g) c) b))) a)) ≈⟨⟩ - μ ( x * ( y * z ) ) o (FMap F (λ f → FMap F (λ g → f , g) (μ (y * z ) (FMap F (λ f₁ → FMap F (λ g → f₁ , g) c) b)))) + μ ( x * ( y * z ) ) o (FMap F (λ f → ( FMap F (λ g → f , g) o ( μ (y * z ) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) )) b )) + ≈⟨ {!!} ⟩ -- assoc + μ ( x * ( y * z ) ) o (FMap F (λ f → ( (FMap F (λ g → f , g) o ( μ (y * z ))) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) ) b )) + ≈⟨ {!!} ⟩ -- nat μ + μ ( x * ( y * z ) ) o (FMap F (λ f → ( ( μ ( x * ( y * z ) ) o FMap F (FMap F (λ g → f , g)) ) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) ) b )) + ≈⟨ {!!} ⟩ -- assoc + μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (FMap F (λ g → f , g)) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c )) ) b )) + ≈⟨ {!!} ⟩ -- distr F + μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (FMap F (λ g → f , g) o (λ f₁ → FMap F (λ g → f₁ , g) c)))) b )) + ≈⟨⟩ + μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F ((λ f₁ → (FMap F (λ g → f , g) o FMap F (λ g → f₁ , g)) c)))) b )) + ≈⟨ {!!} ⟩ -- distr F + μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ f₁ → (FMap F ((λ g → f , g) o (λ g → f₁ , g))) c))) b )) + ≈⟨⟩ + μ ( x * ( y * z ) ) o (FMap F (λ f → ( μ ( x * ( y * z ) ) o ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c))) b )) + ≈⟨⟩ + μ ( x * ( y * z ) ) o (FMap F ( μ ( x * ( y * z ) ) o (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b ))) + ≈⟨ {!!} ⟩ -- distr F + μ ( x * ( y * z ) ) o (FMap F ( μ ( x * ( y * z ) )) o FMap F (λ f → ( FMap F (λ g → (FMap F (λ h → f , (g , h))) c)) b )) + ≈⟨ {!!} ⟩ -- assoc + ( μ ( 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 )) ≈⟨ {!!} ⟩ + ( μ ( 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 + μ ( 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 + μ ( 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) )) + --- ≈⟨ cdr (car ( nat (Monad.μ monad ))) ⟩ + ≈⟨ {!!} ⟩ + μ ( x * ( y * z )) o (( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o + (λ f → FMap F (λ g → f , g) c)) o μ (x * y ) ) o (FMap F (λ f → FMap F (λ g → f , g) b) )) + ≈⟨ {!!} ⟩ --- assoc + μ ( x * ( y * z )) o ( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o + (λ f → FMap F (λ g → f , g) c)) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) ))) + ≈⟨ {!!} ⟩ --- assoc + μ ( x * ( y * z )) o (( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ) o + FMap F (λ f → FMap F (λ g → f , g) c)) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) ))) + ≈⟨ {!!} ⟩ -- assoc + μ ( x * ( y * z )) o (( FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) )) o + (FMap F (λ f → FMap F (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) )))) + ≈⟨ {!!} ⟩ -- assoc + ( μ ( x * ( y * z )) o (FMap F (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) ))) o + (FMap F (λ f → FMap F (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) ))) + ≈⟨ {!!} ⟩ -- nat μ + (FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o μ ( ( x * y ) * z )) o + (FMap F (λ f → FMap F (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) ))) + ≈⟨ {!!} ⟩ -- nat μ FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) o - (μ ( ( x * y ) * z ) o (FMap F (λ f → FMap (Monad.T monad) (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) )))) + (μ ( ( x * y ) * z ) o (FMap F (λ f → FMap F (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) )))) ≈⟨⟩ ( λ a → FMap F (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc) - (μ ( ( x * y ) * z ) (FMap F (λ f → FMap (Monad.T monad) (λ g → f , g) c) (μ (x * y ) (FMap F (λ f → FMap F (λ g → f , g) b) a))))) + (μ ( ( x * y ) * z ) (FMap F (λ f → FMap F (λ g → f , g) c) (μ (x * y ) (FMap F (λ f → FMap F (λ g → f , g) b) a))))) ≈⟨⟩ ( λ a → FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) ) ∎ ) where