What are the different approaches to handling grammatical number in type theory?

Question

What are the different approaches to handling grammatical number in type theory?

---

This question asks about the type of and in five boys and girls.

That noun phrase is interesting because boys and girls appears with plural morphology and it's not clear to me how to account for it in the somewhat-restrictive type theory setting. It's also not clear whether to ignore the plural morphology completely. Some languages have plurals, but do not use them when there is an explicit numeral.

I remember from a semantics class ages ago that we have two ground types e and t in type theory, where e is the set of individuals and t is the set of truth values. My recollection is fuzzy, but in the form of type theory that we were presented with, e did not contain plural individuals. Indeed, the decisions that English, or the language under study more generally, makes about what things are singular or plural (or mass or count) are baked into the semantics.

I can think of a couple of choices for how to handle plurals like the dogs and dogs. I'm pretty sure that if the dogs has type T, we're forced to give dogs type [T,t].

• extend e to include plural individuals as well, but define an additional predicate P (of type [e,t]) that is true for all plural individuals and false for all singular individuals. the dogs would then have type e
• encode plurals as predicates. the dogs would then have type [e,t]. So, we're identifying the dogs with its membership predicate.
• Add a new ground type p for plural individuals. This gives us a system that's reminiscent of a form of plural logic.

I'm curious which approaches (whether or not they appear in the above list) are commonly used to account for the meaning of plurals.