Mercurial > hg > Members > kono > Proof > category

changeset 505:1f47d14533d0

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 Fri, 17 Mar 2017 10:43:32 +0900
parents b489f27317fb
children 817093714fd5
files SetsCompleteness.agda
diffstat 1 files changed, 19 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 17 10:25:57 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 17 10:43:32 2017 +0900
@@ -54,25 +54,33 @@
 open Functor
 open NTrans
 
-record Slimit  { c₂ }  ( Γobj : {I A  : Set  c₂ } → I → A )  ( Γmap : {I A  : Set  c₂ } → ( (f :  I → I )  →  A → A  )) : Set  c₂ where
-     field
-      s-u0 : {!!}
+record Slimit  { c₂ } ( ΓObj :  Obj (Sets { c₂ }) → Obj (Sets { c₂ }) ) ( ΓMap :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B )) 
+      : Set  c₂ where
+     -- field
+        -- tlimit : Obj Sets
+        --  tmap :  (A : Obj Sets) → Hom Sets ? (ΓObj A)
+        -- tcommute :   {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets tlimit  ] ]
 
 open Slimit
 
 SetsLimit : { c₂ : Level} 
-          ( ΓObj :  {I A  : Set  c₂ } → I → A ) ( ΓMap : {I A  : Set  c₂ } → ( (f :  I → I )  →  A → A  ))
-          ( ΓObj' :  Obj Sets → Obj Sets ) ( ΓMap' :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj' A) ( ΓObj' B ))
-          ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj' ΓMap' ) 
-        →  Limit Sets Sets ( record { FObj =  ΓObj' ; FMap =  ΓMap' ; isFunctor = Γ } )
-SetsLimit { c₂} ΓObj ΓMap   ΓObj' ΓMap'  Γ = record { 
-           a0 =  Slimit  ΓObj  ΓMap  
-         ; t0 = s-u0 {!!}
+          ( ΓObj :  Obj Sets → Obj Sets ) ( ΓMap :  {A B : Obj Sets} → Hom Sets A B → Hom Sets (ΓObj A) ( ΓObj B ))
+          ( Γ : IsFunctor  (Sets { c₂}) (Sets { c₂}) ΓObj ΓMap ) 
+        →  Limit Sets Sets ( record { FObj =  ΓObj ; FMap =  ΓMap ; isFunctor = Γ } )
+SetsLimit { c₂} ΓObj ΓMap Γ = record { 
+           a0 =  Slimit  ΓObj  ΓMap
+         ; t0 = record { TMap = tmap ; isNTrans = record { commute = tcommute } }
          ; isLimit = record {
                limit  = {!!}
              ; t0f=t = {!!}
              ; limit-uniqueness  = {!!}
            }
-       }
+       } where
+          tmap :  (a : Obj Sets) → Hom Sets (Slimit  ΓObj  ΓMap) (ΓObj a)
+          tmap  a _ = {!!}
+          tcommute :   {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets (Slimit  ΓObj  ΓMap)  ] ]
+          tcommute {a} {b} {f} = {!!}
 
 
+
+