Mercurial > hg > Members > kono > Proof > category
changeset 1119:4e7513a4229a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Jul 2024 17:33:36 +0900 |
| parents | 939dd4cdfea4 |
| children | 121e28cccdf6 |
| files | src/monad→monoidal.agda |
| diffstat | 1 files changed, 5 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/src/monad→monoidal.agda Sat Jul 06 09:41:27 2024 +0900 +++ b/src/monad→monoidal.agda Sat Jul 06 17:33:36 2024 +0900 @@ -85,13 +85,11 @@ FMap T (λ g → f , g) (φ (b , c)) ≡⟨ refl ⟩ FMap T (λ g → f , g) (TMap μ (Σ y (λ v → z)) (FMap T (λ f → FMap T (λ g → f , g) c) b)) ≡⟨ nat μ (FMap T (λ f → FMap T (λ g → (f , g)) c) b) ⟩ - TMap μ (x * y * z) (FMap T (FMap T (λ g → f , g)) (FMap T (λ f → FMap T (λ g → f , g) c) b)) - ≡⟨ ? ⟩ - TMap μ ( x * ( y * z ) ) ( ( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b) - ≡⟨ sym ( cong (λ k → TMap μ (x * y * z) k ) (fcong b (λ w → sym (fdistr c) ) ) ) ⟩ - TMap μ (x * y * z) (FMap T (λ z₁ → FMap T ? (FMap T ? c)) b) ≡⟨ ? ⟩ - TMap μ (x * y * z) (FMap T (λ z₁ → FMap T (λ z₂ → ?) ? ) a ) ≡⟨ cong (λ k → TMap μ (x * y * z) k ) (fcong ? (λ x → fdistr ? ) ) ⟩ - TMap μ (x * y * z) ? ∎ ) ) ⟩ + TMap μ (x * y * z) (FMap T (FMap T (λ g → f , g)) (FMap T (λ f → FMap T (λ g → f , g) c) b)) + ≡⟨ sym (cong (λ k → TMap μ (x * y * z) k) (fdistr b )) ⟩ + TMap μ (x * y * z) (FMap T ((λ f₁ → (FMap T (λ g → f , g) (FMap T (λ g → f₁ , g) c )))) b) + ≡⟨ sym (cong (λ k → TMap μ (x * y * z) k ) (fcong b (λ x → fdistr c ) )) ⟩ + TMap μ (x * y * z) (( FMap T (λ g → (FMap T (λ h → f , (g , h))) c)) b ) ∎ ) ) ⟩ ? ≡⟨ ? ⟩ TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) (FMap T (λ h → ? h) b)) ≡⟨ cong (λ k → TMap μ (x * y * z) (FMap T (TMap μ (x * y * z)) k )) ? ⟩