TT.elf

tp : type.

val : tp -> type.
el : tp -> type.
! : val A -> el A.

eq : {A:tp} el A -> el A -> type.

⇓ : el A -> val A -> type. %infix right 11 ⇓.
red : eq A M (! N)
       <- M ⇓ N.

1 : tp.
<> : val 1.
terminal/<> : ! <> ⇓ <>.

2 : tp.
tt : val 2.
ff : val 2.
terminal/tt : ! tt ⇓ tt.
terminal/ff : ! ff ⇓ ff.

+ : tp -> tp -> tp. %infix right 11 +.
inl : el A -> val (A + B).
inr : el B -> val (A + B).
decide : {C:el (A + B) -> tp}
          {M:{u:el A} el (C (! (inl u)))}
          {N:{u:el B} el (C (! (inr u)))}
          {S : el (A + B)} el (C S).
terminal/inl : !(inl M) ⇓ (inl (! N))
                <- M ⇓ N.
terminal/inr : !(inr M) ⇓ (inr (! N))
                <- M ⇓ N.
compute/decide : (decide ([u:el (A + B)] C u) M N (!(inl X))) ⇓ V
                  <- (M X) ⇓ V.

example = decide ([x:el (1 + 1)] 2) ([l] ! tt) ([r] ! ff) (!(inl (! <>))).

%query 1 * eq _ example (! N).