Mercurial > hg > Members > kono > Proof > category
changeset 104:53a79dfdcd04
problem written
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 31 Jul 2013 16:33:59 +0900 |
| parents | 8dcf926482af |
| children | b881dbc47684 |
| files | em-category.agda |
| diffstat | 1 files changed, 27 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/em-category.agda Wed Jul 31 15:42:38 2013 +0900 +++ b/em-category.agda Wed Jul 31 16:33:59 2013 +0900 @@ -31,7 +31,7 @@ -- open Functor open NTrans -record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where +record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where obj : Obj A obj = a phi : Hom A (FObj T a) a @@ -41,17 +41,20 @@ eval : A [ A [ φ o TMap μ a ] ≈ A [ φ o FMap T φ ] ] open IsEMAlgebra -record EMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where +record EMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (c₁ ⊔ c₂ ⊔ ℓ) where field isEMAlbgebra : IsEMAlgebra a φ open EMAlgebra -data EMObj {a : Obj A} {φ : Hom A (FObj T a) a } : Set (suc ( c₁ ⊔ c₂ ⊔ ℓ)) where +data EMObj {a : Obj A} {φ : Hom A (FObj T a) a } : Set ( c₁ ⊔ c₂ ⊔ ℓ) where emObj : (IsEMAlgebra a φ) -> EMObj {a} {φ} emobj : EMObj -> Obj A emobj (emObj isAlgebra) = obj isAlgebra +emphi : EMObj -> ? -- {a : Obj A} -> ? -- Hom A (FObj T a ) a +emphi (emObj isAlgebra) = phi isAlgebra + record IsEMHom {x y : Obj A} {φ : Hom A (FObj T x) x } {φ' : Hom A (FObj T y) y } (a : EMObj {x} {φ} ) (b : EMObj {y} {φ'} ) @@ -60,14 +63,15 @@ homomorphism : A [ A [ φ' o FMap T α ] ≈ A [ α o φ ] ] open IsEMHom -record EMHom {x y : Obj A } +record Eilenberg-Moore-Hom {x y : Obj A } (a : EMObj {x}) (b : EMObj {y}) - {α : Hom A x y} : Set (c₂ ⊔ ℓ) where + {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where field EMap : Hom A x y isEMHom : IsEMHom a b α -open EMHom +open Eilenberg-Moore-Hom +EMHom = \(a b : EMObj) -> Eilenberg-Moore-Hom {emobj a} {emobj b} a b Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} @@ -93,13 +97,10 @@ open import Relation.Binary.Core -Lemma-EM2 : (a b : EMObj) - {x : Obj A} - {φ : Hom A (FObj T x) x } - (c : EMObj {x} {φ}) +Lemma-EM2 : (a b c : EMObj) (g : EMHom b c) - (f : EMHom a b) -> A [ A [ φ o FMap T (A [ (EMap g) o (EMap f) ] ) ] - ≈ A [ (A [ (EMap g) o (EMap f) ]) o φ ] ] + (f : EMHom a b) -> A [ A [ (emphi c) o FMap T (A [ (EMap g) o (EMap f) ] ) ] + ≈ A [ (A [ (EMap g) o (EMap f) ]) o (emphi c) ] ] Lemma-EM2 _ _ (emObj isAlgebra ) g f = let x = obj isAlgebra φ = phi isAlgebra @@ -112,11 +113,12 @@ _≗_ : { a : EMObj } { b : EMObj } (f g : EMHom a b ) -> Set ℓ _≗_ f g = A [ EMap f ≈ EMap g ] -_∙_ : { a b : EMObj A } → { c : EMObj A } → +_∙_ : { a b c : EMObj } → ( EMHom b c) → (EMHom a b) → EMHom a c -_∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g) o (EMap f) ] ; isEMHom = Lemma-EM2 a b c g f } +_∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g) o (EMap f) ] ; isEMHom = + record { homomorphism = ? } } -- Lemma-EM2 a b c g f } } -isEilenberg-MooreCategory : IsCategory ( Obj A ) EMHom _≗_ _∙_ EM-id +isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id isEilenberg-MooreCategory = record { isEquivalence = isEquivalence ; identityL = KidL ; identityR = KidR @@ -125,27 +127,27 @@ } where open ≈-Reasoning (A) - isEquivalence : { a b : Obj A } -> + isEquivalence : { a b : EMObj } -> IsEquivalence {_} {_} {EMHom a b} _≗_ isEquivalence {C} {D} = -- this is the same function as A's equivalence but has different types record { refl = refl-hom ; sym = sym ; trans = trans-hom } - KidL : {C D : Obj A} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f + KidL : {C D : EMObj} -> {f : EMHom C D} → (EM-id ∙ f) ≗ f KidL {_} {_} {f} = ? -- Lemma7 (EMap f) - KidR : {C D : Obj A} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f + KidR : {C D : EMObj} -> {f : EMHom C D} → (f ∙ EM-id) ≗ f KidR {_} {_} {f} = ? -- Lemma8 (EMap f) - Ko-resp : {a b c : Obj A} -> {f g : EMHom a b } → {h i : EMHom b c } → + Ko-resp : {a b c : EMObj} -> {f g : EMHom a b } → {h i : EMHom b c } → f ≗ g → h ≗ i → (h ∙ f) ≗ (i ∙ g) Ko-resp {a} {b} {c} {f} {g} {h} {i} eq-fg eq-hi = ? -- Lemma10 {a} {b} {c} (EMap f) (EMap g) (EMap h) (EMap i) eq-fg eq-hi - Kassoc : {a b c d : Obj A} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } → + Kassoc : {a b c d : EMObj} -> {f : EMHom c d } → {g : EMHom b c } → {h : EMHom a b } → (f ∙ (g ∙ h)) ≗ ((f ∙ g) ∙ h) Kassoc {_} {_} {_} {_} {f} {g} {h} = ? -- Lemma9 (EMap f) (EMap g) (EMap h) -Eilenberg-MooreCategory : Category c₁ c₂ ℓ +Eilenberg-MooreCategory : Category (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) ℓ Eilenberg-MooreCategory = - record { Obj = Obj A + record { Obj = EMObj ; Hom = EMHom ; _o_ = _∙_ ; _≈_ = _≗_ @@ -171,21 +173,21 @@ -- ; distr = distr1 -- } -- } where --- identity : {a : Obj A} → A [ ufmap (EM-id {a}) ≈ id1 A (FObj T a) ] +-- identity : {a : EMObj} → A [ ufmap (EM-id {a}) ≈ id1 A (FObj T a) ] -- identity {a} = let open ≈-Reasoning (A) in -- begin -- TMap μ (a) o FMap T (TMap η a) -- ≈⟨ IsMonad.unity2 (isMonad M) ⟩ -- id1 A (FObj T a) -- ∎ --- ≈-cong : {a b : Obj A} {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → A [ ufmap f ≈ ufmap g ] +-- ≈-cong : {a b : EMObj} {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → A [ ufmap f ≈ ufmap g ] -- ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (A) in -- begin -- TMap μ (b) o FMap T (EMap f) -- ≈⟨ cdr (fcong T f≈g) ⟩ -- TMap μ (b) o FMap T (EMap g) -- ∎ --- distr1 : {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → A [ ufmap (g ∙ f) ≈ (A [ ufmap g o ufmap f ] )] +-- distr1 : {a b c : EMObj} {f : EMHom a b} {g : EMHom b c} → A [ ufmap (g ∙ f) ≈ (A [ ufmap g o ufmap f ] )] -- distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (A) in -- begin -- ufmap (g ∙ f)