Mercurial > hg > Members > kono > Proof > category

changeset 537:2f261a3836bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 30 Mar 2017 18:11:11 +0900
parents 09beac05a0fb
children d22c93dca806
files SetsCompleteness.agda
diffstat 1 files changed, 12 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Mar 30 17:34:37 2017 +0900
+++ b/SetsCompleteness.agda	Thu Mar 30 18:11:11 2017 +0900
@@ -235,7 +235,16 @@
        }  where
           a0 : Obj Sets
           a0 =  snat  (ΓObj s Γ) (ΓMap s Γ) 
-          e  :  Hom Sets a0 (iproduct I (λ j → ΓObj s Γ j))
-          e  =  λ x → record { pi1  = λ j →  snmap x j }
+          comm2 : { a : Obj Sets } {x : a } {i j : I} (t : NTrans C Sets (K Sets C a) Γ) (f : I → I) 
+             → ΓMap s Γ f (TMap t (small← s i) x) ≡ TMap t (small← s j) x
+          comm2 = {!!}
           limit1 : (a : Obj Sets) → NTrans C Sets (K Sets C a) Γ → Hom Sets a (snat (ΓObj s Γ) (ΓMap s Γ)) 
-          limit1 = {!!}
+          limit1 a t = λ x →  record { snmap = λ i →  ( TMap t ( small← s i ) ) x ;
+              sncommute = λ f → comm2 t f }
+
+
+
+
+
+
+