Mercurial > hg > Members > kono > Proof > category

changeset 501:61daa68a70c4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sets completeness failed
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 16 Mar 2017 10:26:30 +0900
parents 6c993c1fe9de
children 01a0dda67a8b
files SetsCompleteness.agda
diffstat 1 files changed, 15 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Wed Mar 15 19:26:51 2017 +0900
+++ b/SetsCompleteness.agda	Thu Mar 16 10:26:30 2017 +0900
@@ -44,11 +44,22 @@
            }
        }
 
+open Functor
+open NTrans
 
-SetsLimit : { c₁' c₂' ℓ' : Level} {  c₂ : Level}  ( I : Category c₁' c₂' ℓ' ) → ( Γ : Functor I (Sets { c₂}) ) →  Limit Sets I Γ
-SetsLimit I Γ = record { 
-           a0 = {!!} 
-         ; t0 = {!!}
+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
+     field
+      Carrier : Set  c₂
+      s-a0 : Carrier
+      s-u0 : NTrans I Sets ( K Sets I Carrier ) Γ
+
+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 Γ )
+         ; t0 = s-u0 {!!}
          ; isLimit = record {
                limit  = {!!}
              ; t0f=t = {!!}