Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 550:c2ce1c6a3570

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
close this
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Apr 2017 03:24:44 +0900
parents adef39d19884
children
comparison
equal deleted inserted replaced
549:adef39d19884 550:c2ce1c6a3570
232 232
233 scomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) 233 scomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j )
234 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) 234 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i )
235 → ( i j : OC ) → ( f : I ) 235 → ( i j : OC ) → ( f : I )
236 → SM f ( snmap s i ) ≡ snmap s j 236 → SM f ( snmap s i ) ≡ snmap s j
237 → SM f (snmeq s t i (eq1 i)) ≡ snmeq s t j (eq1 j) 237 → {x : ( i : OC ) → SO i } → (x ≡ λ i → snmeq s t i (eq1 i ) )
238 scomm2 SO SM s t eq1 i j f eq2 = lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1) where 238 → SM f (x i) ≡ x j
239 scomm2 SO SM s t eq1 i j f eq2 refl = lemma eq2 (snmeqeqs SO SM s t i eq1) (snmeqeqs SO SM s t j eq1) where
239 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) 240 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj )
240 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 241 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
241 242
242 tcomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j ) 243 tcomm2 : { c₂ : Level } { I OC : Set c₂ } ( SO : OC → Set c₂ ) ( SM : { i j : OC } → (f : I )→ SO i → SO j )
243 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) 244 ( s t : snat SO SM ) → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i )
247 tcomm2 SO SM s t eq1 i j f eq2 = lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt SO SM s t j eq1) where 248 tcomm2 SO SM s t eq1 i j f eq2 = lemma eq2 (snmeqeqt SO SM s t i eq1) (snmeqeqt SO SM s t j eq1) where
248 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj ) 249 lemma : { si sni : SO i} { sj snj : SO j } → ( SM f si ≡ sj ) → (si ≡ sni ) → (sj ≡ snj ) → ( SM f sni ≡ snj )
249 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3 250 lemma eq1 eq2 eq3 = subst2 (λ x → SM f x) (λ y → y ) eq1 eq2 eq3
250 251
251 252
252 -- {!!} -- subst ( λ x → SM f x ) ( λ x → x ) ? ? ?
253
254 -- irr : { c₂ : Level} {d : Set c₂ } { x y : d } ( eq eq' : x ≡ y ) → eq ≡ eq'
255 -- irr refl refl = refl
256
257 -- irr2 : { c₂ : Level} {d : Set c₂ } { x1 x2 y1 y2 : d } ( eqx : x1 ≡ x2 )( eqy : y1 ≡ y2 )
258 -- ( eq1 : x1 ≡ y1 ) ( eq2 : x2 ≡ y2 ) → eq1 ≡ eq2
259 -- irr2 = ?
260
261
262 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j) 253 snat-cong : { c : Level } { I OC : Set c } ( SObj : OC → Set c ) ( SMap : { i j : OC } → (f : I )→ SObj i → SObj j)
263 { s t : snat SObj SMap } 254 { s t : snat SObj SMap }
264 → (( i : OC ) → snmap s i ≡ snmap t i ) 255 → (( i : OC ) → snmap s i ≡ snmap t i )
265 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j ) 256 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap s i ) ≡ snmap s j )
266 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j ) 257 → ( ( i j : OC ) ( f : I ) → SMap {i} {j} f ( snmap t i ) ≡ snmap t j )
267 → s ≡ t 258 → s ≡ t
268 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = ≡cong2 ( λ x y → 259 snat-cong {_} {I} {OC} SO SM {s} {t} eq1 eq2 eq3 = begin
269 record { snmap = λ i → x i ; sncommute = λ {i} {j} f → y x i j f } ) (extensionality Sets ( λ i → eq1 i )) 260 record { snmap = λ i → snmap s i ; sncommute = λ {i} {j} f → sncommute s f }
270 ( extensionality Sets ( λ x → 261 ≡⟨
271 ( extensionality Sets ( λ i → 262 ≡cong2 ( λ x y →
272 ( extensionality Sets ( λ j → 263 record { snmap = λ i → x i ; sncommute = λ {i} {j} f → y ? i j f } ) ( extensionality Sets ( λ i → snmeqeqs SO SM s t i eq1 ) )
273 ( extensionality Sets ( λ f → snat-irr x i j f 264 ( extensionality Sets ( λ x →
274 {!!} 265 ( extensionality Sets ( λ i →
275 {!!} 266 ( extensionality Sets ( λ j →
276 )))))))) where 267 ( extensionality Sets ( λ f → scomm2 SO SM s t eq1 i j f (eq2 i j f ) x
277 smi=pi : ( i j : OC ) (f : I ) 268 ))))))))
278 → { sm : ( i : OC ) → SO i } 269 ⟩
279 → { smi : SO i } 270 record { snmap = λ i → snmeq s t i (eq1 i ) ; sncommute = λ {i} {j} f → snmc s t (eq1 i) (eq1 j) (eq2 i j f ) (eq3 i j f ) }
280 → ( sm i ≡ smi ) 271 ≡⟨ {!!} ⟩
281 → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i ) 272 record { snmap = λ i → snmap t i ; sncommute = λ {i} {j} f → sncommute t f }
282 → smi ≡ snmap s i 273 ∎ where
283 smi=pi i j f {sm} refl eq1 = {!!} where 274 open import Relation.Binary.PropositionalEquality
284 lemma : { si ti : SO i } → ( si ≡ ti ) → sm i ≡ si 275 open ≡-Reasoning
285 lemma refl = {!!}
286 scomm1 : ( i j : OC ) (f : I )
287 → ( sm : ( i : OC ) → SO i )
288 → { smfi smj : SO j}
289 → ( sm j ≡ sm j )
290 → smfi ≡ smj
291 → SM f (sm i) ≡ sm j
292 scomm1 i j f = {!!}
293 scomm : {sm : ( i : OC ) → SO i } ( i j : OC ) (f : I )
294 → ( eq1 : ( i : OC ) → snmap s i ≡ snmap t i )
295 → ( eq2 : ( i j : OC ) ( f : I ) → SM {i} {j} f ( snmap s i ) ≡ snmap s j )
296 → SM f (sm i) ≡ sm j
297 scomm {sm} i j f eq1 eq2 = {!!} -- scomm1 i j f sm (eq1 j) ( ≡cong ( λ k → SM f ) ( eq1 i )) (eq2 i j f )
298 snat-irr1 : (sm : ( i : OC ) → SO i ) ( i j : OC ) → ( f : I ) → { smfi smj : SO j } → ( es et : smfi ≡ smj ) → es ≡ et
299 snat-irr1 sm i j f refl refl = refl
300 snat-irr : (sm : ( i : OC ) → SO i ) ( i j : OC ) → ( f : I ) → ( es et : SM f ( sm i ) ≡ sm j ) → es ≡ et
301 snat-irr sm i j f es et = snat-irr1 sm i j f es et
302
303 snat-irr' : (sm : ( i : OC ) → SO i ) ( i j : OC ) → ( f : I ) → { snmapsi snmapti : SO i } → snmapsi ≡ snmapti → snmapsi ≡ sm i → ( es et : SM f ( sm i ) ≡ sm j ) → es ≡ et
304 snat-irr' sm i j f {pi} {.pi} refl eq es et = snat-irr1 sm i j f es et
305
306 276
307 open import HomReasoning 277 open import HomReasoning
308 open NTrans 278 open NTrans
309 279
310 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) ) 280 Cone : { c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I : Set c₁ ) ( s : Small C I ) ( Γ : Functor C (Sets {c₁} ) )