# Should Type Theory replace Set Theory as the Foundation of Mathematics ?

Thorsten Altenkirch

##  1 Introduction

Set theory is usually traced back to Cantor who used sets in an informal way
giving rise to what is called _naive set theory_. Nowadays we usually refer to
axiomatic set theory which was formulated by Zermelo and Fraenkel and which is
called Zermelo-Fraenkel Set Theory or short ZFC. When saying Set Theory 111I
am capitalising both Set Theory and Type Theory when referring to specific
theories with this name not in the sense of a set theory or a type theory. we
mean ZFC.

Type Theory was introduced by Per Martin-Löf [ML75] and there are several
incarnations. The early _Extensional Type Theory_ (ETT) [MLS84] gave way to
_Intensional Type Theory_ (ITT) [NPS90] but recently, heavily influenced by
Voevodsky using concepts from Homotopy Theory, Homotopy Type Theory (HoTT)
[Uni13] was developed. 222Since not everybody wants to read the whole book,
introductory presentations of HoTT include [Alt19, AN19, Gra18]. When saying
Type Theory we mean HoTT.

In Set Theory all mathematical objects are viewed as sets and we write $a\in
A$ to mean that $a$ is an element of the set $A$. Since in modern Set Theory
we don’t use _urelements_ , $a$ is a set again, a process that only stops at
the empty set $\\{\\}$. The same element can occur in different sets and two
sets are equal iff they have the same elements (axiom of extensionality).

Set Theory is based on classical logic 333There are alternatives like CZF and
IZF that are based on intuitionistic logic, see [Cro20] , formally it is
presented in the framework of first order predicate logic. Set Theory can be
viewed as an alternative to higher order logic where the quantification over
predicates is replaced by quantifying over sets, corresponding to predicates.
There are alternative set theories which use intuitionistic predicate logic as
the framework but they all have in common that we first fix the logic as a
framework and then formulate the set theory within this logic.

Type Theory is based on the idea that all mathematical objects belong to a
type and can only be understood as elements of a given type. This corresponds
to mathematical practice where we conceive of a statement quantifying over all
natural numbers as only talking about those while in Set Theory this is
represented by quantifying over all sets and singling out those which are
elements of a particular one, the set of natural numbers. In Type Theory an
element can only be an element of one type 444I am here presenting a pure form
of Type Theory. They are extensions which allow subtyping, which is usually an
attempt to recover features of Set Theory. I prefer to view these sort of
developments as notational conveniences as opposed to foundational features.
hence we cannot talk about elements in isolation which means we cannot reason
about representations. This discipline enables a high degree of extensionality
which is realised by Voevodsky’s univalence axiom entailing that isomorphic
structures are equal.

Types have elements which we write as $a:A$ meaning $a$ is an element of type
$A$. While superficially similar to the set-theoretic $a\in A$ it is
fundamentally different. Saying $a:A$ is part of the static structure of a
mathematical text, only texts which use types consistently make sense. In
particular we cannot ask whether $a:A$ because this is an aspect of our text
not the subject we are talking about. We say that $a:A$ is a judgement not a
proposition.

The formal presentation of Type Theory also requires another judgement which
is called definitional or judgemental equality. E.g. when we define
$n:\mathbb{N}$ as $n:\equiv 3$ we also know that $(1,2,3):\mathbb{N}^{n}$ but
to see this we need to exploit the fact that $n\equiv 3$ statically. Again
$a\equiv b$ is a judgement which is a static property of a mathematical text
not a predicate. Judgemental equality also reflects the computational
character of Type Theory, e.g. we know that all (closed) natural number
expressions can be reduced to a numeral, e.g. $3+4\equiv 7$. Type Theory also
introduces _propositional equality_ but it makes sense to distinguish the
static judgemental equality from the usual propositional equality. Indeed
being equal by definition is a common phrase in mathematics.

Mathematicians often consider ZFC as the only foundation of mathematics, and
frequently don’t actually want to think much about foundations. We argue here
that modern Type Theory, i.e. HoTT, is a preferable and should be considered
as an alternative. We will look at different aspects of type-theoretic and
set-theoretic foundations and compare the two: we start with the different
approaches to logic, we consider the question of representations and in
particular representation independence, which leads to the univalence
principle which changes the way we understand equality. Then we discuss the
relation between the two central aspects where Type Theory and Set Theory are
different: structuralism and constructivity and make the novel observation
that the two are connected. We conclude with a personal reflection which also
includes a short summary of the basic idea of the type theoretic approach.

##  2 Related work

In [Mad19] the author develops a set of criteria for possible foundations and
compares Set Theory, category theory and Homotopy Type Theory using these
criteria. First of all it seems rather misleading to include category theory
as a possible foundation because while it provides _essential guidance_ (one
of the criteria) it requires another foundation to explain what basic
constructions are intuitively permissible. 555Indeed in [Mad19], Maddy
complains: _I don’t know what Voevodsky finds lacking in category-theoretic
foundations – perhaps that it fails to provide a Generous Arena?_ Indeed
categorical guidance can be misleading since it would suggest that symmetric
cartesian categories would be a good concept but you need to go beyond
category theory to see that only preorders satisfy this condition. However,
category theory, fits very well with HoTT, indeed the universal properties
have unique solutions in HoTT, while they are only unique up to isomorphisms.
Maddy in [Mad19], footnote 28, admits that she is _not sure what these
thinkers take to be wrong with ZFC_ , where the thinkers seem to refer to
Voevodsky and others. It is the purpose of this paper to explain what we think
is wrong with ZFC and can be addressed by using HoTT. Maddy also argues that
she thinks that HoTT would need to adopt the axiom of choice to be able to
encode the classical theory of sets 666In loc.cit, p.29: _But to get even to
ETCS, we have to add the axiom of choice,_ where ETCS stands for _The
Elementary Theory of the Category of Sets_ — which is in my experience a
common reaction of philosophers who are only too willing to give in to
intimidation by classical mathematicians and let them define the yardsticks of
mathematics. Her conclusion is that there is no problem with set theory and
that the only advantage HoTT would have to offer is proof checking. While it
is doubtful that this even correct (there are proof systems based on classical
mathematics), it is also misleading. What we try to argue in this paper is
that the fundamental point of HoTT is conceptual, the fact that it lends
itself to implementation is a welcome additional benefit.

