Mercurial > hg > Members > kono > Proof > category
changeset 753:b7d804370c1d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 10 Dec 2017 23:19:37 +0900 |
| parents | e7ace77d7235 |
| children | f01e8d16a85d |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 20 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 22:26:01 2017 +0900 +++ b/monad→monoidal.agda Sun Dec 10 23:19:37 2017 +0900 @@ -95,27 +95,27 @@ ( λ 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) o ( μ (y * z ) o FMap F (λ f₁ → FMap F (λ g → f₁ , g) c ) )) b )) - ≈⟨ {!!} ⟩ -- assoc + ≈⟨⟩ -- 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 + ≈⟨⟩ -- 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 + ≈⟨ {!!} ⟩ -- 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 + ≈⟨ cdr {_} {_} {_} {_} {_} {μ ( x * ( y * z ) )} ( distr F ) ⟩ -- 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 + ≈⟨⟩ -- 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 + ≈↑⟨ car ( IsMonad.assoc ( Monad.isMonad monad )) ⟩ --- 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 ) @@ -126,43 +126,42 @@ ≈⟨⟩ 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 (λ 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 (λ f → FMap F (λ g → f , g) b) ) + ≈⟨ distr F ⟩ 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 + ≈⟨⟩ -- 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 + ≈⟨⟩ -- 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 ))) ⟩ - ≈⟨ {!!} ⟩ + ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ ( x * ( y * z ))} (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 + ≈⟨⟩ --- 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 + ≈⟨ cdr {_} {_} {_} {_} {_} {μ ( x * ( y * z ))} ( car ( distr F )) ⟩ μ ( 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 + ≈⟨⟩ -- 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 + ≈⟨⟩ -- 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 μ + ≈↑⟨ car ( nat ( Monad.μ monad ) ) ⟩ (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 F (λ g → f , g) c) o (μ (x * y ) o (FMap F (λ f → FMap F (λ g → f , g) b) )))) ≈⟨⟩ @@ -204,7 +203,7 @@ FMap F proj₁ o (μ (a * One ) o FMap F ( η (a * One ) o ( λ f → ( f , OneObj )))) ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( cdr {_} {_} {_} {_} {_} {μ (a * One )} ( distr F )) ⟩ FMap F proj1 o (μ (a * One ) o ( FMap F ( η (a * One )) o FMap F ( λ f → ( f , OneObj )))) - ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( assoc {_} {_} {_} {_} { μ (a * One )} { FMap F ( η (a * One ))} {FMap F ( λ f → ( f , OneObj ))} ) ⟩ + ≈⟨⟩ FMap F proj1 o ( ( μ (a * One ) o FMap F ( η (a * One ))) o FMap F ( λ f → ( f , OneObj ))) ≈⟨ cdr {_} {_} {_} {_} {_} {FMap F proj₁} ( car ( IsMonad.unity2 (Monad.isMonad monad ))) ⟩ FMap F proj₁ o ( id1 Sets (FObj F (a * One)) o FMap F ( λ f → ( f , OneObj )))