Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 11:2cbecadc56c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning test
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2013 19:20:37 +0900
parents 3ef6a17353d1
children 72397d77c932
comparison
equal deleted inserted replaced
10:3ef6a17353d1 11:2cbecadc56c1
163 a ≈⟨ x≈y ⟩ relTo y≈z = relTo ( trans-hom x≈y y≈z ) 163 a ≈⟨ x≈y ⟩ relTo y≈z = relTo ( trans-hom x≈y y≈z )
164 164
165 _∎ : {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x 165 _∎ : {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
166 _ ∎ = relTo ( refl-hom ) 166 _ ∎ = relTo ( refl-hom )
167 167
168
169 Lemma61 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
170 { a b : Obj A }
171 { f : Hom A a b }
172 -> A [ A [ (Id {_} {_} {_} {A} b) o f ] ≈ f ]
173 Lemma61 c = IsCategory.identityL (Category.isCategory c)
174
175 -- -> let open ≈-Reasoning c in
176 -- begin
177 -- c [ (Id {_} {_} {_} {c} b) o f ]
178 -- ≈⟨ IsCategory.identityL (Category.isCategory c) ⟩
179 -- f
180 -- ∎
181
168 open Kleisli 182 open Kleisli
169 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> 183 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
170 { T : Functor A A } 184 { T : Functor A A }
171 { η : NTrans A A identityFunctor T } 185 { η : NTrans A A identityFunctor T }
172 { μ : NTrans A A (T ○ T) T } 186 { μ : NTrans A A (T ○ T) T }
173 { a b : Obj A } 187 { a b : Obj A }
174 { f : Hom A a ( FObj T b) } 188 { f : Hom A a ( FObj T b) }
175 { M : Monad A T η μ } 189 { M : Monad A T η μ }
176 ( K : Kleisli A T η μ M) 190 ( K : Kleisli A T η μ M)
177 -> A [ join K b (Trans η b) f ≈ f ] 191 -> A [ join K b (Trans η b) f ≈ f ]
178 Lemma7 c k = {!!} 192 Lemma7 c k =
179 193 -- { a b : Obj c}
194 -- { T : Functor c c }
195 -- { η : NTrans c c identityFunctor T }
196 -- { f : Hom c a ( FObj T b) }
197 {!!}
198
180 199
181 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} 200 Lemma8 : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ}
182 { T : Functor A A } 201 { T : Functor A A }
183 { η : NTrans A A identityFunctor T } 202 { η : NTrans A A identityFunctor T }
184 { μ : NTrans A A (T ○ T) T } 203 { μ : NTrans A A (T ○ T) T }