Our views are similar to [Awo14] who explains why HoTT is essential for
structural mathematics. The present paper is different in that we emphasise
also the constructive aspects of HoTT and relate them to its structural
properties.

##  3 The role of logic

Type Theory does not rely on predicate logic as a framework but introduces
logic using the propositions as types explanation — in this sense logic is an
emergent aspect of Type Theory not a prerequisite. In constructive thinking we
acknowledge that mathematical constructions are taking place in our heads and
that we communicate them using shared intuitions. From this point of view, it
is not the notion of truth which is fundamental but the notion of evidence or
proof. A proposition is given by saying what we need as evidence to accept
that the proposition holds. In the context of Type Theory we can do this by
assigning to every proposition the type of evidence for this proposition. This
is also called the Curry-Howard equivalence but this is based on the
assumption that we already have a logic and a Type Theory and then observe a
formal relationship between the two, while I _define_ logic by the
translation. 777The propositions as types explanation is also related to the
Brouwer-Heyting-Kolmogorov (BHK) semantics which introduces untyped realisers
of propositions.

The translation of propositional connectives into type theoretic connectives
is rather straightforward, for example we translate implication $P\Rightarrow
Q$ as the function type $P\to Q$ between the associated types of evidence
which I denote by the same letters here 888To be more precise we can introduce
an operation $\mathrm{Prf}$ which assign to every proposition $P$ te type of
its proofs $\mathbf{Prf}(P)$ and then we stipulate that
$\mathbf{Prf}(P\Rightarrow Q)\equiv\mathbf{Prf}(P)\to\mathbf{Prf}(Q)$. . The
idea is that evidence for $P$ implies $Q$ is a function which maps evidence
for $P$ into evidence of $Q$ — function types are a primitive concept of Type
Theory 999We explain a function as _black box_ where we can input elements of
the domain and which outputs elements of the codomain. While we have no access
to the mechanism (hence the box is black) the only way to actually construct a
function is via effective means. However, the theory works as well if we
believe in some sort of magic, like that everything is decidable (the
principle of the excluded middle). Formally, the properties of functions are
represented by the laws of $\lambda$-calculus and the principle of functional
extensionality.. Similar we can translate $\forall x:A.P(x)$ by the dependent
function type 101010The dependent function type is a generalisation of the
usual function type where the codomain can vary over the domain. This
corresponds to the cartesian product of a family of sets in Set Theory, hence
the use of $\Pi$ denoted as $\Pi x:A.P(x)$, the idea is that evidence for a
universally quantified statement is a (dependent) function that assigns to
every element $a:A$ evidence for $P(a)$. Negation $\neg P$ we interpret as
saying that $P$ is impossible means $P$ implies falsum
($P\Rightarrow\mathrm{False}$) where falsum ($\mathrm{False}$) is interpreted
as the empty type.

The translation of disjunction and existential quantification depends on what
exactly we mean by a proposition. Here there has been a historic change mainly
since the introduction of HoTT. In ITT we identified types and propositions
which leads to some strange artefacts. For example we would denote a subset
$\\{x:A\mid P(x)\\}$ as the type of dependent pairs $(a,p)$ where $a:A$ and
$p:P(a)$ (this is written as $\Sigma x:A.P(x)$) 111111The justification for
this notation is similar as before, in Set Theory the type of dependent pairs
corresponds to an infinite sum hence $\Sigma$. . Now the embedding from the
subset into $A$ is given by the first projection $\pi_{1}:\\{x:A\mid
P(x)\\}\to A$ 121212Here $\pi_{1}:\Sigma x:A.B(x)\to A$ is defined as
$\pi_{1}(a,b)\equiv a$ and $\pi_{2}:\Pi p:\Sigma x:A.B(x).B(\pi_{1}(p))$ with
$\pi_{2}(a,b)\equiv b$.. However, it turns out that this is not in general an
injection since we can have different proofs $p$ for the same element $a$.
Also the naive translation of existential statements uses again dependent
pairs, i.e. evidence for $\exists x:A.P(x)$ is given by a pair $(a,p)$ with
$a:A$ and $p:P(a)$, we write this type as $\Sigma x:A.P(x)$ as before.
However, this interpretation of existence gives rise to an apparent proof of
the axiom of choice: if we know that for all $x:A$ there exists a $y:B$ such
that a certain relation $R(x,y)$ holds then we can extract the witness and its
justification from the proof. More precisely we can define

$\displaystyle\mathrm{ac}:(\forall x:A.\exists y:B.R(x,y))\to\exists f:A\to
B.\forall x:A.R(x,f(x))$ $\displaystyle\mathrm{ac}(f)=(\lambda
a.\pi_{1}(f(a)),\lambda a.\pi_{2}(f(x)))$

However, this _type theoretic axiom of choice_ hardly corresponds to the axiom
of choice as it is used in Set Theory. Indeed, it is not an axiom but just a
derivable fact.

In HoTT we say a proposition is a type with at most one element. The idea here
is that a proposition should not contain any additional information, its only
purpose is to assert something. As a consequence of univalence we obtain that
two propositions are equal if they are logically equivalent — this is called
propositional extensionality. The embedding from a subset to a set
($\pi_{1}:\\{x:A\mid P(x)\\}\to A$) is now an injection because there is at
most one proof that the proposition $P(a)$ holds. To translate disjunction and
existence we use propositional truncation, that is to any type $A$ we
introduce a proposition $||A||$ which corresponds to the proposition that $A$
is inhabited. 131313Formally, $||A||$ can be defined as a higher inductive
type with two constructors $|-|:A\to||A||$ and $\mathrm{is-prop}:\forall
xy:||A||.x=y$. That is if there is an element $a:A$ we obtain an element of
$||A||$ but we cannot distinguish them anymore. Now we can say that a proof of
existence, i.e. evidence for $\exists x:A.P(x)$ is the propositional
truncation of the naive translation, i.e. $||\Sigma x:A.P(x)||$. Given this
interpretation the translation of

