Add a new page:
So it turns out that important concepts in representation theory are just constructions in homotopy theory carried out in a context of symmetries, constructions which in more basic settings are familiar logical operations. For example, the type theoretic construction governing the formation of induced representations, typically first met as very basic way of expanding an action of a subgroup to an action of the full group, is very basic when carried out on sets and predicates. For instance, consider the case of the set of dogs sent by the function "owner" to the set of people, each dog being assigned its (unique) owner. The equivalent of forming an induced representation in this setting is to map any predicate of dogs to a predicate of people, say, "poodle" is sent to "owner of some poodle".