Skip to content

Instantly share code, notes, and snippets.

@johnchandlerburnham

johnchandlerburnham/W.fm

Last active June 23, 2020 16:18
Show Gist options
  • Save johnchandlerburnham/f645a860fafcb48a5746d2ffb825c7d8 to your computer and use it in GitHub Desktop.
Save johnchandlerburnham/f645a860fafcb48a5746d2ffb825c7d8 to your computer and use it in GitHub Desktop.
Download ZIP
W types in Formality
Raw
W.fm
W(A : Type, B : A -> Type) : Type
w<P : W(A,B) -> Type> ->
(sup : (x: A, f: B(x) -> W(A,B)) -> P(W.sup<A,B>(x,f))) ->
P(w)
W.sup<A: Type, B: A -> Type>(x: A, f: B(x) -> W(A,B)) : W(A,B)
<P> (sup) sup(x,f)
T Two
| t0;
| t1;
Nwf(t: Two): Type
case t:
| Empty;
| Unit;
Nw : Type
W(Two,Nwf)
nw0 : Nw
W.sup<Two,Nwf>(t0, (v) Empty.absurd<W(Two,Nwf)>(v))
nw1 : Nw
W.sup<Two,Nwf>(t1, (v) nw0)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment