Mercurial > hg > Members > kono > Proof > category

comparison em-category.agda @ 107:da14b7f03ff8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no yellow. ready to define category
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 31 Jul 2013 20:07:09 +0900
parents 4dec85377dbc
children e763efd30868
comparison
equal deleted inserted replaced
106:4dec85377dbc 107:da14b7f03ff8
67 {φ : Hom A (FObj T x) x } 67 {φ : Hom A (FObj T x) x }
68 {φ' : Hom A (FObj T y) y } 68 {φ' : Hom A (FObj T y) y }
69 (a : EMObj {x} {φ}) 69 (a : EMObj {x} {φ})
70 (b : EMObj {y} {φ'}) 70 (b : EMObj {y} {φ'})
71 {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where 71 {α : Hom A x y} : Set (c₁ ⊔ c₂ ⊔ ℓ) where
72 field 72 EMap : Hom A x y
73 EMap : Hom A x y 73 EMap = α
74 field
74 isEMHom : IsEMHom a b α 75 isEMHom : IsEMHom a b α
75 open Eilenberg-Moore-Hom 76 open Eilenberg-Moore-Hom
76 77
77 EMHom = \(a : EMObj) (b : EMObj) -> {α : Hom A (emobj a) (emobj b) } -> 78 EMHom : {x y : Obj A} {φ : Hom A (FObj T x) x } {φ' : Hom A (FObj T y) y } {α : Hom A x y }
78 Eilenberg-Moore-Hom {emobj a} {emobj b} {emphi {emobj a} a } {emphi b} a b {α} 79 (a : EMObj {x} {φ} ) (b : EMObj {y} {φ'} ) -> Set (c₁ ⊔ c₂ ⊔ ℓ)
79 80 EMHom {x} {y} {φ} {φ'} {α} a b = Eilenberg-Moore-Hom {x} {y} {φ} {φ'} a b {α}
80 Lemma-EM1 : {x : Obj A} 81
81 {φ : Hom A (FObj T x) x} 82 Lemma-EM1 : {x : Obj A} {φ : Hom A (FObj T x) x} (a : EMObj {x} {φ})
82 (a : EMObj {x} {φ})
83 -> A [ A [ φ o FMap T (id1 A x) ] ≈ A [ (id1 A x) o φ ] ] 83 -> A [ A [ φ o FMap T (id1 A x) ] ≈ A [ (id1 A x) o φ ] ]
84 Lemma-EM1 (emObj isAlgebra ) = let 84 Lemma-EM1 {x} {φ} (emObj isAlgebra ) = let open ≈-Reasoning (A) in
85 x = obj isAlgebra
86 φ = phi isAlgebra
87 open ≈-Reasoning (A) in
88 begin 85 begin
89 φ o FMap T (id1 A x) 86 φ o FMap T (id1 A x)
90 ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩ 87 ≈⟨ cdr ( IsFunctor.identity (isFunctor T) ) ⟩
91 φ o (id1 A (FObj T x)) 88 φ o (id1 A (FObj T x))
92 ≈⟨ idR ⟩ 89 ≈⟨ idR ⟩
93 φ 90 φ
94 ≈⟨ sym idL ⟩ 91 ≈⟨ sym idL ⟩
95 (id1 A x) o φ 92 (id1 A x) o φ
96 ∎ 93 ∎
97 94
98 EM-id : {a : EMObj } -> EMHom a a 95 EM-id : {x : Obj A} {φ : Hom A (FObj T x) x} {a : EMObj {x} {φ} } -> EMHom a a
99 EM-id {a = a} = record { EMap = id1 A (emobj a) ; 96 EM-id {x} {φ} {a = a} = record {
100 isEMHom = record { homomorphism = Lemma-EM1 a } } 97 isEMHom = record { homomorphism = Lemma-EM1 {x} {φ} a } }
101 98
102 open import Relation.Binary.Core 99 open import Relation.Binary.Core
103 100
104 Lemma-EM2 : {x y z : Obj A} 101 Lemma-EM2 : {x y z : Obj A}
105 {φ : Hom A (FObj T x) x} 102 {φ : Hom A (FObj T x) x}
106 {φ' : Hom A (FObj T y) y} 103 {φ' : Hom A (FObj T y) y}
107 {φ'' : Hom A (FObj T z) z} 104 {φ'' : Hom A (FObj T z) z}
105 {α : Hom A x y}
106 {α' : Hom A y z}
108 (a : EMObj {x} {φ} ) 107 (a : EMObj {x} {φ} )
109 (b : EMObj {y} {φ'} ) 108 (b : EMObj {y} {φ'} )
110 (c : EMObj {z} {φ''} ) 109 (c : EMObj {z} {φ''} )
111 (g : EMHom b c) 110 (g : EMHom {y} {z} {φ'} {φ''} {α'} b c )
112 (f : EMHom a b) -> A [ A [ φ'' o FMap T (A [ (EMap g) o (EMap f) ] ) ] 111 (f : EMHom {x} {y} {φ} {φ'} {α} a b)
112 -> A [ A [ φ'' o FMap T (A [ (EMap g) o (EMap f) ] ) ]
113 ≈ A [ (A [ (EMap g) o (EMap f) ]) o φ ] ] 113 ≈ A [ (A [ (EMap g) o (EMap f) ]) o φ ] ]
114 Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} (emObj _) (emObj _) (emObj _) g f = let 114 Lemma-EM2 {_} {_} {_} {φ} {φ'} {φ''} _ _ _ g f = let
115 open ≈-Reasoning (A) in 115 open ≈-Reasoning (A) in
116 begin 116 begin
117 φ'' o FMap T ((EMap g) o (EMap f)) 117 φ'' o FMap T ((EMap g) o (EMap f))
118 ≈⟨ cdr (distr T) ⟩ 118 ≈⟨ cdr (distr T) ⟩
119 φ'' o ( FMap T (EMap g) o FMap T (EMap f) ) 119 φ'' o ( FMap T (EMap g) o FMap T (EMap f) )
122 ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩ 122 ≈⟨ car (IsEMHom.homomorphism (isEMHom g)) ⟩
123 ( EMap g o φ') o FMap T (EMap f) 123 ( EMap g o φ') o FMap T (EMap f)
124 ≈⟨ sym assoc ⟩ 124 ≈⟨ sym assoc ⟩
125 EMap g o (φ' o FMap T (EMap f) ) 125 EMap g o (φ' o FMap T (EMap f) )
126 ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩ 126 ≈⟨ cdr (IsEMHom.homomorphism (isEMHom f)) ⟩
127 EMap g o (EMap f o φ)
128 ≈⟨ assoc ⟩
127 ( (EMap g) o (EMap f) ) o φ 129 ( (EMap g) o (EMap f) ) o φ
128 ∎ 130 ∎
129 _≗_ : { a : EMObj } { b : EMObj } (f g : EMHom a b ) -> Set ℓ 131 _≗_ : { a : EMObj } { b : EMObj } (f g : EMHom a b ) -> Set ℓ
130 _≗_ f g = A [ EMap f ≈ EMap g ] 132 _≗_ f g = A [ EMap f ≈ EMap g ]
131 133
132 _∙_ : { a b c : EMObj } → 134 _∙_ : { a b c : EMObj } →
133 ( EMHom b c) → (EMHom a b) → EMHom a c 135 ( EMHom b c) → (EMHom a b) → EMHom a c
134 _∙_ {a} {b} {c} g f = record { EMap = A [ (EMap g) o (EMap f) ] ; isEMHom = 136 _∙_ {a} {b} {c} g f = record { isEMHom = record { homomorphism = Lemma-EM2 a b c g f } }
135 record { homomorphism = Lemma-EM2 a b c g f } }
136 137
137 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id 138 isEilenberg-MooreCategory : IsCategory EMObj EMHom _≗_ _∙_ EM-id
138 isEilenberg-MooreCategory = record { isEquivalence = isEquivalence 139 isEilenberg-MooreCategory = record { isEquivalence = isEquivalence
139 ; identityL = KidL 140 ; identityL = KidL
140 ; identityR = KidR 141 ; identityR = KidR