Mercurial > hg > Members > kono > Proof > category

annotate level-ex.agda @ 246:80d9ef47566b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cong-γ1 done, cong-δ1 remains
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 09 Sep 2013 12:35:56 +0900
parents 3249aaddc405
children d6a6dd305da2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
153
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module level-ex where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 postulate ℓ : Level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 postulate A : Set ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 postulate a : A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 lemma1 : Set ℓ -> A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 lemma1 = \x -> a
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 lemma2 : A -> Set ℓ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 lemma2 = \x -> A
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 lemma3 : Set (suc ℓ)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 lemma3 = A -> Set ℓ