Mercurial > hg > Members > kono > Proof > category

changeset 544:158aaded24b9

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 Sat, 01 Apr 2017 15:20:29 +0900
parents 34f79fafbba4
children cb0d01f1eec9
files SetsCompleteness.agda
diffstat 1 files changed, 2 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Sat Apr 01 15:18:14 2017 +0900
+++ b/SetsCompleteness.agda	Sat Apr 01 15:20:29 2017 +0900
@@ -191,7 +191,7 @@
 snat-cong {_} {I} {OC} SO SM {s} {t}  eq1  eq2 eq3 = ≡cong2 ( λ x y → record { snmap = λ i → x i ; sncommute =  λ {i} {j} f → {!!} } )  
               ( extensionality Sets  ( λ  i  → eq1 i ) )
               ( extensionality Sets  ( λ  i  → ( extensionality Sets  ( λ  j  → ( extensionality Sets  ( λ  f  → 
-                    irr1 i j f  {!!} {!!}))))))
+                    irr1 i j f  ? ? ))))))
    where
       irr1 : ( i j : OC ) ( f : I )  →  ( es et : SM f ( snmap s i )  ≡ snmap s j )  → es ≡ et 
       irr1 i j f es et = {!!}
@@ -261,7 +261,7 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
-             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) ?  {!!} {!!} ⟩
+             ≡⟨ snat-cong (ΓObj s Γ) (ΓMap s Γ) {!!}  {!!} {!!} ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x