Mercurial > hg > Members > kono > Proof > category

comparison nat.agda @ 9:3207ae6d4442

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reasoning
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2013 18:16:46 +0900
parents d5e4db7bbe01
children 3ef6a17353d1
comparison
equal deleted inserted replaced
8:d5e4db7bbe01 9:3207ae6d4442
142 refl-hom = \a -> IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory a )) 142 refl-hom = \a -> IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory a ))
143 143
144 trans-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } 144 trans-hom : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A }
145 { x y z : Hom A a b } → 145 { x y z : Hom A a b } →
146 A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ] 146 A [ x ≈ y ] → A [ y ≈ z ] → A [ x ≈ z ]
147 trans-hom = \a -> IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory a )) 147 trans-hom a b c = ( IsEquivalence.trans (IsCategory.isEquivalence ( Category.isCategory a ))) b c
148 148
149 infix 2 _∎ 149 infixr 2 _∎_
150 infixr 2 _≈⟨_⟩_ 150 infixr 2 _≈⟨_!_⟩_
151 infix 1 begin_ 151 infix 1 begin_
152 152
153 data IsRelatedTo {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } ( x y : Hom A a b ) : 153 data IsRelatedTo {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } ( x y : Hom A a b ) :
154 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where 154 Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
155 relTo : (x≈y : A [ x ≈ y ] ) → IsRelatedTo A x y 155 relTo : (x≈y : A [ x ≈ y ] ) → IsRelatedTo A x y
156 156
157 begin_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } { x y : Hom A a b} → 157 begin_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } { x y : Hom A a b} →
158 IsRelatedTo A x y → A [ x ≈ y ] 158 IsRelatedTo A x y → A [ x ≈ y ]
159 begin relTo x≈y = x≈y 159 begin relTo x≈y = x≈y
160 160
161 _≈⟨_⟩_ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } 161 _≈⟨_!_⟩_ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> {a b : Obj A }
162 { x y z : Hom A a b } → 162 ( x : Hom A a b ) → { y z : Hom A a b } →
163 A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z 163 A [ x ≈ y ] → IsRelatedTo A y z → IsRelatedTo A x z
164 _≈⟨_⟩_ = {!!} 164 a ≈⟨ _ ! x≈y ⟩ relTo y≈z = relTo ( trans-hom a x≈y y≈z )
165 165
166 -- _≈⟨ x ⟩ _ = ? -- relTo (Trans1 x≈y y≈z) 166 _∎_ : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
167 -- _≈⟨ x≈y ⟩ relTo y≈z = ? -- relTo (Trans1 x≈y y≈z) 167 a ∎ _ = relTo ( refl-hom a )
168
169 _∎ : {c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} {a b : Obj A } (x : Hom A a b) → IsRelatedTo A x x
170 _∎ _ = relTo {!!}
171 168
172 open Kleisli 169 open Kleisli
173 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) -> 170 Lemma7 : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) ->
174 { T : Functor A A } 171 { T : Functor A A }
175 { η : NTrans A A identityFunctor T } 172 { η : NTrans A A identityFunctor T }