Mercurial > hg > Members > kono > Proof > category

changeset 506:817093714fd5

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, 17 Mar 2017 11:53:53 +0900
parents 1f47d14533d0
children c1c12e5a82ad
files SetsCompleteness.agda
diffstat 1 files changed, 13 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 17 10:43:32 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 17 11:53:53 2017 +0900
@@ -54,21 +54,24 @@
 open Functor
 open NTrans
 
-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  ] ]
+record Slimit  { c₂ }  (I :  Set  c₂ ) ( ΓObj  : I → Set  c₂ ) 
+          ( ΓMap : ( f : I → I ) →  Set  c₂   →  Set  c₂   )  : Set  c₂ where
+     field
+        sobj :  I
+        bb :  ΓObj  sobj
+        cc :  I → I
+        ec :  ΓMap cc I
+        dc :  ΓObj  sobj → I
 
 open Slimit
 
 SetsLimit : { c₂ : Level} 
+          ( I :  Set  c₂ ) ( ΓObj'  : I → Set  c₂ )( ΓMap' :   {  f : I → I } →  Set  c₂   →  Set  c₂ ) 
           ( Γ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
+SetsLimit { c₂} I ΓObj' ΓMap'  ΓObj ΓMap Γ = record { 
+           a0 =  Slimit  I  ΓObj'  ΓMap'
          ; t0 = record { TMap = tmap ; isNTrans = record { commute = tcommute } }
          ; isLimit = record {
                limit  = {!!}
@@ -76,9 +79,9 @@
              ; limit-uniqueness  = {!!}
            }
        } where
-          tmap :  (a : Obj Sets) → Hom Sets (Slimit  ΓObj  ΓMap) (ΓObj a)
+          tmap :  (a : Obj Sets) → Hom Sets (Slimit  I {!!}  {!!}) (Γ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 : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ ΓMap f o tmap a ] ≈ Sets [ tmap  b o id1 Sets (Slimit I {!!} {!!})  ] ]
           tcommute {a} {b} {f} = {!!}