blob: 21990a4eeae93fcffd910627279a47e08b718510 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
id : (l : Level) -> (a : Set l) -> (x : a) -> a
id = \(l : Level) -> \(a : Set l) -> \(x : a) -> x
unitfoo : (_ : One) -> One
unitfoo = \(Unit : One) -> Unit
-- W-types: https://cs.stackexchange.com/a/55674/45548
-- for any n : Level, B : Set ? and any A : B -> Set ?, the following is allowed:
-- data[W] T : Set n where
-- c : (x : B) -> (_ : A x -> T) -> T
-- TODO: how parametric can n/n1/n2 be?
-- data Nat : Set 0 where
-- zero : Nat
-- succ : Nat -> Nat
-- ~>
-- B = One + One
-- A (inj1 Unit) = Void
-- A (inj2 Unit) = One
-- data[W] Nat : Set 0 where
-- c : (x : B) -> (_ : A x -> Nat) -> Nat
-- data List (C : Set 0) : Set 0 where
-- nil : List C
-- cons : C -> List C -> List C
-- ~>
-- B =
-- data[W] List (C : Set 0) : Set 0 where
-- c :
-- data Vec (A : Set 0) : Nat ->
|
