diff options
| -rw-r--r-- | example.txt | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/example.txt b/example.txt index 29ab618..21990a4 100644 --- a/example.txt +++ b/example.txt @@ -3,3 +3,30 @@ 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 -> |