First Class Types?

[ken-okabe]

https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html

In Idris, types are first class, meaning that they can be computed and manipulated (and passed to functions) just like any other language construct.

Is this possible in Kind?

[algebraic-dev]

Yes, e.g.

Choose (n: Bool) : Type
Choose Bool.true = Nat
Choose Bool.false = String