Inventing a concrete syntax

ind F : ★.

ind T : ★;
I : T.

ind Bool : ★;
true : Bool;
false : Bool.

ind N : ★;
O : N;
S : N → N.

ind Ord : ★
OO : Ord;
OS : Ord → Ord;
OL : (N → Ord) → Ord.

ind Fin : N → ★;
fz : (n:N)Fin (S n);
fs : (n:N)Fin n → Fin (S n).

ind Eq (A:★)(x:A):A → ★;
refl : Eq A x x.

ind JMEq (A:★)(x:A):(B:★)B → ★;
JMrefl : JMEq A x A x.

ind So : Bool → ★;
oh : So true.

ind Ex (T:★)(P:T → ★):★;
witness : (t : T)Prf(P t) → Ex T P.

ind Acc (A:★)(R:A → A → ★):A → ★;
below : ((y:A)R y x → Acc A R y) → Acc A R x.

ind W (A:★)(B:A → ★):★;
sup : (a:A)(f:B a → W A B)W A B.