Introduce a type theory glossary.

The goal here is to provide just enough discussion about type theory
and the basics of applied state counting that we can establish some
language-independent terminology clearly.

A lot of this exists in literature and theory already... but gathering
it in one place, written in one style, in a single page that can be
read top to bottom in one sitting... seems to provide value.
(Sending someone off on a quest to "read wikipedia and all the related
content around concept $X" is great and all, but, ehm.  It's a little
high latency, a little unreliable in outcome, etc.)

This subsumed and replaces the cardinality doc, so that file be yeet.

This was kicked off in large part by discussion over in
#241 (comment) ,
so thanks to @vmx for some of the kick in the shorts to start writing.

Also thanks to @bsunsrud and @BatmanAoD for some polishing and early
feedback on early drafts, and to @Reasonable-Solutions for some review
of the categorical bits, all of which was very helpful.