Mercurial > hg > Members > kono > Proof > category

comparison negnat.agda @ 822:4c0580d9dda4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
from cart to graph, hom equality to set equality
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 May 2019 21:16:58 +0900
parents 2f07f4dd9a6d
children
comparison
equal deleted inserted replaced
821:fbbc9c03bfed 822:4c0580d9dda4
163 lemma1 : { n : ℕ } -> mod (suc (suc n )) ≡ mod n 163 lemma1 : { n : ℕ } -> mod (suc (suc n )) ≡ mod n
164 lemma1 = refl 164 lemma1 = refl
165 lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n 165 lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n
166 lemma2 = refl 166 lemma2 = refl
167 167
168 data One : Set where
169 * : One
170
171 lemma1 : ( x y : One ) → x ≡ y
172 lemma1 * * = refl
173
174 lemma2 : {A : Set} ( x : A) → x ≡ x
175 lemma2 x = refl
168 176
169 177
178 open import Data.Empty
179 open import Relation.Nullary
180 open import Level
170 181
182 lemma4 : Set (Level.suc Level.zero)
183 lemma4 = {A : Set} ( x y : A) → ¬ ( ¬ x ≡ y )
184
185 data A : Set where
186 x y z : A
187
188 data _==_ : ( a b : A ) → Set where
189 x=y : x == y
190
191 lemma3 : ( a b : A ) → a == b → ¬ a ≡ b
192 lemma3 _ _ x=y = λ ()
193