On type functions

[Joseph Rushton Wakeling]

On Sunday, 3 May 2020 at 09:35:34 UTC, Stefan Koch wrote:
> Let's take something that was designed to express computation, 
> functions, and extend it with the ability to take types as 
> objects.
> The type function is born. (I thought I came up with it, but 
> recently remembered that I first saw it in idris 
> (https://www.idris-lang.org/))

Actually if I remember right you _did_ come up with it 
independently, and then you spoke with me about it and I said "I 
think you should look at Idris, it sounds like they are doing 
something similar..." :-)