Mercurial > hg > Members > kono > Proof > category

comparison record-ex.agda @ 153:3249aaddc405

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sync
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 17 Aug 2013 21:09:34 +0900
parents
children d6a6dd305da2
comparison
equal deleted inserted replaced
152:5435469c6cf0 153:3249aaddc405
1 module record-ex where
2
3 data _∨_ (A B : Set) : Set where
4 or1 : A -> A ∨ B
5 or2 : B -> A ∨ B
6
7 postulate A B C : Set
8 postulate a1 a2 a3 : A
9 postulate b1 b2 b3 : B
10
11 x : ( A ∨ B )
12 x = or1 a1
13 y : ( A ∨ B )
14 y = or2 b1
15
16 f : ( A ∨ B ) -> A
17 f (or1 a) = a
18 f (or2 b) = a1
19
20 record _∧_ (A B : Set) : Set where
21 field
22 and1 : A
23 and2 : B
24
25 z : A ∧ B
26 z = record { and1 = a1 ; and2 = b2 }
27
28 xa : A
29 xa = _∧_.and1 z
30 xb : B
31 xb = _∧_.and2 z
32
33 open _∧_
34
35 ya : A
36 ya = and1 z
37
38 open import Relation.Binary.PropositionalEquality
39
40 data Nat : Set where
41 zero : Nat
42 suc : Nat -> Nat
43
44 record Mod3 (m : Nat) : Set where
45 field
46 mod3 : (suc (suc (suc m ))) ≡ m
47 n : Nat
48 n = m
49
50 open Mod3
51
52 Lemma1 : ( x : Mod3 ( suc (suc (suc (suc zero))))) ( y : Mod3 ( suc zero ) ) -> n x ≡ n y
53 Lemma1 x y = mod3 y
54