|
138
|
1 module level1 where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4
|
|
|
5 ex1 : { A B : Set} → Set
|
|
|
6 ex1 {A} {B} = A → B
|
|
|
7
|
|
|
8 ex2 : { A B : Set} → ( A → B ) → Set
|
|
|
9 ex2 {A} {B} A→B = ex1 {A} {B}
|
|
|
10
|
|
266
|
11 ex7 : {A B : Set} → Set _
|
|
|
12 ex7 {A} {B} = lemma2 ( A → B ) _ -- → A → B
|
|
|
13
|
|
138
|
14
|
|
|
15 -- record FuncBad (A B : Set) : Set where
|
|
|
16 -- field
|
|
|
17 -- func : A → B → Set
|
|
|
18
|
|
|
19 record Func {n : Level} (A B : Set n ) : Set (suc n) where
|
|
|
20 field
|
|
|
21 func : A → B → Set n
|
|
|
22
|
|
|
23 record Func2 {n : Level} (A B : Set n ) : Set {!!} where
|
|
|
24 field
|
|
|
25 func : A → B → Func A B
|
