Mercurial > hg > Members > kono > Proof > category

changeset 602:b7659ad60a69

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
makeEqu/makeProd does not woek
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Jun 2017 18:57:15 +0900
parents 2e7b5a777984
children e548f8f2b9b4
files SetsCompleteness.agda
diffstat 1 files changed, 12 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Mon Jun 05 14:16:36 2017 +0900
+++ b/SetsCompleteness.agda	Mon Jun 05 18:57:15 2017 +0900
@@ -160,18 +160,27 @@
         --    c
 
 --  
-makeEqu :  {  c₂ : Level}  →  {a b c : Obj  (Sets {c₂})} → (e : Hom  (Sets {c₂}) c a )  → (f g : Hom  (Sets {c₂}) a b)  → IsEqualizer  (Sets {c₂}) e f g
+makeEqu :  { c₂ : Level}  →  {a b c : Obj  (Sets {c₂})} → (e : Hom  (Sets {c₂}) c a )  → (f g : Hom  (Sets {c₂}) a b)  → IsEqualizer  (Sets {c₂}) e f g
 makeEqu {c₂} {a} {b} {c} e f g =  record {
                fe=ge  = {!!}
              ; k = λ {d} h eq → {!!}
              ; ek=h = λ {d} {h} {eq} → {!!}
              ; uniqueness  = {!!}
        } where
-           equ0 : IsEqualizer Sets (λ e → equ e )f g
+           equ0 : IsEqualizer Sets (λ e → equ e ) f g
            equ0 = SetsIsEqualizer a b f g
            c→equ0 : Hom Sets c ( sequ a b f g )
-           c→equ0 = {!!}
+           c→equ0 x = elem (e x)  {!!} -- (  ≡cong ( λ y → y {!!} ) ( IsEqualizer.fe=ge equ0 ) )
 
+makeProd :  { c₂ : Level} → ( I :  Obj (Sets {c₂}) ) 
+    → (p : Obj (Sets {c₂})) ( ai : I → Obj (Sets {c₂}) )  ( pi : (i : I) → Hom (Sets {c₂}) p ( ai i ) )
+                  →  IsIProduct (Sets {c₂}) I p ai pi 
+makeProd I p fi pi = record {
+              iproduct = λ {q} qi x → ?
+            ; pif=q = {!!}
+            ; ip-uniqueness = {!!}
+            ; ip-cong  = {!!}
+       }
 
 open Functor