Mercurial > hg > Members > kono > Proof > category

comparison SetsCompleteness.agda @ 561:2c0e168c832e

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 Mon, 10 Apr 2017 10:48:50 +0900
parents ba9c6dbbe6cb
children 14483d9d604c
comparison
equal deleted inserted replaced
560:ba9c6dbbe6cb 561:2c0e168c832e
234 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 234 comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I )
235 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x 235 → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
236 comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) ) 236 comm2 {a} {x} t f = ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
237 comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I ) 237 comm3 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I )
238 → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap x₁ i)) o setprod t ] ≈ Sets [ (λ x₁ → snmap x₁ j) o setprod t ] ] 238 → Sets [ Sets [ (λ x₁ → ΓMap s Γ f (snmap x₁ i)) o setprod t ] ≈ Sets [ (λ x₁ → snmap x₁ j) o setprod t ] ]
239 comm3 {a} {x} t f = {!!} 239 comm3 {a} {x} t f = IsNTrans.commute (isNTrans t )
240 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ)) 240 limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ))
241 limit1 a t = λ ( x : a ) → record { 241 limit1 a t = λ ( x : a ) → record {
242 snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x 242 snequ1 = λ {i} {j} f → k ( setprod t ) (comm3 {a} {x} t f ) x
243 } 243 }
244 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ] 244 t0f=t : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {i : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ ) i o limit1 a t ] ≈ TMap t i ]
254 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin 254 limit-uniqueness {a} {t} {f} cif=t = extensionality Sets ( λ x → begin
255 limit1 a t x 255 limit1 a t x
256 ≡⟨⟩ 256 ≡⟨⟩
257 record { snequ1 = λ {i} {j} f' → k ( setprod t ) (comm3 {a} {x} t f' ) x } 257 record { snequ1 = λ {i} {j} f' → k ( setprod t ) (comm3 {a} {x} t f' ) x }
258 ≡⟨ ≡cong ( λ ff → record { snequ1 = λ {i} {j} f' → ff i j f' }) ( 258 ≡⟨ ≡cong ( λ ff → record { snequ1 = λ {i} {j} f' → ff i j f' }) (
259 extensionality Sets ( λ i → extensionality Sets ( λ j → extensionality Sets ( λ f' → k-cong {i} {j} f' x 259 extensionality Sets ( λ i → extensionality Sets ( λ j → extensionality Sets ( λ f'
260 → k-cong {i} {j} f' x
260 ))) 261 )))
261 ) ⟩ 262 ) ⟩
262 record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' } 263 record { snequ1 = λ {i} {j} f' → snequ1 (f x) f' }
263 ≡⟨⟩ 264 ≡⟨⟩
264 f x 265 f x
265 ∎ ) where 266 ∎ ) where
266 open import Relation.Binary.PropositionalEquality 267 open import Relation.Binary.PropositionalEquality
267 open ≡-Reasoning 268 open ≡-Reasoning
268 k-cong : { i j : Obj C } ( f' : I → I ) ( x : a ) → k ( setprod t ) (comm3 {a} {x} t f' ) x ≡ snequ1 (f x) f' 269 snmap-cong : ( e : snequ (ΓObj s Γ) (ΓMap s Γ) ) {i : Obj C } { f g : I → I }
270 → snmap ( equ ( snequ1 e f)) i ≡ snmap ( equ ( snequ1 e g)) i
271 snmap-cong e {i} = ≡cong ( λ s → snmap s i ) refl
272 k-cong : { i j : Obj C } ( f' : I → I ) ( x : a ) → k ( setprod t ) (comm3 {a} {x} t f' ) x ≡ snequ1 (f x) f'
269 k-cong {i} {j} f' x = begin 273 k-cong {i} {j} f' x = begin
270 k ( setprod t ) (comm3 {a} {x} t f' ) x 274 k ( setprod t ) (comm3 {a} {x} t f' ) x
271 ≡⟨ elm-cong (k ( setprod t ) (comm3 {a} {x} t f' ) x ) ( snequ1 (f x) f' ) ( begin 275 ≡⟨ elm-cong (k ( setprod t ) (comm3 {a} {x} t f' ) x ) ( snequ1 (f x) f' ) ( begin
272 equ (k (setprod t) (comm3 t f') x) 276 equ (k (setprod t) (comm3 {a} {x} t f') x)
273 ≡⟨⟩ 277 ≡⟨⟩
274 record { snmap = λ i' → TMap t i' x } 278 record { snmap = λ i' → TMap t i' x }
275 ≡⟨ ≡cong ( λ s → record { snmap = λ i' → s i' } ) ( extensionality Sets ( λ i' → ( sym ( begin 279 ≡⟨ ≡cong ( λ s → record { snmap = λ i' → s i' } ) ( extensionality Sets ( λ i' → ( sym ( begin
276 snmap ( equ ( snequ1 (f x) f')) i' 280 snmap ( equ ( snequ1 (f x) f')) i'
277 ≡⟨ ? ⟩ 281 ≡⟨ snmap-cong (f x) ⟩
278 snmap ( equ ( snequ1 (f x) (λ x → x ))) i' 282 snmap ( equ ( snequ1 (f x) (λ x → x ))) i'
279 ≡⟨ ≡cong ( λ f → f x ) cif=t ⟩ 283 ≡⟨ ≡cong ( λ f → f x ) cif=t ⟩
280 TMap t i' x 284 TMap t i' x
281 ∎ )))) ⟩ 285 ∎ )))) ⟩
282 record { snmap = λ i' → snmap (equ (snequ1 (f x) f')) i' } 286 record { snmap = λ i' → snmap (equ (snequ1 (f x) f')) i' }