Some W-type notes

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 ->