From 07a64a3096b1e48fd240d19e51f3448dd9402787 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Tue, 9 Jan 2024 22:36:53 +0100 Subject: Some W-type notes --- example.txt | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'example.txt') 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 -> -- cgit v1.2.3-70-g09d2