$(\forall x:A.\exists y:B.R(x,y))\to\exists f:A\to B.\forall x:A.R(x,f(x))$

is not provable since we extract an element from a propositional truncation
which is clearly wrong because here all elements have been identified. And
indeed this formulation of the axiom of choice has the power of the classical
axiom, in particular we can derive the excluded middle using Diaconescu’s
construction.

By the principle of the excluded middle 141414The term _excluded middle_
doesn’t actually reflect its meaning. _Excluded_ clearly is a negative
statement, hence we should render it is saying _It cannot be that a
proposition is neither true nor false_ , which can be translated is
$\neg\neg(P\vee\neg P)$, which _is_ constructively provable. A better term for
the universal assertion of $P\vee\neg P$, would be _universal decidability_ or
_magicae nigrae_ in latin. we mean

$\forall P:\mathbf{Prop}.P\vee\neg P$

Here I write $\mathbf{Prop}$ for all _propositional types_ , i.e. types with
at most one element and $P\vee Q$ is the translation of disjunction using
propositional truncation, ie. $||P+Q||$ 151515Here $A+B$ is the coproduct or
binary sum in Type Theory corresponding to disjoint union in Set Theory. It
can be defined as $A+B=\Sigma b:\mathrm{Bool}.P(B)$ with
$P(\mathrm{true})\equiv A$ and $P(\mathrm{false})\equiv B$. . Actually in this
particular example we don’t need to truncate because it can never happen that
both $P$ and $\neg P$ hold. Clearly there is no function which assigns to
every proposition either a proof of it or a proof of its negation. We don’t
even need to appeal to the undecidability of our logic but observe that we
cannot look _into_ a proposition due to propositional extensionality. Hence
excluded middle seems to suggest that we can decide any proposition without
even looking at it!

However, we can justify excluded middle by a different translation of the
connectives and a different explanation what is a proposition. That is we can
interpret $P\vee_{\mathrm{class}}Q$ as the statement that not both are false
$\neg(\neg P\wedge\neg Q)$ and similar we can explain existence
$\exists_{\mathrm{class}}x:A.P(x)$ by saying it is not the case that $P$ is
always false, i.e. $\neg(\forall x:A.\neg P(x))$. Note that we don’t need any
truncation because negated statements are always propositions. Moreover the
translations are valid equivalences in classical logic. However, to obtain the
correct behaviour of the connectives, in particular to justify reasoning by
cases and the elimination rule of the existential, we need to limit
propositions to the negative ones, i.e. to the ones for which proof by
contradiction holds, that is we define
$\mathbf{Prop}_{\mathrm{c}lass}=\\{P:\mathbf{Prop}\mid\neg\neg P\to P\\}$. So
for example if we know $P\vee Q$ and $P\to R$ and $Q\to R$ we can conclude
$\neg\neg R$ and if $R$ is negative we also know $R$. Similar reasoning
justifies the rule of existential elimination. Moreover the remaining
connectives preserve the property of being negative. The negative translation
I have described here is called the Gödel-Gentzen translation, first described
by Gödel [Göd33].

We may think that there is no difference between propositions as types with at
most one element and negative propositions because in neither case can we
extract information. However, while the axiom of choice is unprovable in both
cases, the axiom of unique choice is provable for the type theoretic
interpretation of propositions, that is

$\displaystyle\mathrm{auc}:(\forall x:A.\exists!y:B.R(x,y))\to\exists f:A\to
B.\forall x:A.R(x,f(x))$ $\displaystyle\mathrm{auc}(f)=(\lambda
a.\pi_{1}(f(a)),\lambda a.\pi_{2}(f(x)))$

where $\exists!x:A.P(x)$ means _unique existence_ which can be defined as

$\exists x:A.P(x)\wedge\forall y:A.P(y)\Rightarrow x=y.$

This can be proven in Type Theory because the statement of unique existence is
already a proposition anyway and hence we can extract the witness. However,
using the negative translation we cannot justify unique choice.

##  4 Representation

To illustrate the difference between Set Theory and Type Theory let’s look at
the representation of numbers, starting with the natural numbers. In Set
Theory natural numbers are encoded using only sets, the most common encoding
is due to von Neumann:

$\displaystyle 0$ $\displaystyle=\\{\\}$ $\displaystyle 1$
$\displaystyle=\\{0\\}$ $\displaystyle 2$ $\displaystyle=\\{0,1\\}$
$\displaystyle\vdots$ $\displaystyle\quad\vdots$ $\displaystyle n$
$\displaystyle=\\{0,1,\dots,n-1\\}$

However, there are many alternative ways, e.g. the following is due to
Zermelo:

$\displaystyle 0$ $\displaystyle=\\{\\}$ $\displaystyle 1$
$\displaystyle=\\{0\\}$ $\displaystyle 2$ $\displaystyle=\\{1\\}$
$\displaystyle\vdots$ $\displaystyle\quad\vdots$ $\displaystyle n$
$\displaystyle=\\{n-1\\}$

