"Sizes are Conats"... "Size is a higher inductive type"... when will it end


Today's mood
I really thought Sizes were just going to be inductives and that's that

@ionchy where can I get one of these, I need to hang it up in the boardroom at work

Sign in to participate in the conversation

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.