Mathematical object described irrespective of a foundational system?

Question

Is there a mathematical discipline that studies mathematical objects based on their behavior rather than their encoding?

I ask because a group is classically defined as a set with a binary operation and a handful of axioms. But I am learning type theory, and I am able to define a group as a type with a binary function and some constraints. The set theoretic and type theoretic formulations have different encodings, and yet I still believe I am working with the same mathematical object despite different foundational systems.

Is category theory or some other discipline capable of abstracting away the details of how an object like a group is encoded and instead define them on the basis of behavior that should be encoding-irrelevant?

Answer 1

I would argue that type theory is precisely such a discipline, that is we can view type theory as a language designed to manipulate certain types of objects independently of their encoding.

Let me be precise in what I mean by encoding here. To do mathematics we in any case need a foundational system. That is a system which tells us how to construct valid mathematical objects in a consistent manner. Set theory does this very well, because it allows us to define objects of just about any complexity. Let us call set theory System S. Let me be very explicit and remark that in System S with an appropriate set theoretic universe $U$, we usually define the set of monoids (for simplicity) as the set

$$\text{Mon}_S := \{x\in U\ |\ \exists m,\star\in\text{fun}(m\times m,m),1\in m. x = \langle m,\langle \star,1\rangle\rangle\wedge \phi(m,\star,1)\}$$

where $\phi(m,\star,1)$ ensures the identity and associativity axioms $\mathcal A$.

In particular, I prefer to think of the operations $\text{fun}(\cdot,\cdot)$,$\langle\cdot,\cdot\rangle$ and $\cdot\times\cdot$ as nothing but macros with the expansions \begin{align*} \langle x,y\rangle &:= \{x,\{x,y\}\}\\ x\times y &:=\{w\in U\ |\ \exists u\in x,v\in y. w = \langle u,v\rangle\}\\ \text{fun}(A,B)&:=\{\alpha\in \mathcal P(A\times B)\ |\ \forall u\in A. \exists! v\in B. \langle u,v\rangle\in\alpha\}. \end{align*}

Let us now suppose we have a type theory System M with universe $\text{Type}$, equality types $s =_A t$, dependent sums $\Sigma_{x:A}B$, and arrow types $A\to B$. In this system we would simply define the type of monoids as $$\text{Mon}_M := \Sigma_{M:Type}\Sigma_{\star:(M\times M\to M)}\Sigma_{1:M}P(M,\star,1)$$ where $P(M,\star,1)$ are the type-theoretic monoid axioms. $\newcommand{\llb}{[\![}\newcommand{\rrb}{]\!]}$

What is important here is that we can encode System M into System S as follows

• For a suitable set universe $U$ we encode $$\llb \text{Type}\rrb_\sigma := U$$
• The function space is encoded $$\llb A\to B\rrb_\sigma := \text{fun}(\llb A\rrb_\sigma,\llb B\rrb_\sigma)$$
• Supposing $x:A\vdash t:B$ we encode lambda abstractions as $$\llb \lambda x:A.t\rrb_\sigma := \{w\in \llb A\rrb_\sigma\times \llb B\rrb_\sigma\ |\ \forall u\in\llb A\rrb_\sigma, v\in\llb B\rrb_\sigma. w = (u,v)\implies v = \llb t\rrb_{\sigma,x\mapsto u}\}$$
• and a variable $x:A$ as $$\llb x\rrb_\sigma := \sigma(x).$$
• Given a type family $B:A\to \text{Type}$ (written this way for simplicity), we encode dependent sums as $$\llb\Sigma_{x:A}B\rrb_\sigma :=\{z\in \llb A\rrb_\sigma\times\llb \text{Type}\rrb_\sigma\ |\ \forall x\in\llb A\rrb_\sigma,y\in\llb \text{Type}\rrb_\sigma. z = (x,y)\implies \\ y\in \llb B\rrb_\sigma(x)\}.$$
• We can encode equality as $$\llb s =_A t\rrb_\sigma := \{x\in\{\emptyset\}\ |\ \llb s\rrb_\sigma = \llb t\rrb_\sigma\}$$
• and a proof $p: s =_A t$ is encoded $$\llb p\rrb_\sigma := \emptyset.$$

And of course, one should check that for every $t : A$, the encoding satisfies $$\llb t\rrb_{[]} \in \llb A\rrb_{[]}\qquad\text{(for $[]$ the empty valuation)}.$$

Now if we take $M:\text{Mon}_M$, $\llb M\rrb_{[]}$ is the encoding of the monoid $M$ in System S, although this encoding is a bit more complicated than the definition of a monoid directly in System S described by $\text{Mon}_S$.

Now why should we bother going through all this effort? The reason is that the definition of a monoid in this type theory is much better behaved than that in set theory. What System M does is give a coarser abstraction layer above System S. So whereas it would make sense to ask a meaningless question such as whether $\emptyset \in \llb M\rrb$ in System S, such a question cannot even be stated within System M. In fact, the only things that can be stated about $M$ are statements in the theory of monoids, unless we add assumptions about $M$. This explains how type theory gives us a way to talk about objects independently of their encoding.