Mercurial > hg > Members > kono > Proof > category
changeset 717:a41b2b9b0407
Haskell Monoidal Funtor to Applicative done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 24 Nov 2017 14:26:01 +0900 |
| parents | 35457f9568f3 |
| children | f2e617dc2c21 |
| files | monoidal.agda |
| diffstat | 1 files changed, 61 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/monoidal.agda Fri Nov 24 13:20:14 2017 +0900 +++ b/monoidal.agda Fri Nov 24 14:26:01 2017 +0900 @@ -542,16 +542,17 @@ _<*>_ {a} {b} x y = FMap F ( λ r → ( proj₁ r ) ( proj₂ r ) ) (φ ( x , y )) _・_ : { a b c : Obj (Sets {c₁} ) } → (b → c) → (a → b) → a → c _・_ f g = λ x → f ( g x ) - left : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y - left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq + -- left does not work right it makes yellows. why? + -- left : {n : Level} { a b : Set n} → { x y : a } { h : a → b } → ( x ≡ y ) → h x ≡ h y + -- left {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → h k ) eq right : {n : Level} { a b : Set n} → { x y : a → b } { h : a } → ( x ≡ y ) → x h ≡ y h right {_} {_} {_} {_} {_} {h} eq = ≡-cong ( λ k → k h ) eq open Relation.Binary.PropositionalEquality - φ→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } + FφF→F : { a b c d e : Obj Sets } { g : Hom Sets a c } { h : Hom Sets b d } { f : Hom Sets (c * d) e } { x : FObj F a } { y : FObj F b } → FMap F f ( φ ( FMap F g x , FMap F h y ) ) ≡ FMap F ( f o map g h ) ( φ ( x , y ) ) - φ→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin + FφF→F {a} {b} {c} {d} {e} {g} {h} {f} {x} {y} = sym ( begin FMap F ( f o map g h ) ( φ ( x , y ) ) ≡⟨ ≡-cong ( λ k → k ( φ ( x , y ))) ( IsFunctor.distr (isFunctor F) ) ⟩ FMap F f (( FMap F ( map g h ) ) ( φ ( x , y ))) @@ -602,7 +603,7 @@ ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , u ) ) ≡⟨ ≡-cong ( λ k → ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , k ))) u→F ⟩ ( FMap F ( λ r → ( proj₁ r ) ( proj₂ r )) ) ( φ ( FMap F ( λ y → id ) unit , FMap F id u ) ) - ≡⟨ φ→F ⟩ + ≡⟨ FφF→F ⟩ FMap F (λ x → proj₂ x ) (φ (unit , u ) ) ≡⟨⟩ FMap F (Iso.≅→ (mλ-iso isM)) (φ (unit , u )) @@ -619,7 +620,7 @@ ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , k)) , v)) , w)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f g x → f (g x)) unit , FMap F id u )) , v)) , w)) - ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) φ→F ⟩ + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( k , v)) , w)) ) FφF→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (φ ( unit , u)) , v)) , w)) ≡⟨ ≡-cong ( λ k → ( FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ @@ -635,13 +636,13 @@ ( FMap F (λ x g h → x (g h) ) u , v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ ( FMap F (λ x g h → x (g h) ) u , k)) , w)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x g h → x (g h)) u , FMap F id v)) , w)) - ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) φ→F ⟩ + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , w)) ) FφF→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x g h → x (g h)) id) (φ (u , v)) , w)) ≡⟨⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , k)) ) u→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ x h → proj₁ x (proj₂ x h)) (φ (u , v)) , FMap F id w)) - ≡⟨ φ→F ⟩ + ≡⟨ FφF→F ⟩ FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ x h → proj₁ x (proj₂ x h)) id) (φ (φ (u , v) , w)) ≡⟨⟩ FMap F (λ x → proj₁ (proj₁ x) (proj₂ (proj₁ x) (proj₂ x))) (φ (φ (u , v) , w)) @@ -661,7 +662,7 @@ FMap F (λ y → proj₁ y (proj₁ (proj₂ y) (proj₂ (proj₂ y)))) (φ (u , φ (v , w))) ≡⟨⟩ FMap F ( λ x → (proj₁ x) ((λ r → proj₁ r (proj₂ r)) ( proj₂ x))) ( φ ( u , (φ (v , w)))) - ≡⟨ sym φ→F ⟩ + ≡⟨ sym FφF→F ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) ) (sym u→F ) ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ r → proj₁ r (proj₂ r)) (φ (v , w)))) @@ -669,6 +670,55 @@ where open Relation.Binary.PropositionalEquality.≡-Reasoning homomorphism : { a b : Obj Sets } { f : Hom Sets a b } { x : a } → pure f <*> pure x ≡ pure (f x) - homomorphism = {!!} + homomorphism {a} {b} {f} {x} = begin + pure f <*> pure x + ≡⟨⟩ + FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y → f) unit , FMap F (λ y → x) unit)) + ≡⟨ FφF→F ⟩ + FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y → f) (λ y → x)) (φ (unit , unit)) + ≡⟨⟩ + FMap F (λ y → f x) (φ (unit , unit)) + ≡⟨ ≡-cong ( λ k → FMap F (λ y → f x) k ) φunitl ⟩ + FMap F (λ y → f x) (FMap F (Iso.≅← (mρ-iso isM)) unit) + ≡⟨⟩ + FMap F (λ y → f x) (FMap F (λ y → (y , OneObj)) unit) + ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F ))) ⟩ + FMap F (λ y → f x) unit + ≡⟨⟩ + pure (f x) + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning interchange : { a b : Obj Sets } { u : FObj F ( a → b ) } { x : a } → u <*> pure x ≡ pure (λ f → f x) <*> u - interchange = {!!} + interchange {a} {b} {u} {x} = begin + u <*> pure x + ≡⟨⟩ + FMap F (λ r → proj₁ r (proj₂ r)) (φ (u , FMap F (λ y → x) unit)) + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (k , FMap F (λ y → x) unit)) ) u→F ⟩ + FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F id u , FMap F (λ y → x) unit)) + ≡⟨ FφF→F ⟩ + FMap F ((λ r → proj₁ r (proj₂ r)) o map id (λ y → x)) (φ (u , unit)) + ≡⟨⟩ + FMap F (λ r → proj₁ r x) (φ (u , unit)) + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r x) k ) φunitl ⟩ + FMap F (λ r → proj₁ r x) (( FMap F (Iso.≅← (mρ-iso isM))) u ) + ≡⟨ right ( sym ( IsFunctor.distr (isFunctor F )) ) ⟩ + FMap F (( λ r → proj₁ r x) o ((Iso.≅← (mρ-iso isM) ))) u + ≡⟨⟩ + FMap F (( λ r → proj₂ r x) o ((Iso.≅← (mλ-iso isM) ))) u + ≡⟨ right ( IsFunctor.distr (isFunctor F )) ⟩ + FMap F (λ r → proj₂ r x) (FMap F (Iso.≅← (IsMonoidal.mλ-iso isM)) u) + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₂ r x) k ) (sym φunitr ) ⟩ + FMap F (λ r → proj₂ r x) (φ (unit , u)) + ≡⟨⟩ + FMap F ((λ r → proj₁ r (proj₂ r)) o map (λ y f → f x) id) (φ (unit , u)) + ≡⟨ sym FφF→F ⟩ + FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , FMap F id u)) + ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , k)) ) (sym u→F) ⟩ + FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ y f → f x) unit , u)) + ≡⟨⟩ + pure (λ f → f x) <*> u + ∎ + where + open Relation.Binary.PropositionalEquality.≡-Reasoning +