Mercurial > hg > Members > kono > Proof > category

changeset 542:bc3802c5c8e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
bad
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 Mar 2017 17:44:53 +0900
parents 505962017fd1
children 34f79fafbba4
files SetsCompleteness.agda
diffstat 1 files changed, 6 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Fri Mar 31 10:28:34 2017 +0900
+++ b/SetsCompleteness.agda	Fri Mar 31 17:44:53 2017 +0900
@@ -186,9 +186,10 @@
      { smap : { i j :  OC  }  → (f : I )→  sobj i → sobj j } →
      ( s t :  snat sobj smap ) →
      ( snmap s ≡ snmap t )  → s ≡ t
-snat-cong s t smt=sms =   begin
+snat-cong {c₂} {I} s t smt=sms =   begin
                 record { snmap = snmap s ; sncommute = λ f → sncommute s f }
-             ≡⟨  ≡cong2 ( λ sm sc → record { snmap = sm  ; sncommute = λ f →  ?  }  ) smt=sms  ( irr ? ? ) ⟩
+             -- ≡⟨  ≡cong2 ( λ sm ( sc : I → ? ≡ ?  ) → record { snmap = sm  ; sncommute = λ f → sc f }  ) smt=sms {!!} ⟩
+             ≡⟨ {!!} ⟩
                 record { snmap = snmap t ; sncommute = λ f → sncommute t f }
              ∎   where
                   open  import  Relation.Binary.PropositionalEquality
@@ -260,7 +261,9 @@
                   limit1 a t x
              ≡⟨⟩
                   record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }
-             ≡⟨ {!!} ⟩
+             ≡⟨ snat-cong (  record { snmap = λ i →  ( TMap t i ) x ; sncommute = λ f → comm2 t f }  )  
+                       (record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }  ) 
+                        {!!}   ⟩
                   record { snmap = λ i →  snmap  (f x ) i  ; sncommute = sncommute (f x ) }
              ≡⟨⟩
                   f x