Mercurial > hg > Members > kono > Proof > category

changeset 564:40dfdb801061

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on ging ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Apr 2017 10:18:36 +0900
parents 8b18361e6ca9
children 6cf91ef84ca0
files SetsCompleteness.agda
diffstat 1 files changed, 24 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sun Apr 23 19:17:04 2017 +0900
+++ b/SetsCompleteness.agda	Mon Apr 24 10:18:36 2017 +0900
@@ -203,7 +203,7 @@
     → NTrans C Sets (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ) )) Γ
 Cone C I s  Γ =  record {
                TMap = λ i →  λ se → snmap (equ (snequ1 se {i} {i} (λ x → x )) ) i
-             ; isNTrans = record { commute = {!!} }
+             ; isNTrans = record { commute = commute1 }
       } where
          commute1 :  {a b : Obj C} {f : Hom C a b} → Sets [ Sets [ FMap Γ f o (λ se → snmap (equ (snequ1 se {a} {a} (λ x → x))) a) ] ≈
                 Sets [ (λ se → snmap (equ (snequ1 se {b} {b} (λ x → x))) b) o FMap (K Sets C (snequ (ΓObj s Γ) (ΓMap s Γ))) f ] ]
@@ -233,8 +233,29 @@
            a0 =  snequ  (ΓObj s Γ) (ΓMap s Γ)  
          ; t0 = Cone C I s Γ 
          ; isLimit = record {
-               limit  =  {!!}
+               limit  =  limit1 
              ; t0f=t = λ {a t i } → {!!}
-             ; limit-uniqueness  =  λ {a t i }  → {!!}
+             ; limit-uniqueness  =  λ {a} {t} {f} → uniquness1 {a} {t} {f}
           }
        }  where
+              limit2 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → {i j : Obj C } →　 ( f : I → I ) 
+                    → ( x : a )  → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
+              limit2 a t {i} {j} f x =   ≡cong ( λ g → g x )   ( IsNTrans.commute ( isNTrans t  ) )
+              limit1 :  (a : Obj Sets) → ( t : NTrans C Sets (K Sets C a) Γ ) → Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ))
+              limit1 a t x = record {
+                   snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x  )
+                } 
+              uniquness1 : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snequ (ΓObj s Γ) (ΓMap s Γ) )} →
+                    ({i  : Obj C} → Sets [ Sets [ TMap (Cone C I s Γ) i o f ] ≈ TMap t i ]) → Sets [ limit1 a t  ≈ f ]
+              uniquness1 {a} {t} {f} cif=t =  extensionality Sets  ( λ  x  →  begin
+                  limit1 a t x
+                ≡⟨⟩
+                   record { snequ1 = λ {i} {j} f → elem ( record { snmap = λ i → TMap t i x }  ) ( limit2 a t f x ) }
+                ≡⟨ ≡cong ( λ e → record { snequ1 =  λ {i} {j} f → e x } ) ?   ⟩
+                   record { snequ1 = λ {i} {j} f' → snequ1 (f x ) f' }
+                ≡⟨⟩
+                  f x
+                ∎  ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+