Mercurial > hg > Members > kono > Proof > category

diff SetsCompleteness.agda @ 673:0007f9a25e9c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix limit from product and equalizer (not yet finished )
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 03 Nov 2017 13:31:08 +0900
parents 749df4959d19
children faf48511f69d
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Nov 02 09:00:01 2017 +0900
+++ b/SetsCompleteness.agda	Fri Nov 03 13:31:08 2017 +0900
@@ -52,10 +52,9 @@
 open iproduct
 
 SetsIProduct :  {  c₂ : Level} → (I : Obj Sets) (ai : I → Obj Sets )
-     → IProduct ( Sets  {  c₂} ) I
+     → IProduct ( Sets  {  c₂} ) I ai
 SetsIProduct I fi = record {
-       ai =  fi
-       ; iprod = iproduct I fi
+       iprod = iproduct I fi
        ; pi  = λ i prod  → pi1 prod i
        ; isIProduct = record {
               iproduct = iproduct1