Mercurial > hg > Members > kono > Proof > category

changeset 539:9a657775d81e

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 Fri, 31 Mar 2017 08:11:46 +0900
parents d22c93dca806
children 2373c11a93f1
files SetsCompleteness.agda
diffstat 1 files changed, 16 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 31 08:01:13 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 31 08:11:46 2017 +0900
@@ -152,8 +152,8 @@
 record Small  {  c₁ c₂ ℓ : Level} ( C : Category c₁ c₂ ℓ ) ( I :  Set  c₁ )
                 : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
    field
-     shom→ : {i j : Obj C } →    Hom C i j →  I → I 
-     shom← : {i j : Obj C } →  ( f : I → I ) →  Hom C i j 
+     shom→ : {i j : Obj C } →    Hom C i j →  I  
+     shom← : {i j : Obj C } →  ( f : I ) →  Hom C i j 
      shom-iso : {i j : Obj C } →  { f : Hom C i j } →   shom← ( shom→ f )  ≡ f 
      -- ≈-≡ : {a b : Obj C } { x y : Hom C a b } →  (x≈y : C [ x ≈ y ] ) → x ≡ y
 
@@ -164,14 +164,14 @@
 ΓObj s  Γ i = FObj Γ i
 
 ΓMap :  {  c₁ c₂ ℓ : Level} { C : Category c₁ c₂ ℓ } { I :  Set  c₁ } ( s : Small C I ) ( Γ : Functor C ( Sets { c₁} ))  
-    {i j : Obj C } →　 ( f : I → I ) →  ΓObj s Γ i → ΓObj  s Γ j 
+    {i j : Obj C } →　 ( f : I ) →  ΓObj s Γ i → ΓObj  s Γ j 
 ΓMap  s Γ {i} {j} f = FMap Γ ( shom← s f ) 
 
 record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ ) 
-     ( smap : { i j :  OC  }  → (f : I → I )→  sobj i → sobj j ) : Set  c₂ where
+     ( smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j ) : Set  c₂ where
    field 
        snmap : ( i : OC ) → sobj i 
-       sncommute : { i j : OC } → ( f : I → I ) →  smap f ( snmap i )  ≡ snmap j
+       sncommute : { i j : OC } → ( f :  I ) →  smap f ( snmap i )  ≡ snmap j
 
 open snat
 
@@ -209,18 +209,23 @@
          ; t0 = Cone C I s Γ
          ; isLimit = record {
                limit  = limit1
-             ; t0f=t = {!!}
-             ; limit-uniqueness  = {!!}
-           }
+             ; t0f=t = λ {a t i } → t0f=t {a} {t} {i}
+             ; limit-uniqueness  =  λ {a t i }  → limit-uniqueness   {a} {t} {i}
+          }
        }  where
           a0 : Obj Sets
           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
-          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I) 
+          comm2 : { a : Obj Sets } {x : a } {i j : Obj C} (t : NTrans C Sets (K Sets C a) Γ) (f : I) 
              → ΓMap s Γ f (TMap t i x) ≡ TMap t j x
           comm2 {a} {x} t f =  ≡cong ( λ f → f x ) ( IsNTrans.commute ( isNTrans t ) )
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 
           limit1 a t = λ x →  record { snmap = λ i →  ( TMap t i ) x ;
               sncommute = λ f → comm2 t f }
+          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 ]
+          t0f=t = {!!}
+          limit-uniqueness : {a : Obj Sets} {t : NTrans C Sets (K Sets C a) Γ} {f : Hom Sets a (snat (Γ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 ]
+          limit-uniqueness = {!!}
 
 
 
@@ -228,3 +233,5 @@
 
 
 
+
+