Mercurial > hg > Members > kono > Proof > category
diff negnat.agda @ 822:4c0580d9dda4
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 |
line wrap: on
line diff
--- a/negnat.agda Wed May 01 15:16:54 2019 +0900 +++ b/negnat.agda Wed May 01 21:16:58 2019 +0900 @@ -165,6 +165,29 @@ lemma2 : { n : ℕ } -> isEven (suc (suc n )) ≡ isEven n lemma2 = refl +data One : Set where + * : One + +lemma1 : ( x y : One ) → x ≡ y +lemma1 * * = refl + +lemma2 : {A : Set} ( x : A) → x ≡ x +lemma2 x = refl +open import Data.Empty +open import Relation.Nullary +open import Level +lemma4 : Set (Level.suc Level.zero) +lemma4 = {A : Set} ( x y : A) → ¬ ( ¬ x ≡ y ) + +data A : Set where + x y z : A + +data _==_ : ( a b : A ) → Set where + x=y : x == y + +lemma3 : ( a b : A ) → a == b → ¬ a ≡ b +lemma3 _ _ x=y = λ () +