Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 547:c0078b03201c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 04 Apr 2017 13:51:48 +0900
parents 73a5606fa362
children 03b851adc4fb 97b98b81e990
comparison
equal deleted inserted replaced
546:73a5606fa362 547:c0078b03201c
184 → a ≡ a' 184 → a ≡ a'
185 → b ≡ b' 185 → b ≡ b'
186 → f a b ≡ f a' b' 186 → f a b ≡ f a' b'
187 ≡cong2 _ refl refl = refl 187 ≡cong2 _ refl refl = refl
188 188
189 ≡cong3 : { c : Level } { I OC A B C : Set c } { a a' : OC → A } { b b' : I → B } ( f : (OC → A ) → (I → B ) → C )
190 → a ≡ a'
191 → b ≡ b'
192 → f a b ≡ f a' b'
193 ≡cong3 _ refl refl = refl
194
195
196 snat-cong1 : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j)
197 { s t : snat SObj SMap }
198 → ( snmap s ≡ snmap t )
199 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j )
200 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j )
201 → s ≡ t
202 snat-cong1 SO SM eq eq1 eq2 = ≡cong3 ( λ x y → snat1 SO SM {!!} {!!} ) {!!} {!!}
203
204 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j) 189 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j)
205 { s t : snat SObj SMap } 190 { s t : snat SObj SMap }
206 → (( i : OC ) → snmap s i ≡ snmap t i ) 191 → (( i : OC ) → snmap s i ≡ snmap t i )
207 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) 192 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j )
208 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) 193 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j )
210 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong2 ( λ x y → snat1 SO SM x y ) 195 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong2 ( λ x y → snat1 SO SM x y )
211 ( extensionality Sets ( λ i → eq1 i ) ) 196 ( extensionality Sets ( λ i → eq1 i ) )
212 ( extensionality Sets ( λ snm → 197 ( extensionality Sets ( λ snm →
213 ( extensionality Sets ( λ i → 198 ( extensionality Sets ( λ i →
214 ( extensionality Sets ( λ j → 199 ( extensionality Sets ( λ j →
215 ( extensionality Sets ( λ f → irr2 snm i j f ? {!!} )))))))) 200 ( extensionality Sets ( λ f → irr2 snm i j f ( eq2s i j f (eq1 i) snm (eq2 i j f ) ) {!!} ))))))))
216 where 201 where
202 eq2s1 : { i j : OC } { f : I } → {si : SO i} { sj : SO j }
203 ( snm : ( i : OC ) → SO i ) → ( si ≡ snm i ) → ( sj ≡ snm j ) → SM {i} {j} f si ≡ sj → SM f ( snm i) ≡ snm j
204 eq2s1 {i} {j} {f} {si} {sj} snm eq1 eq2 eq3 = begin
205 SM f ( snm i)
206 ≡⟨ ≡cong (λ x → SM f x ) (sym eq1) ⟩
207 SM f si
208 ≡⟨ eq3 ⟩
209 sj
210 ≡⟨ eq2 ⟩
211 snm j
212 ∎ where
213 open import Relation.Binary.PropositionalEquality
214 open ≡-Reasoning
215 eq2s : ( i j : OC ) ( f : I ) → ( snmap s i ≡ snmap t i ) →
216 ( snm : ( i : OC ) → SO i ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j → SM f ( snm i) ≡ snm j
217 eq2s i j f eq1 snm eq2 = eq2s1 snm {!!} {!!} eq2
218 irr3 : { i j : OC } { f : I } → {snmapsi : SO i } → {snmapsj : SO j } →
219 ( es et : SM f ( snmapsi ) ≡ snmapsj ) → es ≡ et
220 irr3 refl refl = refl
217 irr2 : ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I ) → 221 irr2 : ( snm : ( i : OC ) → SO i ) ( i j : OC ) (f : I ) →
218 ( es et : SM f (snm i ) ≡ snm j ) → es ≡ et 222 ( es et : SM f (snm i ) ≡ snm j ) → es ≡ et
219 irr2 _ _ _ _ es et = {!!} 223 irr2 snm i j f es et = irr3 es et
220
221 -- irr3 : { i j : OC } { f : I } → {snmapsi : SO i } → {snmapsj : SO j } →
222 -- ( es et : SM f ( snmapsi ) ≡ snmapsj ) → es ≡ et
223 -- irr3 refl refl = refl
224 -- irr2 : { i j : OC } { f : I } → {snmapsi snmapti : SO i } {snmapsj snmaptj : SO j } → snmapsi ≡ snmapti → snmapsj ≡ snmaptj →
225 -- ( es : SM f ( snmapsi ) ≡ snmapsj ) ( et : SM f ( snmapti ) ≡ snmaptj ) → {!!}
226 -- irr2 refl refl es et = irr3 es et
227 224
228 225
229 open import HomReasoning 226 open import HomReasoning
230 open NTrans 227 open NTrans
231 228