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?

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 := {xin U | exists m,starintext{fun}(mtimes m,m),1in m. x = langle m,langle star,1rangleranglewedge 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)$,$langlecdot,cdotrangle$ and $cdottimescdot$ as nothing but *macros* with the expansions

begin{align*}

langle x,yrangle &:= {x,{x,y}}\

xtimes y &:={win U | exists uin x,vin y. w = langle u,vrangle}\

text{fun}(A,B)&:={alphain mathcal P(Atimes B) | forall uin A. exists! vin B. langle u,vrangleinalpha}.

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 $Ato B$. In this system we would simply define the type of monoids as

$$text{Mon}_M := Sigma_{M:Type}Sigma_{star:(Mtimes Mto 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 Ato Brrb_sigma := text{fun}(llb Arrb_sigma,llb Brrb_sigma)$$
- Supposing $x:Avdash t:B$ we encode lambda abstractions as

$$llb lambda x:A.trrb_sigma := {win llb Arrb_sigmatimes llb Brrb_sigma | forall uinllb Arrb_sigma, vinllb Brrb_sigma. w = (u,v)implies v = llb trrb_{sigma,xmapsto u}}$$
- and a variable $x:A$ as

$$llb xrrb_sigma := sigma(x).$$
- Given a type family $B:Ato text{Type}$ (written this way for simplicity), we encode dependent sums as

$$llbSigma_{x:A}Brrb_sigma :={zin llb Arrb_sigmatimesllb text{Type}rrb_sigma |

forall xinllb Arrb_sigma,yinllb text{Type}rrb_sigma. z = (x,y)implies \ yin llb Brrb_sigma(x)}.$$
- We can encode equality as

$$llb s =_A trrb_sigma := {xin{emptyset} | llb srrb_sigma = llb trrb_sigma}$$
- and a proof $p: s =_A t$ is encoded

$$llb prrb_sigma := emptyset.$$

And of course, one should check that for every $t : A$, the encoding satisfies

$$llb trrb_{[]} in llb Arrb_{[]}qquadtext{(for $[]$ the empty valuation)}.$$

Now if we take $M:text{Mon}_M$, $llb Mrrb_{[]}$ 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 Mrrb$ 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.