Mercurial > hg > Members > kono > Proof > category

changeset 504:b489f27317fb

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:25:57 +0900
parents bd33096c189b
children 1f47d14533d0
files SetsCompleteness.agda
diffstat 1 files changed, 12 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 17 09:25:46 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 17 10:25:57 2017 +0900
@@ -11,18 +11,18 @@
 open import Relation.Binary.Core
 open import Function
 
-record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+record Σ {a} (A : Set a) (B : Set a) : Set a where
   constructor _,_
   field
     proj₁ : A
-    proj₂ : B proj₁
+    proj₂ : B 
 
 open Σ public
 
 
 SetsProduct :  {  c₂ : Level} → CreateProduct ( Sets  {  c₂} )
 SetsProduct { c₂ } = record { 
-         product =  λ a b →    Σ a  (λ _ → b)
+         product =  λ a b →    Σ a  b
        ; π1 = λ a b → λ ab → (proj₁ ab)
        ; π2 = λ a b → λ ab → (proj₂ ab)
        ; isProduct =  λ a b → record {
@@ -54,18 +54,19 @@
 open Functor
 open NTrans
 
-record Slimit  { c₂ : Level}  { c₁' c₂' ℓ' : Level}   ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I (Sets { c₂}) )  
-         : Set (suc ℓ' ⊔ (suc c₂' ⊔ (suc c₁' ⊔ suc (suc c₂)))) where
+record Slimit  { c₂ }  ( Γobj : {I A  : Set  c₂ } → I → A )  ( Γmap : {I A  : Set  c₂ } → ( (f :  I → I )  →  A → A  )) : Set  c₂ where
      field
-      Carrier : Set  c₂
-      s-a0 : Carrier
-      s-u0 : NTrans I Sets ( K Sets I Carrier ) Γ
+      s-u0 : {!!}
 
 open Slimit
 
-SetsLimit : { c₂ : Level} { c₁' c₂' ℓ' : Level}   ( I : Category c₁' c₂' ℓ' ) ( Γ : Functor I (Sets { c₂}) ) →  Limit Sets I Γ
-SetsLimit { c₂} I Γ = record { 
-           a0 = s-a0 {!!} -- ( Slimit I Γ )
+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 {!!}
          ; isLimit = record {
                limit  = {!!}