Mercurial > hg > Members > kono > Proof > category

diff S.agda @ 672:749df4959d19

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix completeness
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 02 Nov 2017 09:00:01 +0900
parents 855e497a9c8f
children
line wrap: on
line diff
--- a/S.agda	Mon Oct 30 18:18:36 2017 +0900
+++ b/S.agda	Thu Nov 02 09:00:01 2017 +0900
@@ -26,12 +26,12 @@
 
     open snat
 
-    snat-cong' :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
-             ( s t :  snat SObj SMap   )
-         → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
-         → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
-         → s ≡ t
-    snat-cong' s t refl refl = {!!}
+    -- snat-cong' :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
+    --          ( s t :  snat SObj SMap   )
+    --      → ( ( λ i  → snmap s i )  ≡  ( λ i →  snmap t i ) )
+    --      → ( ( λ i j f →  smap0 s f ( snmap s i )  ≡ snmap s j   ) ≡ (  ( λ  i j f → smap0 t f ( snmap t i )  ≡ snmap t j ) ) )
+    --      → s ≡ t
+    -- snat-cong' s t refl refl = {!!}
 
     snat-cong : {c : Level}
                 {I OC : Set c}