Mercurial > hg > Members > kono > Proof > category
changeset 103:8dcf926482af
on oging
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 31 Jul 2013 15:42:38 +0900 |
parents | 09af60198ce5 |
children | 53a79dfdcd04 |
files | em-category.agda |
diffstat | 1 files changed, 30 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/em-category.agda Wed Jul 31 15:26:25 2013 +0900 +++ b/em-category.agda Wed Jul 31 15:42:38 2013 +0900 @@ -32,6 +32,10 @@ open Functor open NTrans record IsEMAlgebra (a : Obj A) (φ : Hom A (FObj T a) a ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + obj : Obj A + obj = a + phi : Hom A (FObj T a) a + phi = φ field identity : A [ A [ φ o TMap η a ] ≈ id1 A a ] eval : A [ A [ φ o TMap μ a ] ≈ A [ φ o FMap T φ ] ] @@ -42,37 +46,37 @@ isEMAlbgebra : IsEMAlgebra a φ open EMAlgebra -data EMObj {a : Obj A} {φ : Hom A (FObj T a) a } : Set ( c₁ ⊔ c₂ ) where - emObj : \a φ -> (IsEMAlgebra a φ) -> EMObj {a} {φ} +data EMObj {a : Obj A} {φ : Hom A (FObj T a) a } : Set (suc ( c₁ ⊔ c₂ ⊔ ℓ)) where + emObj : (IsEMAlgebra a φ) -> EMObj {a} {φ} emobj : EMObj -> Obj A -emobj (emObj x φ isAlgebra) = x +emobj (emObj isAlgebra) = obj isAlgebra -record IsEMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } - {x y : Obj A} {φ : FObj T x -> x } {φ' : FObj T y -> y } - (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ ) - (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y φ' ) - (α : Hom A a b) : Set c₂ where +record IsEMHom {x y : Obj A} {φ : Hom A (FObj T x) x } {φ' : Hom A (FObj T y) y } + (a : EMObj {x} {φ} ) + (b : EMObj {y} {φ'} ) + (α : Hom A x y) : Set ℓ where field homomorphism : A [ A [ φ' o FMap T α ] ≈ A [ α o φ ] ] open IsEMHom -record EMHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } - {x y : Obj A } - (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x) - (b : EMObj {c₁} {c₂} {ℓ} {A} {T} y) - {α : Hom A a b} : Set c₂ where +record EMHom {x y : Obj A } + (a : EMObj {x}) + (b : EMObj {y}) + {α : Hom A x y} : Set (c₂ ⊔ ℓ) where field EMap : Hom A x y - isEMHom : IsEMHom {c₁} {c₂} {ℓ} {A} {T} a b α + isEMHom : IsEMHom a b α open EMHom -Lemma-EM1 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } - {x : Obj A} - {φ : FObj T x -> x } - (a : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ) +Lemma-EM1 : {x : Obj A} + {φ : Hom A (FObj T x) x} + (a : EMObj {x} {φ}) -> A [ A [ φ o FMap T (id1 A x) ] ≈ A [ (id1 A x) o φ ] ] -Lemma-EM1 (emObj x φ isAlgebra ) = let open ≈-Reasoning (A) in +Lemma-EM1 (emObj isAlgebra ) = let + x = obj isAlgebra + φ = phi isAlgebra + open ≈-Reasoning (A) in begin φ o FMap T (id1 A x) ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩ @@ -89,15 +93,17 @@ open import Relation.Binary.Core -Lemma-EM2 : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } - (a b : EMObj) +Lemma-EM2 : (a b : EMObj) {x : Obj A} - {φ : FObj T x -> x } - (c : EMObj {c₁} {c₂} {ℓ} {A} {T} x φ) + {φ : Hom A (FObj T x) x } + (c : EMObj {x} {φ}) (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 φ ] ] -Lemma-EM2 _ _ (emObj c φ isAlgebra ) g f = let open ≈-Reasoning (A) in +Lemma-EM2 _ _ (emObj isAlgebra ) g f = let + x = obj isAlgebra + φ = phi isAlgebra + open ≈-Reasoning (A) in begin φ o FMap T (A [ (EMap g) o (EMap f) ] ) ≈⟨ ? ⟩