Mercurial > hg > Members > kono > Proof > category

diff S.agda @ 663:855e497a9c8f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
introducd HeterogeneousEquality https://stackoverflow.com/questions/44456608/two-fields-record-congruence-in-agda
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Oct 2017 22:42:56 +0900
parents 7194ba55df56
children 749df4959d19
line wrap: on
line diff
--- a/S.agda	Sat Aug 12 16:35:58 2017 +0900
+++ b/S.agda	Sun Oct 22 22:42:56 2017 +0900
@@ -14,6 +14,7 @@
     open import Relation.Binary.Core
     open import Function
     import Relation.Binary.PropositionalEquality
+    open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
     record snat   { c₂ }  { I OC :  Set  c₂ } ( sobj :  OC →  Set  c₂ )
          ( smap : { i j :  OC  }  → (f : I ) →  sobj i → sobj j ) : Set  c₂ where
@@ -25,12 +26,22 @@
 
     open snat
 
-    snat-cong :  { c : Level }  { I OC :  Set  c }  { SObj :  OC →  Set  c  } { SMap : { i j :  OC  }  → (f : I )→  SObj i → SObj j }
+    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' 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)
+              → (snmap-≡ : snmap s ≡ snmap t)
+              → (sncommute-≅ : sncommute s ≅ sncommute t)
+              → s ≡ t
+    snat-cong _ _ refl refl = refl
 
 --This is quite simlar to the answer of 
 --