Mercurial > hg > Members > kono > Proof > category
changeset 744:c8e9786c273a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 08 Dec 2017 17:51:33 +0900 |
| parents | e33e9ae1514b |
| children | 9dbbbb295a09 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 26 insertions(+), 15 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Tue Dec 05 17:04:03 2017 +0900 +++ b/monad→monoidal.agda Fri Dec 08 17:51:33 2017 +0900 @@ -91,21 +91,32 @@ → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) assocφ = {!!} idrφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ≡ x - idrφ {a} {x} = begin - FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) - ≡⟨⟩ - FMap F proj₁ (μ (a * One) (FMap F (λ f → FMap F (λ g → f , g) (η One OneObj)) x)) - ≡⟨ {!!} ⟩ - FMap F proj₁ (μ (a * One) (FMap F (λ f → η ( a * One ) (f , OneObj ) ) x ) ) - ≡⟨ {!!} ⟩ - FMap F proj₁ ( FMap F (λ f → {!!}) ( μ {!!} (η {!!} x ) ) ) - ≡⟨ {!!} ⟩ - id1 Sets {!!} x - ≡⟨ {!!} ⟩ - x - ∎ where - open Relation.Binary.PropositionalEquality - open Relation.Binary.PropositionalEquality.≡-Reasoning + idrφ {a} {x} = monoidal.≡-cong ( λ h → h x ) ( begin + ( λ x → FMap F (Iso.≅→ (mρ-iso isM)) (φ (x , unit)) ) + ≈⟨⟩ + ( λ x → FMap F proj₁ (μ (a * One) (FMap F (λ f → FMap F (λ g → f , g) (η One OneObj)) x)) ) + ≈⟨⟩ + ( λ x → FMap F proj₁ ((μ (a * One) o (FMap F (λ f → FMap F (λ g → f , g) (η One OneObj)))) x)) + ≈⟨⟩ + ( λ x → ( FMap F proj₁ o ( (μ (a * One ) o λ y → FMap F (λ f → FMap F ( λ g → ( f , g )) y ) x ) o η One )) OneObj ) + ≈⟨ {!!} ⟩ + ( λ x → ( FMap F proj₁ o (( μ ( a * One ) o FMap F {!!} ) o η (FObj F a ))) x ) + ≈⟨⟩ + FMap F proj₁ o (( μ ( a * One ) o FMap F {!!} ) o η (FObj F a )) + ≈⟨ cdr ( car (nat ( Monad.μ monad ))) ⟩ + FMap F proj₁ o (( FMap F {!!} o μ a ) o η (FObj F a )) + ≈⟨ cdr assoc ⟩ + FMap F proj₁ o ( FMap F {!!} o ( μ a o η (FObj F a ))) + ≈⟨ {!!} ⟩ + FMap F proj₁ o ( FMap F {!!} o id1 Sets (FObj F a ) ) + ≈⟨ cdr idR ⟩ + FMap F proj₁ o FMap F (λ z → z , {!!} ) + ≈↑⟨ distr F ⟩ + FMap F (id1 Sets a ) + ≈⟨ IsFunctor.identity ( Functor.isFunctor F ) ⟩ + id1 Sets (FObj F a) + ∎ ) where + open ≈-Reasoning Sets hiding ( _o_ ) idlφ : {a : Obj Sets } { x : FObj F a } → FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , x)) ≡ x idlφ = {!!}