Mercurial > hg > Members > kono > Proof > category
changeset 778:06388660995b
fix applicative for Agda version 2.5.4.1
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 26 Sep 2018 20:17:09 +0900 |
| parents | 5160b431f1de |
| children | 6b4bd02efd80 |
| files | applicative.agda discrete.agda limit-to.agda monad→monoidal.agda |
| diffstat | 4 files changed, 25 insertions(+), 26 deletions(-) [+] |
line wrap: on
line diff
--- a/applicative.agda Wed Sep 26 10:00:02 2018 +0900 +++ b/applicative.agda Wed Sep 26 20:17:09 2018 +0900 @@ -217,12 +217,7 @@ ≡⟨ sym ( left ( left comp )) ⟩ (((( pure _・_ <*> (pure (λ f → f (λ j k → j , k)))) <*> (pure (λ f g x y → f , g x y))) <*> a ) <*> b) <*> c ≡⟨ trans (left ( left (left (left p*p) ))) (left (left (left p*p ) )) ⟩ - ((pure (( _・_ (λ f → f (λ j k → j , k))) (λ f g x y → f , g x y)) <*> a ) <*> b) <*> c - ≡⟨⟩ (((pure (λ f g h → f , g , h)) <*> a) <*> b) <*> c - ≡⟨⟩ - ((pure ((_・_ ((_・_ ((_・_ ( (λ abc → proj₁ (proj₁ abc) , proj₂ (proj₁ abc) , proj₂ abc))))))) - (( _・_ ( _・_ ((λ j k → j , k)))) (λ j k → j , k))) <*> a) <*> b) <*> c ≡⟨ sym (trans ( left ( left ( left (left (right (right p*p))) ) )) (trans (left (left( left (left (right p*p))))) (trans (left (left (left (left p*p)))) (trans ( left (left (left (right (left (right p*p )))))) (trans (left (left (left (right (left p*p))))) (trans (left (left (left (right p*p)))) (left (left (left p*p)))) ) ) ) @@ -426,11 +421,11 @@ (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φ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)) + (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → 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)) (φ - (FMap F ( λ x → (λ r → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩ + (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) k , v)) , w)) ) ) φunitr ⟩ 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)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) + ( (FMap F ( λ x → (λ (r : ((b → c) → _ ) * (b → c) ) → proj₁ r (proj₂ r)) ((map (λ y f g x → f (g x)) id ) x)) (FMap F (Iso.≅← (mλ-iso isM)) u) ) , v)) , w)) ≡⟨ ≡-cong ( λ k → FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ (k u , v)) , w)) ) (sym ( IsFunctor.distr (isFunctor F ))) ⟩ FMap F (λ r → proj₁ r (proj₂ r)) (φ (FMap F (λ r → proj₁ r (proj₂ r)) (φ
--- a/discrete.agda Wed Sep 26 10:00:02 2018 +0900 +++ b/discrete.agda Wed Sep 26 20:17:09 2018 +0900 @@ -92,37 +92,31 @@ -- Category with no arrow but identity -record DiscreteObj {c₁ : Level } (S : Set c₁) : Set c₁ where - field - obj : S -- this is necessary to avoid single object - -open DiscreteObj - -record DiscreteHom { c₁ : Level} { S : Set c₁} (a : DiscreteObj {c₁} S) (b : DiscreteObj {c₁} S) +record DiscreteHom { c₁ : Level} { S : Set c₁} (a : S) (b : S) : Set c₁ where field discrete : a ≡ b -- if f : a → b then a ≡ b - dom : DiscreteObj S + dom : S dom = a open DiscreteHom -_*_ : ∀ {c₁} → {S : Set c₁} {a b c : DiscreteObj {c₁} S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c +_*_ : ∀ {c₁} → {S : Set c₁} {a b c : S} → DiscreteHom {c₁} b c → DiscreteHom {c₁} a b → DiscreteHom {c₁} a c _*_ {_} {a} {b} {c} x y = record {discrete = trans ( discrete y) (discrete x) } -DiscreteId : { c₁ : Level} { S : Set c₁} ( a : DiscreteObj {c₁} S ) → DiscreteHom {c₁} a a +DiscreteId : { c₁ : Level} { S : Set c₁} ( a : S ) → DiscreteHom {c₁} a a DiscreteId a = record { discrete = refl } open import Relation.Binary.PropositionalEquality -assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : DiscreteObj {c₁} S} +assoc-* : {c₁ : Level } { S : Set c₁} {a b c d : S} {f : (DiscreteHom c d )} → {g : (DiscreteHom b c )} → {h : (DiscreteHom a b )} → dom ( f * (g * h)) ≡ dom ((f * g) * h ) assoc-* {c₁} {S} {a} {b} {c} {d} {f} {g} {h } = refl DiscreteCat : {c₁ : Level } → (S : Set c₁) → Category c₁ c₁ c₁ DiscreteCat {c₁} S = record { - Obj = DiscreteObj {c₁} S ; + Obj = S ; Hom = λ a b → DiscreteHom {c₁} {S} a b ; _o_ = λ{a} {b} {c} x y → _*_ {c₁ } {S} {a} {b} {c} x y ; _≈_ = λ x y → dom x ≡ dom y ; -- x ≡ y does not work because refl ≡ discrete f is failed as it should be @@ -135,11 +129,11 @@ associative = λ{a b c d f g h } → assoc-* { c₁} {S} {a} {b} {c} {d} {f} {g} {h} } } where - identityL : {a b : DiscreteObj {c₁} S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f + identityL : {a b : S} {f : ( DiscreteHom {c₁} a b) } → dom ((DiscreteId b) * f) ≡ dom f identityL {a} {b} {f} = refl - identityR : {A B : DiscreteObj S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f + identityR : {A B : S} {f : ( DiscreteHom {c₁} A B) } → dom ( f * DiscreteId A ) ≡ dom f identityR {a} {b} {f} = refl - o-resp-≈ : {A B C : DiscreteObj S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → + o-resp-≈ : {A B C : S } {f g : ( DiscreteHom {c₁} A B)} {h i : ( DiscreteHom B C)} → dom f ≡ dom g → dom h ≡ dom i → dom ( h * f ) ≡ dom ( i * g ) o-resp-≈ {a} {b} {c} {f} {g} {h} {i} refl refl = refl
--- a/limit-to.agda Wed Sep 26 10:00:02 2018 +0900 +++ b/limit-to.agda Wed Sep 26 20:17:09 2018 +0900 @@ -248,7 +248,7 @@ → ( Γ : Functor (DiscreteCat S ) A ) → (lim : Limit ( DiscreteCat S ) A Γ ) → Obj A plimit A S Γ lim = a0 lim -discrete-identity : { c₁ : Level} { S : Set c₁} { a : DiscreteObj {c₁} S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ] +discrete-identity : { c₁ : Level} { S : Set c₁} { a : S } → (f : DiscreteHom a a ) → (DiscreteCat S) [ f ≈ id1 (DiscreteCat S) a ] discrete-identity f = refl pnat : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (S : Set c₁) @@ -277,7 +277,7 @@ ∎ lim-to-product : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ( S : Set c₁ ) - → ( Γ : Functor (DiscreteCat S) A ) + → ( Γ : Functor (DiscreteCat S) A ) -- could be constructed from S → Obj A → (lim : Limit (DiscreteCat S) A Γ ) → IProduct (Obj (DiscreteCat S)) A (FObj Γ) lim-to-product A S Γ lim = record {
--- a/monad→monoidal.agda Wed Sep 26 10:00:02 2018 +0900 +++ b/monad→monoidal.agda Wed Sep 26 20:17:09 2018 +0900 @@ -62,7 +62,17 @@ 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 (λ xy → f (proj₁ xy) , g (proj₂ xy)) (FMap F (λ g₁ → x₁ , g₁) y) ) + ≈⟨⟩ + ( λ x₁ → ( FMap F (λ xy → f (proj₁ xy) , g (proj₂ xy)) o FMap F (λ g₁ → x₁ , g₁) ) y ) + ≈↑⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( extensionality Sets ( λ x₁ → distr F )) ⟩ + ( λ x₁ → FMap F (λ g₁ → ( λ xy → f (proj₁ xy) , g (proj₂ xy)) (x₁ , g₁)) y ) + ≈⟨⟩ + ( λ x₁ → FMap F (λ g₁ → f x₁ , g g₁) y ) + ≈⟨ monoidal.≡-cong ( λ h → λ x₁ → h x₁ y ) ( extensionality Sets ( λ x₁ → distr F )) ⟩ + ( λ x₁ → ( FMap F (λ g₁ → f x₁ , g₁) o FMap F g ) y ) + ≈⟨⟩ ( λ x₁ → FMap F (λ g₁ → f x₁ , g₁) (FMap F g y) ) ∎ ) ) ) ⟩