Mercurial > hg > Members > kono > Proof > category
changeset 754:f01e8d16a85d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 11 Dec 2017 01:45:18 +0900 |
| parents | b7d804370c1d |
| children | a1c3d82be8c8 |
| files | monad→monoidal.agda |
| diffstat | 1 files changed, 11 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/monad→monoidal.agda Sun Dec 10 23:19:37 2017 +0900 +++ b/monad→monoidal.agda Mon Dec 11 01:45:18 2017 +0900 @@ -87,6 +87,11 @@ ∎ where open Relation.Binary.PropositionalEquality open Relation.Binary.PropositionalEquality.≡-Reasoning + ≡←≈ : {a b : Obj (Sets {l}) } { x y : Hom (Sets {l}) a b } → (x≈y : Sets [ x ≈ y ]) → x ≡ y + ≡←≈ refl = refl + fcongλ : { a b c : Obj (Sets {l} ) } { x y : a → Hom (Sets {l}) a b } → Sets [ x ≈ y ] + → Sets [ FMap F ( λ (f : a) → ( x f )) ≈ FMap F ( λ (f : a ) → ( y f )) ] + fcongλ {a} {b} {c} {x} {y} eq = let open ≈-Reasoning (Sets {l}) hiding ( _o_ ) in fcong F eq assocφ : { x y z : Obj Sets } { a : FObj F x } { b : FObj F y }{ c : FObj F z } → φ (a , φ (b , c)) ≡ FMap F (Iso.≅→ (mα-iso isM)) (φ (φ (a , b) , c)) assocφ {x} {y} {z} {a} {b} {c} = monoidal.≡-cong ( λ h → h a ) ( begin @@ -97,15 +102,16 @@ μ ( 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 )) - ≈⟨ {!!} ⟩ - μ ( 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 + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) + ( car {_} {_} {_} {_} {_} { FMap F (λ f₁ → FMap F (λ g → f₁ , g) c )} (nat (Monad.μ monad ))) ) )) ⟩ + μ ( 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 + ≈↑⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ f → monoidal.≡-cong ( λ h → h b ) + ( cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) )} (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 + ≈⟨ cdr {_} {_} {_} {_} {_} { μ ( x * ( y * z ) ) } (fcong F (extensionality Sets (λ 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 ))