Mercurial > hg > Members > kono > Proof > category

annotate level-ex.agda @ 872:bfe0215593b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
decidablity of < f , g > is required
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Apr 2020 07:54:18 +0900
parents d6a6dd305da2
children
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
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
11 lemma1 : Set ℓ → A
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
12 lemma1 = λ x → a
153
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
14 lemma2 : A → Set ℓ
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
15 lemma2 = λ x → A
153
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 ℓ)
300
d6a6dd305da2 arrow and lambda fix
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 153
diff changeset
18 lemma3 = A → Set ℓ