Mercurial > hg > Members > kono > Proof > category

changeset 525:cb35d6b25559

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 Mon, 27 Mar 2017 10:18:08 +0900
parents d6739779b4ac
children b035cd3be525
files SetsCompleteness.agda
diffstat 1 files changed, 15 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Mar 27 06:55:25 2017 +0900
+++ b/SetsCompleteness.agda	Mon Mar 27 10:18:08 2017 +0900
@@ -134,8 +134,14 @@
            lemma5 refl  x  = refl   -- somehow this is not equal to lemma1
            uniqueness :   {d : Obj Sets} {h : Hom Sets d a} {fh=gh : Sets [ Sets [ f o h ] ≈ Sets [ g o h ] ]} {k' : Hom Sets d (sequ a b f g)} →
                 Sets [ Sets [ (λ e → equ e) o k' ] ≈ h ] → Sets [ k h fh=gh  ≈ k' ]
-           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) → 
-                 elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x ) )
+           uniqueness  {d} {h} {fh=gh} {k'} ek'=h =  extensionality Sets  ( λ ( x : d ) →  begin
+                k h fh=gh x
+             ≡⟨ elm-cong ( k h fh=gh x) (  k' x ) (lemma5 {d} {h} {fh=gh} {k'} ek'=h x )  ⟩
+                k' x
+             ∎  ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+
 
 open Functor
 open NTrans
@@ -165,9 +171,11 @@
 
 open IProduct
 
+record slim   { c₂ }   ( sobj : Set  c₂ →  Set  c₂ ) ( smap : { a b : Set  c₂ } ( f :  a → b ) → Set  c₂ ) : Set  c₂ where
+
 SetsLimit :  { c₂ : Level}  →  Limit Sets Sets Γ
 SetsLimit { c₂}  = record { 
-           a0 =  {!!}
+           a0 =  slim ΓObj ΓMap
          ; t0 = record { 
                TMap = λ i → Sets  [ proj i o  e i ]
              ; isNTrans = record { commute = {!!} } 
@@ -180,10 +188,10 @@
        }  where
           eqa : {i j : Obj Sets} (f : Hom Sets i j) → sequ (Obj Sets) (Obj Sets) {!!} {!!}         --  {!!} {!!} (FMap Γ f o  proj i) ( proj j ) 
           eqa f = {!!}
-          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets ( sequ {!!} {!!} {!!} {!!}  )) i ) (iproduct (Obj Sets) (λ I → ΓObj (Obj Sets)))
-          e i =  λ x → record { pi1  = λ i → record { obj =  sequ ? {!!} {!!} {!!}    } }
-          proj :  (i : Obj Sets) → ( prod : iproduct (Obj Sets) (λ i → ΓObj (Obj Sets) )) → FObj Γ i
-          proj i prod =  record { obj = {!!} }
+          e :  (i : Obj Sets) →  Hom Sets (FObj (K Sets Sets (slim ΓObj ΓMap)) i ) (iproduct (slim ΓObj ΓMap) (λ I → ΓObj (slim ΓObj ΓMap)))
+          e i =  λ x → record { pi1  = λ j → record { obj =  record {}} }
+          proj :  (i : Obj Sets) → ( prod : iproduct (slim ΓObj ΓMap) (λ i → ΓObj (slim ΓObj ΓMap))) → FObj Γ i
+          proj i prod =  record { obj = ? }
           comm1 :  {a b : Obj Sets} {f : Hom Sets a b} → Sets [ Sets [ FMap Γ f o (λ lim → {!!} ) ] ≈
                        Sets [ (λ lim → {!!}) o FMap (K Sets Sets {!!}) f ] ]
           comm1 {a} {b} {f} = {!!}