A friendly little systems language with first-class types. https://github.com/pikelet-lang
Yay I managed to implement "Gentle art of levitation", including the levitation part. I had to change to a bidirectional core language to make it work. Here is the description of Descriptions in its full beauty:
DescD =
ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^) (ConD^ (True^2, Unit^2))
(ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^)
(ConD^ (False^2, True^2, Type, \x. ConD^ (False^2, False^2, False^2, Lift lower x, ConD^ (True^2, Unit^2), Unit^2), Unit^2))
(ConD^ (False^2, True^2, Bool^, \x. (elim BoolDesc^) (ConD^ (False^2, False^2, True^2, ConD^ (True^2, Unit^2), Unit^2))
(ConD^ (False^2, True^2, Type, \x. ConD^ (False^2, False^2, True^2, ConD^ (True^2, Unit^2), Unit^2), Unit^2)) (lower x), Unit^2)) (lower x), Unit^2)) (lower x), Unit^2);
😅
^
and ^2
noise is the lifting from the universe hierarchy
DescD : Desc^ =
SumD^ End^ ( -- End : Desc
SumD^ (Arg^ Type (\A. HInd^ (Lift A) End^)) ( -- Arg : (A : Type) -> (A -> Desc) -> Desc
SumD^ (Ind^ End^) -- Ind : Desc -> Desc
(Arg^ Type (\_. Ind^ End^)))); -- HInd : Type -> Desc -> Desc