So for example the number 3 is represented as
$\\{\\{\\},\\{\\{\\}\\},\\{\\{\\},\\{\\{\\}\\}\\}$ using von Neumann’s
encoding and as $\\{\\{\\{\\}\\}\\}$ in Zermelo’s. The axiom of infinity uses
one particular representation to introduce the existence of the infinite set
of natural numbers, e.g. von Neumann’s, and using the axiom of replacement we
can deduce that the alternative representation, e.g. Zermelo’s also forms a
set.

We can formulate properties that distinguish the two representations, for
example in von Neumann’s encoding we have that $n\subseteq n+1$ which fails in
Zermelo’s, e.g. $1\not\subseteq 2$ if we use Zermelo’s encoding. This
statement is not really a statement about numbers but about their encoding, we
say it is not structural. Mathematicians would normally avoid non-structural
properties, because they entail that results are may not be transferable
between different representations of the same concept. However, frequently
non-structural properties are exploited to prove structural properties and
then it is not clear whether the result is transferable.

In Type Theory natural numbers are an example of an inductive type, defined by
the constructors. Following Peano we say that natural numbers are generated
from $0:\mathbb{N}$ and $\mathrm{suc}:\mathbb{N}\to\mathbb{N}$ (the successor,
$\mathrm{suc}(n)$ means $n+1$). To define functions out of the natural numbers
we use an elimination principle that allows us to perform dependent recursion,
that is given a family of types indexed by the natural numbers
$M:\mathbb{N}\to\mathbf{Type}$ and an element $z:M(0)$ and $s:\Pi
n:\mathbb{N}.M(n)\to M(\mathrm{suc}(n))$ we can define a function $f:\Pi
n:\mathbb{N}.M(n)$ with the definitional equalities $f(0)\equiv m(0)$ and
$f(\mathrm{suc}(m))\equiv s(n,f(n))$. The elimination principle allows us to
define functions like addition but also to derive properties, e.g. that
addition forms a commutative monoid exploiting the propositions as types
explanation.

The definition of the natural numbers precisely identifies the structural
properties of the type: it is equivalent to stating that $\mathbb{N}$ is an
initial algebra, a natural number object, in the language of category theory.
And because we cannot talk about elements in isolation it is not possible to
even state non-structural properties of the natural numbers. Indeed, we cannot
distinguish different representations, for example using binary numbers
instead.

Both in Set Theory and in Type Theory we can go on and construct more
elaborate sets/types of numbers, e.g.
$\mathbb{Z},\mathbb{Q},\mathbb{R},\mathbb{C}$. In Set Theory we can talk about
subsets, e.g. we may want to stipulate that $\mathbb{N}\subseteq\mathbb{Z}$
but it turns out that this doesn’t hold for the most natural choice of
encodings. 161616E.g. we may represent integers as equivalence classes of
pairs of natural numbers with the same difference, i.e. $(a,b)=(c,d)$ if
$a+d=c+b$.. Yes, we can start with the biggest number class we want to
represent and then define the other ones as subsets via comprehension.

In Type Theory the notion of a subset doesn’t make sense in general for types.
We can observe that we have a canonical embedding function between the
different number types, e.g. $\mathbb{N}\to\mathbb{Z}$ and we can agree
notationally that we can omit this function when it is clear from the context
that we use a natural number when an integer was required.

While we don’t have a notion of subset on types, we can talk about subsets of
a given type $A$ which are just propositionally valued functions
$P:A\to\mathbf{Prop}$. Given any two of such subsets we can define $P\subseteq
Q$ as $\forall x:A.P(x)\to Q(x)$ in Type Theory. This means we can actually
play the same trick as in Set Theory and define our number classes as subsets
of the largest number class we want to consider and we have indeed the subset
relations we may expect.

Hence Type Theory allows us to do basically the same things as Set Theory as
far as numbers are concerned (modulo the question of constructivity) but in a
more disciplined fashion limiting the statements we can express and prove to
purely structural ones.

One may think that Type Theory is somehow less minimalistic, while in Set
Theory we only need $\\{\dots\\}$ to represent all mathematical concepts there
seems to be quite a menagerie of type constructors: $\Pi$-types,
$\Sigma$-types, equality types and so on. However, to be fair we should
compare the axioms of Set Theory with the basic constructions of Type Theory.
And indeed while in applied Type Theory we may introduce a lot of apparently
unrelated types we can often reduce them to a basic collection. So for example
most inductive constructions can be reduced to the type of well-founded trees
or $W$-types. The reduction of more advanced type constructors such as Higher
Inductive-Inductive types (HIITs) are subject of current work, similar to the
question whether advanced set theoretic constructions can be reduced to some
axioms.

##  5 Univalence and equality

Type Theory doesn’t allow us to make statements about representations because
we cannot talk about elements in isolation. This means that we cannot observe
intensional properties of our constructions. This already applies to
Intensional Type Theory, so for example we cannot observe any difference
between two functions which are pointwise equal. However, on the other hand in
ITT we cannot prove them to be equal either. This is a consequence of the way
the equality type is treated in ITT. That is for any element $a:A$ there is a
canonical element of the equality type $\mathrm{refl}(a):a=a$. Now consider
$f,g:\mathbb{N}\to\mathbb{N}$ with

$\displaystyle f(x)$ $\displaystyle=x+0$ $\displaystyle g(x)$
$\displaystyle=0+x$

Using induction it is easy to show that $f(x)=g(x)$ for all $x:\mathbb{N}$.
However, the only prove of $f=g$ would need to be canonical (since we have no
other assumptions) i.e. $\mathrm{refl}(h)$ but this would require that
$h\equiv f\equiv g$ and $f$ and $g$ are clearly not definitionally equal.

Hence in ITT while we cannot distinguish extensionally equal functions we do
not identify them either. This seems to be a rather inconvenient
incompleteness of ITT, which is overcome by HoTT. In HoTT a type doesn’t just
have elements but also it comes with an equality type that tells what is the
type of evidence that two objects are equal. In the case of the function type
this evidence is equivalent to functional extensionality. Another example is
propositional extensionality: two propositions are equal if and only if they
are logically equivalent. By incorporating these principles Type Theory is as
extensional as Set Theory but it turns out it is much better.

This is a consequence of the fact that we cannot observe the representations
of objects. What does this mean for types: what can we observe about a type?
Now we can observe the cardinality of a type — e.g. whether it has two
elements or whether it is countably infinite and so on — but nothing else.
Hence extensionally two types with the same number of elements should be
considered equal. This may appear counterintuitive on the first glance because
it entails for example that $\mathbb{Z}=\mathbb{N}$. But then can you write a
property of a type that distinguished $\mathbb{Z}$ from $\mathbb{N}$? You may
say that addition behaves differently for the two but you just have the type
and no operation on them. Indeed, if we talk about the algebraic structure,
e.g. we consider them as commutative monoids, then they are not equivalent
because we can distinguish them.

It is a consequence of the univalence principle that two isomorphic types are
equal 171717The actual statement of univalence is slightly different and uses
the notion of an _equivalence_ which refines isomorphism in a setting where
equality is not always propositional. A function $f:A\to B$ is an equivalence
if for any $b:B$ there is a unique $a:A$ and $p:f(a)=b$. Since equivalence is
reflexive there is an obvious function from equality of two types to their
equivalence. Univalence states that this function is an equivalence.  where by
isomorphic I mean that there a functions in both directions which when
composed are equal to the identity. So basically two types are equal if there
is a one-to-one correspondence between their elements. This also applies to
algebraic structures like the aforementioned commutative monoids. While the
monoids associated to $\mathbb{Z}$ and $\mathbb{N}$ are not isomorphic we
cannot distinguish different representations of the same algebraic structure,
e.g. using unary or binary numbers to represent $\mathbb{N}$. And indeed it is
a consequence of univalence that isomorphic algebraic structures are equal.

This reflects mathematical practice to view isomorphic structures as equal.
However, this is certainly not supported by Set Theory which can distinguish
isomorphic structures. Yes, indeed all structural properties are preserved but
what exactly are those? In HoTT all properties are structural, hence the
problem disappears.

There is a price to pay for this elegance. We usually expect that equality is
a proposition but this ceases to hold when we say that evidence for equality
of types is isomorphism because there is usually more than one isomorphism
between isomorphic types. 181818One can force equality to be a proposition by
truncating it. However, this means that we loose important properties such as
the ability to always replace equals by equals. The conclusion is that
equality of structures in general is not a proposition but a structure itself.

What is equality actually? I said that every type comes with a notion of
equality, with an equality type but what are the properties of equality types.
If equality were just a proposition then it would be easy: equality is just an
equivalence relation (i.e. reflexive, symmetric and transitive) and every
function has to preserve it. This view is called the setoid interpretation and
it is a useful easy case of the actual story. 191919Setoids have been used to
justify extensional principles, see [Alt99, ABKT19]. But since we have types
and we can iterate the construction of equality types, i.e. we get a whole
infinite tower of equalities, the answer is a bit more involved. The first
step up from equivalence relations are groupoids, these are categories where
every morphism corresponding to an equality type has an inverse. Or more
naively, it is the combination of an equivalence relation and a group. 202020A
one object groupoid is a group while a groupoid where every homset is
propositional is an equivalence relation. However, we need to iterate this
process any number of times arriving at weak infinity groupoids. They are
called weak because all the properties don’t hold strictly but only upto
higher equality. This is where homotopy theory comes in helpful because these
structures have been investigated and they can be defined as simplicial sets
with the Kan property or more exactly Kan fibrations for dependent types (see
[nLa22]). Actually in the context of Type Theory it turns out that cubical
sets are technically better behaved. 212121In [CCHM16] cubical sets are used
to provide a constructive explanation of the univalence axiom. This semantics
gives rise to cubical Type Theory, which is now implemented in cubical
agda.[VMA21]. Cubical Type Theory can be understood as a refinement of HoTT.

##  6 Structuralism and constructivity

We may think that the constructive nature of Type Theory which comes from the
propositions as types approach to logic is rather orthogonal to its support of
structural mathematics which stems from the fact that elementhood is treated
statically. Indeed, we can add classical principles like the unrestricted
axiom of choice (and hence excluded middle) to HoTT and still have univalence.
So are these two aspects orthogonal? Can we just have univalence but don’t
embrace constructive Mathematics?

While this is possible in principle, I would argue that there is indeed a
connection between these two aspects. Univalence forces us to revisit the
notion of equality and accept that equality isn’t always a proposition. It is
this step which at the same time renders many applications of choice
unnecessary. Choice in conventional mathematics becomes necessary because we
only talk about propositions, and hence choices need to be hidden in
propositions. When we later need to refer to the choices we have just hidden,
we need to use the axiom of choice. In Type Theory we can indeed exploit the
fact that our constructions may be types and not propositions and the choices
are explicit. 222222There is another case where HoTT can avoid the use of
choice, which comes from using Higher Inductive Types. This is used in the
definitions of the Cauchy Reals in the HoTT book, [Uni13] section 11.3, and
for example in the definition of the partiality monad. [ADK17].

A simple example for this phenomena is the way categories are treated in HoTT.
Categories are a generalisation of preorders but indeed we prefer to deal with
partial orders where the equivalence introduced by the order coincides with
equality. Can we do the same for categories? Indeed in HoTT we can introduce
the notion of a _univalent category_ 232323In the terminology of the HoTT
book, ordinary categories are called precategories and univalent categories
are called categories. , where isomorphism and equality of objects are
equivalent (i.e. isomorphic). And indeed most categories that arise from
semantic considerations – like the category of sets, or categories of
algebraic structure – are univalent. In contrast the counterpart to univalent
categories in a classical setting are _skeletal categories_ , which are very
rare and their constructions only succeeds by heavy use of the axiom of
choice.

##  7 Conclusions

Axiomatic Set Theory was developed in the 1930ies and then it constituted
considerable progress in making the foundations of mathematics precise.
However, much has happened since and it is time to reconsider the foundations
of mathematics, in particular in light of a shift of major applications of
mathematics from natural science to computer science and related disciplines.

From the viewpoint of computer science, it seems almost preposterous to think
that all mathematical concepts can be adequately represented as sets, which
correspond to a type of trees where we ignore order and multiplicity of
subtrees. This encoding seems to be not very different than the insight that
all structures in computing can be represented as a sequence of 0s and 1s.
Indeed, it seems to me that set theory is something like the machine language
of mathematics, but it doesn’t share the redeeming feature that in computing
we _need_ to translate everything to machine language. Mathematics which is a
construction of our mind doesn’t need a machine language it should rather
reflect our basic intuitions.

Set Theory enables us to ask stupid questions, like _Are the integers a subset
of the rationals?_ or _Is 2 a subset of 3_? Mathematicians tell me that they
just don’t ask these questions so they don’t really need a better language.
This reminds me, who worked as a programmer in the 1980ies, of the attitude of
some of my colleagues who didn’t see the need for high-level languages because
they knew how to do the right thing on the machine level.

The basic tenants of Type Theory are this: mathematical concepts are
represented as types, where every type comes with a static notion of
elementhood and an equality type. The main property of the equality type is
that objects are equal if they represent the same mathematical object, in
particular we view objects as equal if they satisfy the same properties – this
is just paraphrasing Leibniz. A consequence of this is that equalities aren’t
always propositions because they may be me more than one way that two objects
can be equal. Logic emerges in Type Theory, via the propositions as types
explanation, which replaces the philosophically difficult concept of truth
with the notion of evidence which can be expressed as a type.

As far as constructivity is concerned, I would like to quote Frank Pfenning
who recently said in a lecture _I have lost the ability to understand
classical logic_. I share the same problem, specifically with the boolean
explanation of logic: it seems to me that we cannot _assign_ a boolean to
every formula in arithmetic. Now I understand that _assign_ here seems to
refer to a _classical function_. However, and this may be because I am
computer scientist, it seems to me a strange abuse of the word assignment if
you have one but cannot tell me what is the output for a given input.

It seems to me that the classical approach can only succeed by an intensive
process of brain-washing, replacing naive concepts, like function, which
rather elaborate replacements. It seems that many mathematicians think that
this process is necessary for them to continue their leading edge research in
modern mathematics. That may well be so, but maybe we shouldn’t give up the
hope that there is the possibility for a more naïve form of mathematics which
favours explainability over latest fashion research.

## References

  * [ABKT19] Thorsten Altenkirch, Simon Boulier, Ambrus Kaposi, and Nicolas Tabareau.  Setoid type theory—a syntactic translation.  In International Conference on Mathematics of Program Construction, pages 155–196. Springer, 2019.
  * [ADK17] Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus.  Partiality, revisited.  In International Conference on Foundations of Software Science and Computation Structures, pages 534–549. Springer, 2017.
  * [Alt99] Thorsten Altenkirch.  Extensional equality in intensional type theory.  In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pages 412–420. IEEE, 1999.
  * [Alt19] Thorsten Altenkirch.  Naïve type theory.  In Reflections on the Foundations of Mathematics, pages 101–136. Springer, 2019.
  * [AN19] Benedikt Ahrens and Paige Randall North.  Univalent foundations and the equivalence principle.  In Reflections on the Foundations of Mathematics, pages 137–150. Springer, 2019.
  * [Awo14] Steve Awodey.  Structuralism, invariance, and univalence.  Philosophia Mathematica, 22(1):1–11, 2014.
  * [CCHM16] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg.  Cubical type theory: a constructive interpretation of the univalence axiom.  arXiv preprint arXiv:1611.02108, 2016.
  * [Cro20] Laura Crosilla.  Set Theory: Constructive and Intuitionistic ZF.  In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2020 edition, 2020.
  * [Göd33] Kurt Gödel.  Zur intuitionistischen Arithmetik und Zahlentheorie.  Ergebnisse eines mathematischen Kolloquiums, 4(1933):34–38, 1933\.
  * [Gra18] Daniel Grayson.  An introduction to univalent foundations for mathematicians.  Bulletin of the American Mathematical Society, 55(4):427–450, 2018\.
  * [Mad19] Penelope Maddy.  What do we want a foundation to do?  In Reflections on the Foundations of Mathematics, pages 293–311. Springer, 2019.
  * [ML75] Per Martin-Löf.  An intuitionistic theory of types: Predicative part.  In Studies in Logic and the Foundations of Mathematics, volume 80, pages 73–118. Elsevier, 1975.
  * [MLS84] Per Martin-Löf and Giovanni Sambin.  Intuitionistic type theory, volume 9.  Bibliopolis Naples, 1984.
  * [nLa22] nLab authors.  Kan fibration.  http://ncatlab.org/nlab/show/Kan\%20fibration, June 2022.
  * [NPS90] Bengt Nordström, Kent Petersson, and Jan M Smith.  Programming in Martin-Löf’s type theory, volume 200.  Oxford University Press Oxford, 1990.
  * [Uni13] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  * [VMA21] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel.  Cubical agda: a dependently typed programming language with univalence and higher inductive types.  Journal of Functional Programming, 31, 2021.


# Codegrees of primitive characters of solvable groups

Ping Jin, Lei Wang, Yong Yang  School of Mathematical Sciences, Shanxi
University, Taiyuan, 030006, China<EMAIL_ADDRESS><EMAIL_ADDRESS>Three Gorges Mathematical Research Center, China Three Gorges University,
Yichang, Hubei 443002, China and Department of Mathematics, Texas State
University, 601 University Drive, San Marcos, TX 78666, USA<EMAIL_ADDRESS>
###### Abstract.

We obtain the codegree of a certain primitive character for a finite solvable
group, and thereby give a negative answer to a question proposed by Moretó in
[8].

###### Key words and phrases:

codegree, primitive character, element order, solvable group

*Corresponding author

##  1\. Introduction

Let $G$ be a finite group, and write $\operatorname{Irr}(G)$ to denote the set
of irreducible complex characters of $G$. The concept of character codegree,
originally defined as $|G|/\chi(1)$ for any nonlinear irreducible character
$\chi$ of $G$, was introduced in [1] in order to characterize the structure of
finite groups. For a nonlinear character $\chi\in\mathrm{Irr}(G/N)$ where $N$
is a nontrivial normal subgroup of $G$, however, this character will have two
different codegrees when it is considered as the character of $G$ and of
$G/N$, respectively. To eliminate this inconvenience, Qian, Wang, and Wei in
[9] redefined the codegree
$\mathrm{cod}(\chi)=|G:\operatorname{Ker}\chi|/\chi(1)$ for an arbitrary
character $\chi$ of $G$. Up to now many properties of codegrees have been
studied, such as variations on Huppert’s $\rho$-$\sigma$ conjecture, the
relationship between the codegrees and the element orders, groups with few
codegrees, and recognizing simple groups using the codegree set, etc.

The authors believe that among the above-mentioned results, the most
interesting finding is the relation between the codegrees and the element
orders (see [5, 10, 11] for example). Here we mention a result of Qian ([10,
Theorem 1.1]), which says that if a finite solvable group $G$ has an element
$g$ of square-free order, then $G$ must have an irreducible character of
codegree divisible by the order $o(g)$ of $g$. In a short time, Isaacs [5]
established the same result for an arbitrary finite group. Recently Qian [11]
strengthened further his previous result, showing that for every element $g$
of a finite solvable group $G$, there exists necessarily some $\chi\in{\rm
Irr}(G)$ such that $o(g)$ divides ${\rm cod}(\chi)$.

Motivated by the results in [5, 10, 11], Moretó considered the converse
relation of codegrees and element orders and proposed an interesting question
[8, Question B]. He also mentioned that the counterexamples, if exist, seem to
be rare.

Question. Let $G$ be a finite solvable group and let
$\chi\in\operatorname{Irr}(G)$. Does there exist $g\in G$ such that
$\pi(\operatorname{cod}(\chi))\subseteq\pi(o(g))$? Here $\pi(n)$ denotes the
set of prime divisors of a positive integer $n$.

In this note we will construct examples to show that this question has a
negative answer in general. To do so, we first show that any faithful
primitive character of a finite solvable group $G$ has codegree divisible by
all prime divisors of $|G|$ (Theorem 2.2 below), and then present a sufficient
condition to guarantee that a solvable group possess a faithful primitive
character (Theorem 2.3 below). These two results, which we think, perhaps are
of independent interest.

Throughout this paper all groups considered are finite and characters are
defined over the complex field. For notation and terminology, we refer to [4].

##  2\. Codegrees of primitive characters

We begin by reviewing some facts from $\pi$-theory of characters. If $G$ is a
$\pi$-separable group, where $\pi$ is a set of primes, a character
$\chi\in\operatorname{Irr}(G)$ is said to be $\pi$-special if $\chi(1)$ is a
$\pi$-number and the determinantal order $o(\theta)$ is a $\pi$-number for
every irreducible constituent $\theta$ of the restriction $\chi_{S}$ for every
subnormal subgroup $S$ of $G$. This definition was first introduced by
Gajendragadkar in [2], and plays a prominent role in the character theory of
solvable groups. For simplicity, we say that $\chi$ is $p$-special if the set
$\pi$ consists of a single prime $p$.

######  Lemma 2.1.

Let $G$ be a solvable group and let $\chi\in\operatorname{Irr}(G)$ be a
nonlinear character.

(1) If $\chi$ is primitive, then $\chi=\prod\chi_{p}$, where each $\chi_{p}$
is $p$-special and $p$ runs over $\pi(\chi(1))$.

(2) If $\chi$ is $p$-special for a prime $p$, then $\chi_{P}$ is irreducible
for any Sylow $p$-subgroup $P$ of $G$.

###### Proof.

Part (1) is Theorem 2.17 of [6], and (2) is a special case of Theorem 2.10 of
the same reference. ∎

We can now establish the two results regarding the codegrees of primitive
characters, as mentioned in the introduction.

######  Theorem 2.2.

Let $G$ be a solvable group, and let $\chi\in\operatorname{Irr}(G)$ be a
faithful primitive character. Then $\operatorname{cod}(\chi)$ is divisible by
each prime factor of $|G|$, that is, $\pi(\operatorname{cod}(\chi))=\pi(|G|)$.

###### Proof.

If $\chi(1)=1$, then $\operatorname{cod}(\chi)=|G|$ by definition, and there
is noting to prove. So we may assume that $\chi(1)>1$. By Lemma 2.1(1), we can
write $\chi=\prod\chi_{p}$, where $p$ runs over $\pi(\chi(1))$ and $\chi_{p}$
is $p$-special. Note that $\operatorname{cod}(\chi)=|G|/\chi(1)$, and to
complete the proof, therefore, it suffices to show that
$\operatorname{cod}(\chi)$ can be divisible by every prime in $\pi(\chi(1))$.

Suppose that $p$ does not divide $\operatorname{cod}(\chi)$ for some
$p\in\pi(\chi(1))$. Then $|G|/\chi_{p}(1)$ is not divisible by $p$, so
$\chi_{p}$ has $p$-defect zero. In this case, it is well known that $\chi_{p}$
vanishes all nontrivial elements of a Sylow $p$-subgroup $P$ of $G$ (see
Theorem 8.17 of [4] for example), but then, by Lemma 2.1(2), we see that the
restriction $\chi_{P}$ is irreducible. This cannot be the case, thus proving
the theorem. ∎

######  Theorem 2.3.

Let $G$ be a solvable but non-nilpotent group, and assume that the following
conditions hold.

(1) $Z(G)$ is a cyclic group.

(2) $F(G)/Z(G)$ is a chief factor of $G$.

(3) $|F(G)|$ and $|G/F(G)|$ are relatively prime.
Then there is a faithful primitive character $\chi\in\operatorname{Irr}(G)$
such that

$\operatorname{cod}(\chi)=|G|/|F(G):Z(G)|^{\frac{1}{2}}.$

If in addition $G/F(G)$ has no element of order divisible by all prime
divisors of $|G/F(G)|$, then $\pi(\operatorname{cod}(\chi))$ is not contained
in $\pi(o(x))$ for every $x\in G$.

###### Proof.

We will complete the proof by carrying out the following steps.

_Step 1. We fix a faithful linear character $\lambda$ of $Z(G)$ and let
$\theta\in\operatorname{Irr}(F(G))$ lie over $\lambda$. Then $\theta$ is
faithful and fully ramified with respect to $F(G)/Z(G)$, so that
$\theta(1)^{2}=|F(G):Z(G)|$._

The existence of such faithful linear character $\lambda$ of $Z(G)$ is
guaranteed by Condition (1). Note that $Z(G)\leq Z(F(G))$ and
$Z(F(G))/Z(G)\vartriangleleft G/Z(G)$, so $Z(G)=Z(F(G))$ by Condition (2). For
any $\theta\in\operatorname{Irr}(F(G))$ lying over $\lambda$, since
$\theta_{Z(G)}=\theta(1)\lambda$, we see that $\operatorname{Ker}\theta\cap
Z(G)=\operatorname{Ker}\lambda=1$. But now $Z(G)$ is the center of the
nilpotent group $F(G)$, which forces $\operatorname{Ker}\theta=1$, so $\theta$
is faithful. By Theorem 2.31 of [4], it follows that $\theta$ is fully
ramified with respect to $F(G)/Z(G)$, and thus $\theta(1)^{2}=|F(G):Z(G)|$.

_Step 2. The character $\theta$ is extendible to $G$, and every extension
$\chi\in\operatorname{Irr}(G)$ of $\theta$ is primitive._

By Step 1, we know that $\theta$ is the unique irreducible character of $F(G)$
that lies over $\lambda$, so $\theta$ is necessarily $G$-invariant, and since
$F(G)$ is a normal Hall subgroup of $G$ by Condition (3), it follows that
$\theta$ is extendible to $G$ by Gallagher’s extension theorem (see Theorem
8.15 of [4]). Let $\chi\in\operatorname{Irr}(G)$ be an extension of $\theta$
and suppose that $\chi=\alpha^{G}$, where $\alpha\in\operatorname{Irr}(U)$ for
some subgroup $U$ of $G$. Write $D=F(G)\cap U$. Then $Z(G)\leq U$ (this is an
elementary fact about characters; see Problem 5.12 of [4] or Lemma 10.38 of
[6] for a proof), so $Z(G)\leq D$. Since
$(\alpha^{G})_{F(G)}=\chi_{F(G)}=\theta$, which is irreducible, we conclude
that $G=F(G)U$ and hence $D\vartriangleleft G$. Now by Condition (2), we have
two possibilities: either $D=Z(G)$ or $D=F(G)$. Assume that $D=Z(G)$. Then
$(\alpha_{Z(G)})^{F(G)}=(\alpha^{G})_{F(G)}=\theta$, which forces
$\alpha_{Z(G)}=\lambda$ and hence $\lambda^{F(G)}=\theta$. This is impossible
by Step 1, so $D=F(G)$. Now we have $U=G$, and thus $\chi$ is primitive.

_Step 3. Each extension $\chi\in\operatorname{Irr}(G)$ of $\theta$ is
faithful, and thus $\operatorname{cod}(\chi)=|G|/|F(G):Z(G)|^{\frac{1}{2}}$._

Let $K=\operatorname{Ker}\chi$. Since $\theta$ is faithful by Step 1, we see
that $K\cap F(G)=\operatorname{Ker}\theta=1$, and thus $K$ centralizes $F(G)$
and hence $F(G)/Z(G)$. But $F(G)/Z(G)=F(G/Z(G))$, which is self-centralized in
the solvable group $G/Z(G)$, so $K\leq F(G)$ and $K=1$. This proves that
$\chi$ is faithful, and by definition, we have

$\operatorname{cod}(\chi)=|G:\operatorname{Ker}\chi|/\chi(1)=|G|/\theta(1)=|G|/|F(G):Z(G)|^{\frac{1}{2}}.$

_Step 4. Complete the proof._

We have established that $G$ has a faithful primitive character $\chi$, so
Theorem 2.2 applies, and we obtain $\pi(\operatorname{cod}(\chi))=\pi(|G|)$.
Assume that $\pi(\operatorname{cod}(\chi))\subseteq\pi(o(g))$ for some element
$g\in G$. Then $\pi(o(g))=\pi(|G|)$. Consider the quotient group
$\bar{G}=G/F(G)$. It is clear that the image $\bar{g}$ of $g$ in $\bar{G}$
also has the same property that $\pi(o(\bar{g}))=\pi(|\bar{G}|)$. This shows
that the last statement of the theorem also holds, and the proof is now
complete. ∎

As an application of Theorem 2.3, we can now construct a counterexample to
Moretó’s question. For the definition and properties of semi-linear groups
$\Gamma(q^{n})$, we refer to [7].

Let $T$ be a subgroup of the semi-linear group $\Gamma(2^{10})$, where
$|\Gamma(2^{10})|=(2^{10}-1)\cdot 10$. The normal cyclic subgroup of $T$ from
the bottom $2^{10}-1$ part is of order $2^{5}+1=33=3\cdot 11$, and the Galois
group of $T$ from the top $10$ part is of order $5$, so that $|T|=3\cdot
5\cdot 11$. Since $T$ is not cyclic by a direct calculation, it follows that
$T$ has no element of order divisible by all three primes of $|T|$.

Our group $G$ is the semi-direct product $E\rtimes T$, where $E$ is an extra-
special group of order $2^{11}$ such that $T$ acts faithfully on $E$ and
irreducibly on $E/Z(E)$. We point out that the group $G$ can be realized as a
subgroup of $\operatorname{GL}(2^{5},3)$, and it has been constructed
explicitly in GAP [3]. It is easy to see that $F(G)=E$ and $G/F(G)\cong T$, so
by Theorem 2.3, we conclude that Moretó’s question can have a negative answer.

Using GAP we can calculate the codegree set of the group $G$, which is

$\\{1,3,5,11,15,33,1024,2112,5120,10560\\}.$

Of course one can construct many other examples of the same flavor.

Acknowledgement This work was supported by NSFC (Grant No. 12171289) and a
grant from the Simons Foundation (No. 499532).

## References

  * [1] D. Chillag and M. Herzog, On character degrees quotients, Arch. Math. 55 (1989), 25-29.
  * [2] D. S. Gajendragadkar, A characteristic class of characters of finite $\pi$-separable groups, J. Algebra 59 (1979), 237-259.
  * [3] The GAP Group, GAP – Groups, Algorithms, and Programming, Version 4.11.1; 2021. (https://www.gap-system.org)
  * [4] I. M. Isaacs, Character Theory of Finite Groups, Acdemic press, New York, 1976.
  * [5] I. M. Isaacs, Element orders and character codegrees, Arch. Math. 97 (2011), 499-501.
  * [6] I. M. Isaacs, Characters of Solvable Groups, RI: Amer. Math. Soc. 2018.
  * [7] O. Manz and T. R. Wolf, Representations of Solvable Groups, London Mathematical Society, Lecture Notes Series 185, Cambridge University Press, Cambridge, 1993.
  * [8] A. Moretó, Huppert’s conjecture for character codegrees, Mathematische Nachrichten, https://doi.org/10.1002/mana.202000568.
  * [9] G. Qian, Y. Wang, H. Wei, Co-degrees of irreducible characters in finite groups, J. Algebra 312 (2007), 946-955.
  * [10] G. Qian, A note on element orders and character codegrees, Arch. Math. 95 (2011),101-200.
  * [11] G. Qian, Element orders and character codegrees, Bull. Lond. Math. Soc. 53 (2021), 820-824.