Mercurial > hg > Members > kono > Proof > category

comparison HomReasoning.agda @ 168:a9b4132d619b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 20 Aug 2013 17:57:22 +0900
parents 5435469c6cf0
children 24e83b8b81be
comparison
equal deleted inserted replaced
167:c3863043c4a3 168:a9b4132d619b
115 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] 115 → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ]
116 nat η = IsNTrans.commute ( isNTrans η ) 116 nat η = IsNTrans.commute ( isNTrans η )
117 117
118 infixr 2 _∎ 118 infixr 2 _∎
119 infixr 2 _≈⟨_⟩_ _≈⟨⟩_ 119 infixr 2 _≈⟨_⟩_ _≈⟨⟩_
120 infixr 2 _≈↑⟨_⟩_
120 infix 1 begin_ 121 infix 1 begin_
121 122
122 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly 123 ------ If we have this, for example, as an axiom of a category, we can use ≡-Reasoning directly
123 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y 124 -- ≈-to-≡ : {a b : Obj A } { x y : Hom A a b } → A [ x ≈ y ] → x ≡ y
124 -- ≈-to-≡ refl-hom = refl 125 -- ≈-to-≡ refl-hom = refl
132 begin relTo x≈y = x≈y 133 begin relTo x≈y = x≈y
133 134
134 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } → 135 _≈⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } →
135 x ≈ y → y IsRelatedTo z → x IsRelatedTo z 136 x ≈ y → y IsRelatedTo z → x IsRelatedTo z
136 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z) 137 _ ≈⟨ x≈y ⟩ relTo y≈z = relTo (trans-hom x≈y y≈z)
138
139 _≈↑⟨_⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y z : Hom A a b } →
140 y ≈ x → y IsRelatedTo z → x IsRelatedTo z
141 _ ≈↑⟨ y≈x ⟩ relTo y≈z = relTo (trans-hom ( sym y≈x ) y≈z)
137 142
138 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y 143 _≈⟨⟩_ : { a b : Obj A } ( x : Hom A a b ) → { y : Hom A a b } → x IsRelatedTo y → x IsRelatedTo y
139 _ ≈⟨⟩ x∼y = x∼y 144 _ ≈⟨⟩ x∼y = x∼y
140 145
141 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x 146 _∎ : { a b : Obj A } ( x : Hom A a b ) → x IsRelatedTo x