Mercurial > hg > Members > kono > Proof > category

changeset 607:caab94e897e6

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, 08 Jun 2017 19:48:02 +0900
parents 92eb707498c7
children 7194ba55df56
files SetsCompleteness.agda
diffstat 1 files changed, 0 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/SetsCompleteness.agda	Thu Jun 08 19:26:12 2017 +0900
+++ b/SetsCompleteness.agda	Thu Jun 08 19:48:02 2017 +0900
@@ -175,14 +175,6 @@
 
 open snat
 
-≡cong2 : { c c' : Level } { A B : Set  c } { C : Set  c' } { a a' : A } { b b' : B } ( f : A → B → C )
-    →  a  ≡  a'
-    →  b  ≡  b'
-    →  f a b  ≡  f a' b'
-≡cong2 _ refl refl = refl
-
-open import Relation.Binary.HeterogeneousEquality as HE renaming ( sym to sym' )
-
 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 ) )