Mercurial > hg > Members > kono > Proof > category
changeset 73:b75b5792bd81
on going
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 26 Jul 2013 15:52:24 +0900 |
| parents | cbc30519e961 |
| children | 49e6eb3ef9c0 |
| files | nat.agda |
| diffstat | 1 files changed, 26 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/nat.agda Fri Jul 26 12:38:54 2013 +0900 +++ b/nat.agda Fri Jul 26 15:52:24 2013 +0900 @@ -92,36 +92,27 @@ open Kleisli -- η(b) ○ f = f -Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) → - { T : Functor A A } - ( η : NTrans A A identityFunctor T ) - { μ : NTrans A A (T ○ T) T } - { a : Obj A } ( b : Obj A ) - ( f : Hom A a ( FObj T b) ) - ( m : Monad A T η μ ) - { k : Kleisli A T η μ m} - → A [ join k (TMap η b) f ≈ f ] -Lemma7 c {T} η b f m {k} = - let open ≈-Reasoning (c) - μ = mu ( monad k ) - in +Lemma7 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) ) + → A [ join K (TMap η b) f ≈ f ] +Lemma7 {_} {b} f = + let open ≈-Reasoning (A) in begin - join k (TMap η b) f + join K (TMap η b) f ≈⟨ refl-hom ⟩ - c [ TMap μ b o c [ FMap T ((TMap η b)) o f ] ] - ≈⟨ IsCategory.associative (Category.isCategory c) ⟩ - c [ c [ TMap μ b o FMap T ((TMap η b)) ] o f ] - ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad k )) ) ⟩ - c [ id (FObj T b) o f ] - ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩ + A [ TMap μ b o A [ FMap T ((TMap η b)) o f ] ] + ≈⟨ IsCategory.associative (Category.isCategory A) ⟩ + A [ A [ TMap μ b o FMap T ((TMap η b)) ] o f ] + ≈⟨ car ( IsMonad.unity2 ( isMonad ( monad K )) ) ⟩ + A [ id (FObj T b) o f ] + ≈⟨ IsCategory.identityL (Category.isCategory A) ⟩ f ∎ -- f ○ η(a) = f -Lemma8 : ( a : Obj A ) ( b : Obj A ) +Lemma8 : { a : Obj A } { b : Obj A } ( f : Hom A a ( FObj T b) ) → A [ join K f (TMap η a) ≈ f ] -Lemma8 a b f = +Lemma8 {a} {b} f = begin join K f (TMap η a) ≈⟨ refl-hom ⟩ @@ -139,11 +130,11 @@ -- h ○ (g ○ f) = (h ○ g) ○ f Lemma9 : { a b c d : Obj A } - ( f : Hom A a ( FObj T b) ) + ( h : Hom A c ( FObj T d) ) ( g : Hom A b ( FObj T c) ) - ( h : Hom A c ( FObj T d) ) + ( f : Hom A a ( FObj T b) ) → A [ join K h (join K g f) ≈ join K ( join K h g) f ] -Lemma9 {a} {b} {c} {d} f g h = +Lemma9 {a} {b} {c} {d} h g f = begin join K h (join K g f) ≈⟨⟩ @@ -197,9 +188,6 @@ join K ( join K h g) f ∎ where open ≈-Reasoning (A) -KHom1 : (a : Obj A) → (b : Obj A) -> Set (c₂ ⊔ c₁) -KHom1 = {!!} - record KHom (a : Obj A) (b : Obj A) : Set (suc (c₂ ⊔ c₁)) where field @@ -209,12 +197,10 @@ K-id {a = a} = record { KMap = TMap η a } open import Relation.Binary.Core +open KHom -_⋍_ : - { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set (suc ((c₂ ⊔ c₁) ⊔ ℓ)) -_⋍_ = {!!} - -open KHom +_⋍_ : { a : Obj A } { b : Obj A } (f g : KHom a b ) -> Set ℓ -- (suc ((c₂ ⊔ c₁) ⊔ ℓ)) +_⋍_ {a} {b} f g = A [ KMap f ≈ KMap g ] _*_ : { a b : Obj A } → { c : Obj A } → ( KHom b c) → ( KHom a b) → KHom a c @@ -228,6 +214,7 @@ ; associative = Kassoc } where + open ≈-Reasoning (A) isEquivalence : { a b : Obj A } -> IsEquivalence {_} {_} {KHom a b} _⋍_ isEquivalence {C} {D} = @@ -236,20 +223,20 @@ ; trans = λ {F} {G} {H} → ⋍-trans {F} {G} {H} } where ⋍-refl : {F : KHom C D} → F ⋍ F - ⋍-refl = {!!} + ⋍-refl = refl-hom ⋍-sym : {F G : KHom C D} → F ⋍ G → G ⋍ F - ⋍-sym = {!!} + ⋍-sym = sym ⋍-trans : {F G H : KHom C D} → F ⋍ G → G ⋍ H → F ⋍ H - ⋍-trans = {!!} + ⋍-trans = trans-hom KidL : {C D : Obj A} -> {f : KHom C D} → (K-id * f) ⋍ f - KidL = {!!} + KidL {_} {_} {f} = Lemma7 (KMap f) KidR : {C D : Obj A} -> {f : KHom C D} → (f * K-id) ⋍ f - KidR = {!!} + KidR {_} {_} {f} = Lemma8 (KMap f) Ko-resp : {a b c : Obj A} -> {f g : KHom a b } → {h i : KHom b c } → f ⋍ g → h ⋍ i → (h * f) ⋍ (i * g) Ko-resp = {!!} Kassoc : {a b c d : Obj A} -> {f : KHom c d } → {g : KHom b c } → {h : KHom a b } → (f * (g * h)) ⋍ ((f * g) * h) - Kassoc = {!!} + Kassoc {_} {_} {_} {_} {f} {g} {h} = Lemma9 (KMap f) (KMap g) (KMap h)