Rename UU-Fin to Type-With-Cardinality-ℕ

[fredrik-bakke]

No description provided.

[fredrik-bakke]

This is my last univalent combinatorics PR for the time being.

[fredrik-bakke]

We could also consider the slightly shorter name Type-With-Cardinality-ℕ.

EDIT: I went for this name.

[EgbertRijke]

This pull request contains some big improvements, so I am ready to merge it.

On the other hand, it also brings to the surface a problem that we will need to address at some point. It is really strange to name a group after the specification of its classifying type. Instead, the group should be named after the symmetries it contains. For example, Type-Of-Squares-Group would be a really strange name for the dihedral group. We create this sort of problems when we write Type-With-Cardinality-N-(Concrete-)Group.

Probably the best solution would be to create a separate file for pointed connected types, have the type of types with cardinality n be a pointed connected type, and introduce the nth symmetric concrete group as the pointed connected type of types with cardinality n.