Mercurial > hg > Members > kono > Proof > category
changeset 773:60942538dc41
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 29 Dec 2017 11:32:19 +0900 |
| parents | b7a774977345 |
| children | f3a493da92e8 |
| files | README.txt applicative.agda monad→monoidal.agda monoid-monad.agda |
| diffstat | 4 files changed, 58 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/README.txt Wed Dec 13 09:34:45 2017 +0900 +++ b/README.txt Fri Dec 29 11:32:19 2017 +0900 @@ -21,7 +21,6 @@ list-monoid-cat.agda list-nat.agda list-nat0.agda - maybe-monad.agda maybeCat.agda monoid-monad.agda @@ -34,6 +33,8 @@ adj-monad.agda comparison-em.agda comparison-functor.agda + maybe-monad.agda + maybeCat.agda -- Limit @@ -41,16 +42,28 @@ universal-mapping.agda free-monoid.agda CatExponetial.agda - pullback.agda + pullback.agda -- including limit from product and equalizer discrete.agda limit-to.agda + SetsCompleteness.agda + +-- Freyd Adjoint Functor Theorem + + Comma.agda + Comma1.agda + freyd.agda + freyd1.agda + freyd2.agda + +-- Monoidal functor and Applicative + + monoidal.agda -- Monoidal category and Functor + applicative.agda -- Applicative functor is a monoidal functor + monad→monoidal.agda -- no yet finished - freyd.agda - Comma.agda - linton.agda - -- repositories https://bitbucket.org/shinji_kono/category-exercise-in-agda/src +
--- a/applicative.agda Wed Dec 13 09:34:45 2017 +0900 +++ b/applicative.agda Fri Dec 29 11:32:19 2017 +0900 @@ -315,7 +315,7 @@ ---- -- --- Monoidal laws imples Applicative laws +-- Monoidal laws implies Applicative laws -- HaskellMonoidal→Applicative : {c₁ : Level} ( F : Functor (Sets {c₁}) (Sets {c₁}) )
--- a/monad→monoidal.agda Wed Dec 13 09:34:45 2017 +0900 +++ b/monad→monoidal.agda Fri Dec 29 11:32:19 2017 +0900 @@ -46,6 +46,38 @@ open IsMonoidal id : { a : Obj (Sets {l}) } → a → a id x = x + natφ' : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } + → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) + natφ' {a} {b} {c} {d} {x} {y} {f} {g} = monoidal.≡-cong ( λ h → h x ) ( begin + ( λ x → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) ・ (μ (Σ a (λ k → b)))) ( FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) x )) + ≈⟨⟩ + (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (μ (Σ a (λ k → b)))) o FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) + ≈⟨ car {_} {_} {_} {_} {_} {FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)} ( nat (Monad.μ monad) ) ⟩ + ( μ ( c * d) o FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)))) o FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) + ≈↑⟨ cdr {_} {_} {_} {_} {_} {μ ( c * d)} ( distr F ) ⟩ + μ ( c * d) o FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) ) + ≈⟨ cdr {_} {_} {_} {_} {_} {μ ( c * d)} ( begin + FMap F (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y) ) + ≈⟨⟩ + FMap F (λ x₁ → (FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y)) x₁) + ≈⟨ fcong F ( extensionality Sets ( λ x₁ → monoidal.≡-cong ( λ h → h x₁ ) ( begin + FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o (λ f₁ → FMap F (λ g₁ → f₁ , g₁) y ) + ≈⟨ {!!} ⟩ + ( λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y) ) + ∎ + ) ) ) ⟩ + FMap F (λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y)) + ≈⟨⟩ + FMap F ( (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o f ) + ≈⟨ distr F ⟩ + FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o (FMap F f ) + ∎ + ) ⟩ + μ ( c * d) o (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) o (FMap F f )) + ≈⟨⟩ + ( λ x → μ (Σ c (λ x₁ → d)) (FMap F (λ f₁ → FMap F (λ g₁ → f₁ , g₁) (FMap F g y)) (FMap F f x))) + ∎ ) where + open ≈-Reasoning Sets hiding ( _o_ ) natφ : { a b c d : Obj Sets } { x : FObj F a} { y : FObj F b} { f : a → c } { g : b → d } → FMap F (map f g) (φ (x , y)) ≡ φ (FMap F f x , FMap F g y) natφ {a} {b} {c} {d} {x} {y} {f} {g} = begin
--- a/monoid-monad.agda Wed Dec 13 09:34:45 2017 +0900 +++ b/monoid-monad.agda Fri Dec 29 11:32:19 2017 +0900 @@ -122,9 +122,12 @@ Lemma-MM11 : (λ x y z → ((M ∙ (M ∙ x) y) z)) ≡ (λ x y z → ( _∙_ M x (_∙_ M y z ) )) Lemma-MM11 = extensionality30 Lemma-MM36 -MonoidMonad : Monad A T η μ +MonoidMonad : Monad A MonoidMonad = record { - isMonad = record { + T = T + ; η = η + ; μ = μ + ; isMonad = record { unity1 = Lemma-MM3 ; unity2 = Lemma-MM4 ; assoc = Lemma-MM5 @@ -181,7 +184,7 @@ Lemma-MM12 = Monad.join MonoidMonad (F m f) (F m' g) -open import kleisli {_} {_} {_} {A} {T} {η} {μ} {MonoidMonad} +open import kleisli {_} {_} {_} {A} {T} {η} {μ} {Monad.isMonad MonoidMonad} -- nat-ε TMap = λ a₁ → record { KMap = λ x → x } -- nat-η TMap = λ a₁ → _,_ (ε, M)