
\section{Introduction: Parametricity in dependent type theory}

Broadly speaking, \emph{parametricity} statements assert that type-polymorphic
functions definable in some system must be natural in their type arguments,
in some suitable sense.
Reynolds' original theory of relational
parametricity~\cite{DBLP:conf/ifip/Reynolds83}~characterizes terms
of the polymorphically typed $\lambda$-calculus System~F.  This theory
has since been extended to richer and more expressive
type theories: to pure type systems by Bernardy,
Jansson, and Paterson~\cite{DBLP:journals/jfp/BernardyJP12}, and more
specifically to
dependent type theory by Atkey, Ghani, and Johann~\cite{DBLP:conf/popl/AtkeyGJ14}.

Most parametricity results are meta-theorems about a formal system and
make claims only about terms in the empty context.
For instance,
Reynolds' results show that the only term of System~F
with type $\forall \alpha . \alpha \to \alpha$ definable in the empty context is
the polymorphic identity function $\Lambda \alpha. \lambda (x:\alpha).x$.
Similarly, Atkey, Ghani, and Johann\ \cite[Thm.~2]{DBLP:conf/popl/AtkeyGJ14} prove that any term $f:\prod_{X : \mathcal{U}} X \to X$
definable in the empty context of MLTT
must satisfy $e(f_X(a)) =f_Y(e(a))$ for all
$e : X \to Y$ and $a:X$ in their model; it follows that
$f$ acts as the identity on every type in their model, and hence no such closed term $f$ can be provably not equal to the polymorphic identity function.

Keller and Lasson showed that excluded middle is incompatible with parametricity of the universe of types (in its usual formulation)~\cite{DBLP:conf/csl/KellerL12}.
In this paper, we show, within type theory, that certain violations of
parametricity are possible if and only if certain classical principles
hold.  For example, we show that there is a function
$f : \prod_{X : \mathcal{U}} X \to X$ whose value at the type $\mathbf{2}$ of booleans is
different from the identity if and only if excluded middle holds
(Theorem~\ref{thm:identity-bool}, where one direction uses function
extensionality).

These are theorems \emph{of} dependent type theory, so they apply not only to closed terms but in any context, and the violations of parametricity are expressed using negations of Martin-L\"of's identity type rather than judgemental (in-)equality of terms.
Similarly, we show that excluded middle also follows from certain kinds of non-trivial automorphisms of the universe.

We work throughout in intensional Martin-L\"of type theory, with at least $\Pi$-, $\Sigma$-, identity, finite, and natural numbers types, and a universe closed under these type-formers.
For concreteness, this may be taken to be the theory of \cite{martin-lof:bibliopolis}, or of \cite[A.2]{hottbook}.
When results require further axioms---e.g.\ function extensionality, or univalence of the universe---we include these as explicit assumptions, to keep results as sharp as possible.

By the \emph{law of excluded middle}, we mean always the version from univalent foundations~\cite[3.4.1]{hottbook}, namely that $P + \neg P$
for all \emph{propositions} $P$.
Here a type is called a ``proposition'' (a ``mere proposition'' in the terminology of~\cite{hottbook}) if it
has at most one element, meaning that any two of its elements are
equal in the sense of the identity type.
Note that $\neg P$ (meaning $P\to\mathbf{0}$) is not itself a proposition unless we assume function extensionality, at least for $\mathbf{0}$-valued functions.

The \emph{propositional truncation} of a type $A$ is the universal proposition $\trunc A$ admitting a map from $A$.
We axiomatize this as in \cite[\textsection 3.7]{hottbook}, and always indicate explicitly when we are assuming it.
It is shown in~\cite{keca:toappear} that propositional truncation implies function extensionality.

When propositional truncations exist, the \emph{disjunction} of two propositions $P\vee Q$ is defined to be $\trunc{P+Q}$.
If $P$ and $Q$ are disjoint (i.e.\ $\neg(P+Q)$ holds), then $P+Q$ is already a proposition and hence equivalent to $P\vee Q$.
In particular, when we have propositional truncations, the law of excluded middle could equivalently assert that $P\vee \neg P$ for all propositions $P$.

By a \emph{logical equivalence} of types $X$ and $Y$, written $X\leftrightarrow Y$, we mean two
functions $X \to Y$ and $Y \to X$ subject to no conditions at all.

By an \emph{equivalence} of types $X$ and $Y$ we mean a function $e:X\to Y$ that has both a left and a right inverse, i.e.\ functions $s,r:Y\to X$ with $e(s(y))=y$ for all $y:Y$ and $r(e(x))=x$ for all $x:X$.
This notion of equivalence is logically equivalent to having a \emph{single} two-sided inverse, which is all that we will need in this paper. But the notion of equivalence is better-behaved in univalent foundations (see~\cite[Chapter 4]{hottbook}); the reason is that the type expressing ``being an equivalence'' is a proposition, in the presence of function extensionality, whereas the type expressing ``having a two-sided inverse'' may in general have more than one inhabitant, in particular affecting the consistency of the univalence axiom.


\section{Classical axioms from non-parametricity}
\label{parametricity:section}

In this section, we give a number of ways in which classical axioms can be derived
from specific violations of parametricity.

\subsection{Polymorphic endomaps}

Say that a function $f:\prod_{X : \mathcal{U}} X \to X$ is \emph{natural under
  equivalence} if for any two types $X$ and $Y$ and any equivalence
$e:X \to Y$, we have $e(f_X(x)) = f_Y(e(x))$ for any $x:X$, where we have
written $f_X$ as a shorthand for $f(X)$ and used the equality sign $=$ to denote identity types.
\begin{theorem}
\label{thm:identity-bool}
If there is a function $f:\prod_{X : \mathcal{U}} X \to X$ such that $f_\mathbf{2}$
is not pointwise equal to the identity (i.e.\ $\neg \prod_{x:\mathbf{2}} f_\mathbf{2}(x)=x$)
and $f$ is natural under equivalence, then the law
of excluded middle holds.
Assuming function extensionality, the converse also holds.
\end{theorem}

\begin{proof}
  First we derive excluded middle from~$f$.
  To begin, note that if
  \arxivonly{\linebreak[4]}
  $\neg \prod_{x:\mathbf{2}} f_\mathbf{2}(x)=x$, then we cannot have both $f_\mathbf{2}({\operatorname{t\!t}})={\operatorname{t\!t}}$ and $f_\mathbf{2}({\operatorname{f\!f}})={\operatorname{f\!f}}$, since then we could prove $\prod_{x:\mathbf{2}} f_\mathbf{2}(x)=x$ by case analysis on $x$.
  But then by case analysis on $f_\mathbf{2}({\operatorname{t\!t}})$ and $f_\mathbf{2}({\operatorname{f\!f}})$, we must have $(f_\mathbf{2}({\operatorname{t\!t}})={\operatorname{f\!f}})+(f_\mathbf{2}({\operatorname{f\!f}})={\operatorname{t\!t}})$.
  Without loss of generality, suppose $f_\mathbf{2}({\operatorname{t\!t}})={\operatorname{f\!f}}$.

  Now let $P$ be an arbitrary
  proposition. We do case analysis on
  $f_{P+\mathbf{1}}({\operatorname{inr}}(\star)) : P+\mathbf{1}$.
  \begin{enumerate}
  \item If it is of the form ${\operatorname{inl}}(p)$ with $p:P$, we conclude
    immediately that $P$ holds.
  \item If it is of the form ${\operatorname{inr}}(\star)$, then $P$ cannot hold, for if
    we had $p:P$, then the map $e : \mathbf{2} \to P + \mathbf{1}$ defined by $e({\operatorname{f\!f}})={\operatorname{inl}}(p)$ and $e({\operatorname{t\!t}})={\operatorname{inr}}(\star)$ would be an equivalence, and hence $e(f_\mathbf{2}(x)) = f_{P+\mathbf{1}}(e(x))$ for all $x:\mathbf{2}$ and so
  $ {\operatorname{inl}}(p) = e({\operatorname{f\!f}}) = e (f_\mathbf{2}({\operatorname{t\!t}})) = f_{P+\mathbf{1}} (e({\operatorname{t\!t}})) = f_{P+\mathbf{1}} ({\operatorname{inr}}(\star)) = {\operatorname{inr}}(\star)$, which is a contradiction.
  \end{enumerate}
Therefore $P$ or not $P$.

For the converse, \cite[Exercise~6.9]{hottbook}, suppose
excluded middle holds, let $X:\mathcal{U}$ and $x:X$, and consider the type
$\sum_{x':X} (x'\neq x)$, where $a\neq b$ means $\neg(a=b)$.  By excluded middle, this is either
contractible or not.  (A type $Y$ is \emph{contractible} if
$\sum_{y:Y} \prod_{y':Y} (y=y')$.  Assuming
function extensionality, this is a proposition.) If it is contractible, define $f_X(x)$ to
be the center of contraction (the point $y$ in the definition of
contractibility); otherwise define $f_X(x)=x$.
\end{proof}

\begin{remark} \leavevmode
  \begin{enumerate}
  \item If we assume univalence, any $f:\prod_{X : \mathcal{U}} X \to X$ is automatically
    natural under equivalence, so that assumption can be dispensed with.
    And, of course, if function extensionality holds (which follows
    from univalence) then the hypothesis $\neg \prod_{x:\mathbf{2}} f_\mathbf{2}(x)=x$
    is equivalent to $f_\mathbf{2} \neq \lambda (x:\mathbf{2}). x$.
  \item We do not know whether the converse direction of
    Theorem~\ref{thm:identity-bool} is provable without function
    extensionality.
  \end{enumerate}
\end{remark}

The preceding proof can be generalized as follows.
We say that a point $x:X$ is \emph{isolated} if
the type $x=y$ is decidable for all $y:Y$, i.e.\ if we have $\prod_{y:X} (x=y)+(x\neq y)$.

\begin{lemma}\label{lem:isolated}
  A point $x:X$ is isolated if and only if $X$ is equivalent to
  $Y+\mathbf{1}$, for some type~$Y$, by a map that sends $x$ to
  ${\operatorname{inr}}(\star)$.
\end{lemma}
\begin{proof}
  Since ${\operatorname{inr}}(\star)$ is isolated, such an equivalence certainly
  implies that $x$ is isolated.  Conversely, from
  $\prod_{y:X} (x=y)+(x\neq y)$ we can construct a function
  $d:X\to\mathbf{2}$ such that $d(y)={\operatorname{t\!t}}$ if and only if $x=y$ and $d(y)={\operatorname{f\!f}}$, and if and only if
  $x\neq y$.  Let $Y$ be $\sum_{y:X} (d(y)={\operatorname{f\!f}})$; it is straightforward
  to show $X\equiv Y+\mathbf{1}$.

  If we had function extensionality (for $\mathbf{0}$-valued functions),
  we could dispense with $d$ and define $Y = \sum_{y:X} (x\neq y)$,
  since then $x\neq y$ would be a proposition.  In general we use
  $d(y)={\operatorname{f\!f}}$ as it is always a proposition (since $\mathbf{2}$ has
  decidable equality, hence its identity types are propositions by
  Hedberg's theorem); this is necessary to show that the composite
  $Y+\mathbf{1} \to X \to Y+\mathbf{1}$ acts as the identity on $Y$.
\end{proof}

\begin{theorem}
\label{thm:identity-isolated}
  If there is a function $f:\prod_{X : \mathcal{U}} X \to X$ such that
  $f_X(x)\neq x$ for some isolated point $x:X$ and $f$ is natural
  under equivalence, then the law of excluded middle holds.
  Assuming function extensionality, the converse also holds.
\end{theorem}

\begin{proof}
  To derive excluded middle from~$f$, let $Y$ and $X\equiv Y+\mathbf{1}$ be as in Lemma~\ref{lem:isolated}, and let $P$ be an arbitrary
  proposition. We do case analysis on
  $f_{P\times Y + \mathbf{1}}({\operatorname{inr}}(\star)) : P \times Y + \mathbf{1}$.
  \begin{enumerate}
  \item If it is of the form ${\operatorname{inl}}((p,y))$ with $p:P$, we conclude
    immediately that $P$ holds.
  \item If it is of the form ${\operatorname{inr}}(\star)$, then $P$ cannot hold, for
    if we had $p:P$, then the map $e : X \to P\times Y + \mathbf{1}$
    defined by $e(x)={\operatorname{inr}}(\star)$ (where $x$ is the isolated point) and
    $e(y)={\operatorname{inl}}((p,y))$ for $y \neq x$ would be an equivalence, and
    hence $e(f_X(x)) = f_{P\times Y+\mathbf{1}}(e(x))$, and so
    $ {\operatorname{inl}}((p,f_X(x))) = e (f_X(x)) = f_{P\times Y+\mathbf{1}} (e(x)) =
    f_{P\times Y+\mathbf{1}} ({\operatorname{inr}}(\star)) ={\operatorname{inr}}(\star)$, which is a contradiction.
  \end{enumerate}
Therefore either $P$ or not $P$ holds.
The converse is proven exactly as in Theorem~\ref{thm:identity-bool}.
\end{proof}

Finally, if our type theory includes propositional truncations, we can dispense with
isolatedness.

\begin{theorem}
\label{thm:identity-proptrunc}
  In a type theory with propositional truncations, there is an
  \arxivonly{\linebreak[4]}
  equivalence-natural function $f : \prod_{X:\mathcal{U}} X\to X$ and a type
  $X : \mathcal{U}$ with a point $x:X$ such that $f_X(x)\neq x$ if and only if excluded middle holds.
\end{theorem}
\begin{proof}
  For the ``if'' direction, note that propositional truncation
  implies function extensionality~\cite{keca:toappear}, so the converse direction of
  Theorem~\ref{thm:identity-bool} applies.  For the ``only if'' direction,
  assume that we are given $f : \prod_{X:\mathcal{U}} X\to X$, a type $X:\mathcal{U}$
  and a point $x:X$ with $f_X(x) \ne x$. Let $P$ be any proposition,
  and define
\begin{gather*}
Z  = \sum_{y:X} \trunc{x=y} \vee P, \qquad
z =  (x,|{\operatorname{inl}}(|\operatorname{refl}_x|)|) : Z, \qquad
y =  \operatorname{pr}_1(f_Z(z)) : X.
\end{gather*}
Recall that $A\vee B$ denotes the truncated disjunction $\trunc{A+B}$.
This binds more tightly than $\Sigma$, so $Z = \sum_{y:X} (\trunc{x=y} \vee P)$.
We write $|a|:\trunc{A}$ for the witness induced by a point $a:A$.

Now the second projection $\operatorname{pr}_2(f_Z(z))$ tells us that
$\trunc{x=y} \vee P$.  However, if $P$ holds, then $\operatorname{pr}_1:Z \to X$ is an
equivalence that maps $z$ to $x$. Thus $f_Z(z) \neq z$ and
hence $x\neq y$.
In other words, $P\to (x\neq y)$, hence $(x=y) \to \neg P$ and so also $\trunc{x=y}\to \neg P$.
But since $\trunc{x=y} \vee P$, we have $\neg P \vee P$, which (in the presence of function extensionality) is equivalent to excluded middle.
\end{proof}

\begin{remark}\leavevmode
  \begin{enumerate}
  \item If $x:X$ happens to be isolated, then the type $Z$ defined in
    the proof of Theorem~\ref{thm:identity-proptrunc} is equivalent to
    the type $P\times Y+\mathbf{1}$ used in the proof of
    Theorem~\ref{thm:identity-isolated}.
  \item Since propositional truncation implies function extensionality~\cite{keca:toappear},
    it makes excluded middle into a proposition.  Thus, the existence hypothesis of
    Theorem~\ref{thm:identity-proptrunc} can be truncated or untruncated without change of meaning.
  \item  The hypothesis can also be formulated as
    ``there is a type $X$ such that $f_X$ is apart from the
    identity of $X$'', where two functions $g,h:A \to B$ of types $A$
    and $B$ are \emph{apart} if there is $a:A$ with $g(a) \ne
    h(a)$. We don't know whether it is possible to derive
    excluded middle from the weaker assumption that $f_X$ is simply
    \emph{unequal} to the identity function of $X$, or even that $f$
    is unequal to the polymorphic identity function.
  \end{enumerate}
\end{remark}

The above can be applied to obtain classical axioms from
other kinds of violations of parametricity.  As a simple example,
consider $f:\prod_{X : \mathcal{U}} (X \to X) \to (X \to X)$.  Parametric
elements of this type are Church numerals.
Given $f$, we can define a polymorphic endomap
$g:\prod_{X : \mathcal{U}} X \to X$ by $g_X=f_X(\idfunc[X])$, where
$\idfunc[X]$ is the identity function.  If $f$ is natural under
equivalence, then so is $g$, and hence the assumption that
$f_\mathbf{2}(\idfunc[\mathbf{2}])$ is \emph{not} the identity function gives
excluded middle, assuming function extensionality.

\subsection{Maps of the universe into the booleans}
\label{sec:u-to-bool}

A function $f : \mathcal{U} \to \mathbf{2}$ is \emph{invariant under equivalence}, or
\emph{extensional}, if we have $f(X)=f(Y)$ for any two equivalent types $X$
and~$Y$. We say that it is \emph{strongly non-constant} if we have
$X,Y:\mathcal{U}$ with $f(X) \neq f(Y)$.
Assuming function extensionality, Escard{\'o} and
Streicher~\cite[Thm.~2.2]{DBLP:journals/apal/EscardoS16} showed that if $f : \mathcal{U} \to
\mathbf{2}$ is extensional and strongly non-constant, then the weak limited
principle of omniscience holds (any function $\mathbb{N} \to \mathbf{2}$ is
constant or not).  Alex Simpson strengthened this as follows (also reported
in~\cite[Thm.~2.8]{DBLP:journals/apal/EscardoS16}):

\begin{theorem}[Simpson]\label{thm:simpson}
Assuming function extensionality for $\mathbf{0}$-valued functions,
there is an extensional, strongly non-constant function $f:\mathcal{U} \to
\mathbf{2}$ if and only if weak excluded middle holds (meaning that
$\neg A + \neg\neg A$ for all $A : \mathcal{U}$).
\end{theorem}
\begin{proof}
  In one direction, suppose weak excluded middle, and define $f:\mathcal{U} \to
  \mathbf{2}$ by $f(A)={\operatorname{f\!f}}$ if $\neg A$ and $f(A)={\operatorname{t\!t}}$ if $\neg\neg A$.
  Then $f(\mathbf{0})={\operatorname{f\!f}}$ and $f(\mathbf{1})={\operatorname{t\!t}}$, so $f$ is strongly
  non-constant.  Extensionality follows from the observation that if
  $A\equiv B$ then $\neg A \leftrightarrow \neg B$ and
  $\neg \neg A \leftrightarrow \neg \neg B$.

  In the other direction, suppose $f:\mathcal{U} \to \mathbf{2}$ is extensional,
  and strongly non-constant witnessed by types $X,Y:\mathcal{U}$ with
  $f(X) \neq f(Y)$.  Suppose without loss of generality that
  $f(X)={\operatorname{t\!t}}$ and $f(Y)={\operatorname{f\!f}}$.  For any $A:\mathcal{U}$, define
  $Z = \neg A \times X + \neg\neg A \times Y$.  If $A$, then
  $\neg A\equiv\mathbf{0}$ and $\neg\neg A \equiv \mathbf{1}$
  (using function extensionality), so $Z\equiv Y$
  and $f(Z)={\operatorname{f\!f}}$.  Similarly, if $\neg A$, then $Z\equiv X$ and so
  $f(Z)={\operatorname{t\!t}}$.  On the other hand, $f(Z)$ must be either ${\operatorname{t\!t}}$ or
  ${\operatorname{f\!f}}$ and not both.  If it is ${\operatorname{t\!t}}$, then it is not ${\operatorname{f\!f}}$,
  and so $\neg A$; while if it is ${\operatorname{f\!f}}$, then it is not ${\operatorname{t\!t}}$,
  and so $\neg\neg A$.
\end{proof}

In
Theorem~\ref{polymorphic:into:booleans} below we reuse Simpson's
argument to establish a similar conclusion for polymorphic functions
into the booleans.

\subsection{Polymorphic maps into the booleans}
\label{sec:ptd-u-to-bool}

A function $f:\prod_{X : \mathcal{U}} X \to \mathbf{2}$ is \emph{invariant under
equivalence} if we have $f_Y(e(x)) = f_X(x)$ for any equivalence
$e:X\to Y$ and point $x:X$.
Such a function ``violates parametricity'' if it is non-constant.
Equivalence invariance means that some such violations are literally impossible: for instance, there cannot be a type $X$ with points $x,y:X$ such that $f_X(x) \neq f_X(y)$ if there is an automorphism of $X$ that maps $x$ to $y$.

A violation of constancy \emph{across} types, rather than at a
specific type, is equivalent to weak excluded middle.
\begin{theorem} \label{polymorphic:into:booleans}
  Assuming function extensionality for $\mathbf{0}$-valued functions,
  weak excluded middle holds if and only if there is an
  $f:\prod_{X:\mathcal{U}} X \to \mathbf{2}$ that is invariant under equivalence,
  together with $X,Y:\mathcal{U}$ with isolated points $x:X$ and $y:Y$ such
  that $f_X(x) \neq f_Y(y)$.
\end{theorem}
\begin{proof}
  Assuming weak excluded middle, to show the existence of such an $f$,
  let $X:\mathcal{U}$ and $x:X$.
  Then use weak excluded middle to decide $\neg(\sum_{x':X}x\neq
  x')+\neg\neg(\sum_{x':X}x\neq x')$.
  In the left case, expressing that there are no other elements in $X$
  than $x$, define $f_X(x)={\operatorname{f\!f}}$, and in the right case define
  $f_X(x)={\operatorname{t\!t}}$.
  So, for example, $f_\mathbf{1}(\star)={\operatorname{f\!f}}$ and $f_\mathbf{2}({\operatorname{t\!t}})={\operatorname{t\!t}}$,
  showing that we constructed a non-constant $f$ as required.

  For the other direction, without loss of generality, $f_X(x)={\operatorname{t\!t}}$
  and $f_Y(y)={\operatorname{f\!f}}$.
  By assumption, $X$ is equivalent to $\mathbf{1}+X'$ via an equivalence that sends $x$ to
  ${\operatorname{inl}}(\star)$, and similarly $Y$ is equivalent to $\mathbf{1}+Y'$ via an
  equivalence that sends $y$ to ${\operatorname{inl}}(\star)$.
  Let $A:\mathcal{U}$ and define
  \begin{eqnarray*}
    Z & = & (\mathbf{1} + \neg A \times X') \times (\mathbf{1} + \neg\neg A
            \times Y'), \\
    z & = & ({\operatorname{inl}}(\star),{\operatorname{inl}}(\star)).
  \end{eqnarray*}
  By the invariance under equivalence of $f$,
  \begin{enumerate}
  \item if $\neg A$ then $Z\equiv X$ via an equivalence
    that sends $z$ to $x$, thus $f_Z(z)={\operatorname{t\!t}}$,
  \item if $A$ then $Z\equiv Y$ via an equivalence that sends $z$ to
    $y$, thus $f_Z(z)={\operatorname{f\!f}}$.
  \end{enumerate}
  The contrapositives of these two implications are respectively
  \begin{eqnarray*}
    f_Z(z)={\operatorname{f\!f}} & \to & \neg\neg A,\\
    f_Z(z)={\operatorname{t\!t}} & \to & \neg A.
  \end{eqnarray*}
  Hence we can decide $\neg A$ by case analysis on the value of $f_Z(z)$.
\end{proof}

Provided our type theory includes propositional truncations, we can
dispense with isolatedness as in Theorem~\ref{thm:identity-proptrunc},
assuming the types $x=x$ and $y=y$ are propositions.
\begin{theorem}\label{thm:ptd-u-to-bool}
  In a type theory with propositional truncations, weak excluded
  middle holds if and only if there is an
  $f:\prod_{X:\mathcal{U}} X \to \mathbf{2}$ that is invariant under equivalence,
  together with $X,Y:\mathcal{U}$ with $x:X$ and $y:Y$ such that
  $f_X(x) \neq f_Y(y)$, where the types $x=x$ and $y=y$ are
  propositions.
\end{theorem}
\begin{proof}
  Assuming weak excluded middle, the existence of such an $f$ is shown
  as in the proof of Theorem~\ref{polymorphic:into:booleans}.

  For the other direction, without loss of generality, $f_X(x)={\operatorname{t\!t}}$
  and $f_Y(y)={\operatorname{f\!f}}$.
  Note that since $x=x$ and $y=y$ are propositions, so are $x=x'$ and $y=y'$ for any $x':X$ and $y':Y$, since as soon as they have a point they are equivalent to $x=x$ and $y=y$ respectively.
  Let $A:\mathcal{U}$ and define
  \begin{eqnarray*}
    Z & = & \left(\sum_{x':X}\bracket{x=x'}\vee\neg A\right) \times
            \left(\sum_{y':Y}\bracket{y=y'}\vee\neg\neg A\right), \\
    z & = & ((x,|{\operatorname{inl}}(\operatorname{refl})|),(y,|{\operatorname{inl}}(\operatorname{refl})|)).
  \end{eqnarray*}
  By invariance under equivalence of $f$, we have the following.
  \begin{enumerate}
  \item If $\neg A$ then $Z\equiv X$ via an equivalence that sends $z$
    to $x$, thus $f_Z(z)={\operatorname{t\!t}}$.  This works because the left factor
    of $Z$ becomes equivalent to $X$, and the right factor equivalent
    to $\mathbf{1}$ by the assumptions that $y=y$ is a proposition and
    $\neg A$.
  \item Similarly, if $A$ then $Z\equiv Y$ via an equivalence that
    sends $z$ to $y$, thus $f_Z(z)={\operatorname{f\!f}}$, now using the fact that
    $x=x$ is a proposition.
  \end{enumerate}
  The contrapositives of these two implications are respectively
  \begin{eqnarray*}
    f_Z(z)={\operatorname{f\!f}} & \to & \neg\neg A, \\
    f_Z(z)={\operatorname{t\!t}} & \to & \neg A.
  \end{eqnarray*}
  Hence we can decide $\neg A$ by case analysis on the value of $f_Z(z)$.
\end{proof}

\begin{remark}
  In a type theory with pushouts, the assumptions that $x=x$ and $y=y$
  are propositions can be removed by using the join $(x=x') * \neg A$
  instead of the disjunction $\bracket{x=x'}\vee \neg A$ in the left
  factor of $Z$, and similarly for the right factor of $Z$.  (The
  \emph{join} $B*C$ of types $B$ and $C$ is the pushout of $B$ and $C$
  under $B\times C$.)  This works since joining with an empty type is
  the identity, while joining with a contractible type gives a
  contractible result; see Theorem~\ref{thm:ptd-decomp} below for
  details.
  Indeed, the join of two propositions is their disjunction, by~\cite[Lemma 2.4]{rijke:join}; but the version using joins does not quite subsume the one using disjunctions, since if joins are not already assumed to exist, we do not know how to show that the disjunction of two propositions is their join.
\end{remark}

\subsection{Decompositions of the universe}
\label{sec:decomp}

Theorem~\ref{thm:simpson} can be
interpreted as saying that the universe $\mathcal{U}$ cannot be decomposed
into two disjoint inhabited parts without weak excluded middle.  In
fact, disjointness of the parts is not necessary.  All that is needed
is that both parts be proper, i.e.\ not the whole of $\mathcal{U}$:

\begin{theorem}
  In a type theory with propositional truncation and function
  extensionality for $\mathbf{0}$-valued functions, suppose we have
  equivalence-invariant $P,Q:\mathcal{U}\to\mathcal{U}$ such that for all $Z:\mathcal{U}$ we
  have $P(Z) \vee Q(Z)$, and that we have types $X$ and $Y$ such that
  $\neg P(X)$ and $\neg Q(Y)$.  Then weak excluded middle holds.
\end{theorem}
\begin{proof}
  For any $A:\mathcal{U}$, let $Z = \neg A \times X + \neg\neg A \times Y$ as
  in Simpson's proof.  If $A$, then $Z\equiv Y$, and so $\neg Q(Z)$;
  thus $Q(Z) \to \neg A$.  But if $\neg A$, then $Z\equiv X$, and so
  $\neg P(Z)$; thus $P(Z) \to \neg\neg A$.  Hence the assumed $P(Z)
  \vee Q(Z)$ implies $\neg A \vee \neg \neg A$, which is equivalent to
  $\neg A + \neg\neg A$ since $\neg A$ and $\neg\neg A$ are (by
  function extensionality) disjoint propositions.
\end{proof}

The proof of Theorem~\ref{thm:ptd-u-to-bool} can be similarly adapted.

\begin{theorem}\label{thm:ptd-decomp}
  In a type theory with propositional truncation and $\mathbf{0}$-valued
  function extensionality, suppose we have $P,Q:\prod_{X:\mathcal{U}} X \to
  \mathcal{U}$ that are invariant under equivalence, i.e.\ if $X\equiv Y$ by an
  equivalence sending $x:X$ to $y:Y$, then $P_X(x) \equiv P_Y(y)$, and
  likewise for $Q$.  Suppose also that for all $Z:\mathcal{U}$ and $z:Z$ we
  have $P_Z(z) \vee Q_Z(z)$, and types $X,Y$ with points $x:X$ and
  $y:Y$ such that $\neg P_X(x)$ and $\neg Q_Y(y)$.  Finally, suppose
  either that our type theory has pushouts or that the types $x=x$ and
  $y=y$ are propositions.  Then weak excluded middle holds.
\end{theorem}
\begin{proof}
  For variety in contrast to Theorem~\ref{thm:ptd-u-to-bool},
  suppose we have pushouts; we leave the other case to the reader.
  Let $A:\mathcal{U}$ and define
  \begin{eqnarray*}
    Z & = & \left(\sum_{x':X} (x=x') * \neg A\right) \times
            \left(\sum_{y':Y} (y=y')* \neg\neg A\right), \\
    z & = & ((x,{\operatorname{inl}}(\operatorname{refl})),(y,{\operatorname{inl}}(\operatorname{refl}))).
  \end{eqnarray*}
  Then if $A$, $\neg A\equiv \mathbf{0}$, so $(x=x')*\neg A \equiv (x=x')$,
  and thus the first factor of $Z$ is equivalent to $\sum_{x':X}
  (x=x')$, which is a ``singleton'' or ``based path space'' and hence
  equivalent to $\mathbf{1}$.  On the other hand (still assuming $A$),
  $\neg\neg A\equiv \mathbf{1}$, so $(y=y')*\neg\neg A \equiv \mathbf{1}$, and
  thus the right factor of $Z$ is equivalent to $\sum_{y':Y}\mathbf{1}$ and
  hence to $Y$.  Thus, $A$ implies $Z\equiv Y$, and it is easy to check
  that this equivalence sends $z$ to $y$.  Hence $A \to \neg Q_Z(z)$,
  and so $Q_Z(z) \to \neg A$.  A dual argument shows that $\neg A \to
  \neg P_Z(z)$ and thus $P_Z(z) \to \neg\neg A$, so the assumption
  $P_Z(z) \vee Q_Z(z)$ gives weak excluded middle.
\end{proof}

Since a function $\prod_{X:\mathcal{U}} X \to B$, for any fixed $B$, is the
same as a function $\left(\sum_{X:\mathcal{U}} X\right) \to B$, we can
interpret Theorem~\ref{thm:ptd-decomp} as saying that the universe $\sum_{X : \mathcal{U}} X$ of
\emph{pointed types} also cannot be decomposed into two proper parts
without weak excluded middle.

The results discussed so far illustrate that different violations of
parametricity have different proof-theoretic strength: some violations
are impossible, while others imply varying amounts of excluded middle.

\section{Classical axioms from automorphisms of the universe}
\label{classical:automorphisms}

There have been attempts to apply parametricity to show that the only
automorphism of a universe of types is the identity.  Nicolai Kraus
observed in the HoTT mailing list~\cite{automorphisms:kraus} that,
assuming univalence, automorphisms of a universe $\mathcal{U}$ living in a
universe $\mathcal{V}$ correspond to elements of the loop space%
\footnote{The \emph{loop space} $\Omega(X,x)$ of a type $X$ at a point $x:X$ is the identity type $x=x$; see~\cite[\textsection 2.1]{hottbook}.}
$\Omega(\mathcal{V},\mathcal{U})$, while elements of the higher loop space $\Omega^2(\mathcal{V},\mathcal{U})$
correspond to ``polymorphic automorphisms'' $\prod_{X:\mathcal{U}} X\equiv X$, which are at least as strong as polymorphic endomaps.
In particular, nontrivial elements of $\Omega^2(\mathcal{V},\mathcal{U})$ imply violations of
parametricity for $\prod_{X : \mathcal{U}} X \to X$.  This suggests that
parametricity may play a role in automorphisms of the universe.

We are not aware of a proof that parametricity implies that the only
automorphism of the universe is the identity. However, in the spirit
of the above development, we can show that automorphisms with specific
properties imply excluded middle.  First, however, we observe that if we do have excluded middle then we can construct various nontrivial automorphisms of the universe.

\subsection{Automorphisms from excluded middle}
\label{sec:autom-that-do}

The simplest automorphism of the universe is defined as follows.
By \emph{propositional extensionality} we mean that any two logically equivalent propositions are equal.
(This follows from propositional univalence, i.e.\ univalence asserted only for propositions.
The converse holds at least assuming function extensionality; we do not know whether this assumption is necessary.)

\begin{theorem}\label{thm:swap10}
  Assuming excluded middle, function extensionality, and propositional extensionality, there is an automorphism $f:\mathcal{U}\equiv \mathcal{U}$ such that $f(\mathbf{1})\equiv\mathbf{0}$.
\end{theorem}
\begin{proof}
Given a type
$X$, we use excluded middle to decide if it is a proposition (this works because under function extensionality, being a proposition is itself a proposition).  If it
is, we define $f(X)=\neg X$, and otherwise we define $f(X)=X$.
Assuming propositional extensionality and excluded middle,
we have $\neg\neg X = X$ for any proposition; thus $f(f(X))=X$ whether $X$ is a proposition or not, and hence $f$ is a self-inverse equivalence.
\end{proof}


We can try to construct other automorphisms of the universe by permuting some other subclass of types.
For instance, if we have propositional truncation, then given any two non-equivalent types $A$ and $B$, excluded middle implies that for any type $X$ we have $\trunc{X=A} + \trunc{X=B} + (X\neq A \wedge X\neq B)$, so that the universe $\mathcal{U}$ decomposes as a sum $\mathcal{U}_A + \mathcal{U}_B + \mathcal{U}_{\neq A,B}$, where
\begin{gather*}
  \mathcal{U}_A = \sum_{X:\mathcal{U}} \trunc{X=A}, \qquad
  \mathcal{U}_B = \sum_{X:\mathcal{U}} \trunc{X=B}, \qquad
  \mathcal{U}_{\neq(A,B)} = \sum_{X:\mathcal{U}} (X\neq A \wedge X\neq B).
\end{gather*}
(This requires function extensionality for $X\neq A$ and $X\neq B$ to be propositions, but not univalence.)
Thus, if $\mathcal{U}_A \equiv \mathcal{U}_B$ we can switch those two summands to produce an automorphism of $\mathcal{U}$:

\begin{theorem}\label{thm:uuequiv-aut}
  Assuming function extensionality and excluded middle, if $A\not\equiv B$ and $\mathcal{U}_A \equiv \mathcal{U}_B$, then there is an automorphism $f:\mathcal{U}\equiv \mathcal{U}$ such that $\trunc{f(A)=B}$, hence $f\neq\operatorname{id}$.
\end{theorem}
\begin{proof}
  We use the above decomposition and the given equivalence $\mathcal{U}_A \equiv \mathcal{U}_B$ to produce $f$.
  And since $f$ maps $\mathcal{U}_A$ to $\mathcal{U}_B$, by definition of $\mathcal{U}_B$ we have $\trunc{f(A)=B}$.
\end{proof}

This leads to the question, when can we have $\mathcal{U}_A \equiv \mathcal{U}_B$ but $A \not\equiv B$?
Theorem~\ref{thm:swap10} is the simplest example of this: assuming propositional extensionality, both $\mathcal{U}_{\mathbf{0}}$ and $\mathcal{U}_{\mathbf{1}}$ are contractible, hence equivalent to $\mathbf{1}$.
More generally, let us call a type $X$ \emph{rigid} if $\mathcal{U}_X$ is contractible; then we have:

\begin{theorem}
  Assuming function extensionality and excluded middle, if $A$ and $B$ are rigid types with $A\not\equiv B$, then there is an automorphism $f:\mathcal{U}\equiv \mathcal{U}$ such that $f(A)\equiv B$.
\end{theorem}
\begin{proof}
  This follows from Theorem \ref{thm:uuequiv-aut}.
  In the rigid case we get the stronger conclusion that $f(A)\equiv B$, since $\mathcal{U}_B$ is contractible.
\end{proof}

More generally, under excluded middle any permutation of the rigid types yields an automorphism of the universe.

If we assume UIP, then \emph{every} type is rigid, so that with UIP and excluded middle there are plenty of automorphisms of the universe.
If we instead assume univalence --- as we will do for the rest of this subsection --- most types are not rigid.
For instance, any type with two distinct isolated points, such as $\mathbb{N}$, is not rigid, since we can swap the isolated points to give a nontrivial automorphism and hence a nontrivial equality in $\mathcal{U}_X$.
In particular, if excluded middle holds and $X$ is a \emph{set} (i.e.\ its identity types are all propositions), then all points of $X$ are isolated.
Thus, with excluded middle and univalence, no set with more than one element (i.e.\ with points $x,y:X$ such that $x\neq y$) is rigid.

However, there exist types that are \emph{connected} (i.e.\ $\trunc{X}$ and  $\prod_{x,y:X} \trunc{x=y}$), but that are not trivial; indeed, as remarked above, $\mathcal{U}_A$ is such a type.
Moreover, if we also assume higher inductive types, then from any group $G$ that is a set we can construct a connected type $BG$ such that $\Omega(BG) \equiv G$ \cite[\textsection 3.2]{lf:emspaces}.

This leads us to ask, when is $BG$ rigid for a set-group $G$?
Since $BG$ is a 1-type (i.e.\ its identity types are all sets), $\mathcal{U}_{BG}$ is a 2-type (i.e.\ its identity types are all 1-types).
Hence it is contractible as soon as its loop space is connected and its double loop space is contractible.
In general, the connected components of $\Omega(\mathcal{U}_{BG})$ are the \emph{outer automorphisms} of $G$ (equivalence classes of automorphisms of $G$ modulo conjugation), while $\Omega^2(\mathcal{U}_{BG})$ is the \emph{center} of $G$ (the subgroup of elements that commute with everything).
A group with trivial outer automorphism group and trivial center is sometimes known as a \emph{complete} group (though there is no apparent relation to any topological notion of completeness), and there are plenty of examples.

For instance, the symmetric group $S_n$ is complete in this sense except when $n=2$ or $6$.
Thus, $BS_n$ is rigid for $n\notin \{2,6\}$.
(Note also that $BS_n$ can be constructed without higher inductive types --- but with univalence --- as $\mathcal{U}_{[n]}$, where $[n]$ is a finite $n$-element type, although of course this type only lives in a larger universe $\mathcal{V}$.)
In particular, assuming univalence and excluded middle, there are countably infinitely many rigid types, and hence \emph{uncountably} many nontrivial automorphisms of $\mathcal{U}$ (one induced by every permutation of the types $BS_n$ for $n\notin \{2,6\}$).

This does not exhaust the potential automorphisms of $\mathcal{U}$.
For instance, we have:

\begin{theorem}\label{thm:swap-rigid-prod}
  Let $X$ be an $n$-type for some $n\ge -1$, and let $A$ and $B$ be $n$-connected rigid types such that $X\times A \not\equiv X\times B$.
  Then assuming univalence and excluded middle, there is an automorphism $f:\mathcal{U}\equiv\mathcal{U}$ such that $\trunc{f(X\times A) = (X\times B)}$.
\end{theorem}
\begin{proof}
  We will show that $\mathcal{U}_{X\times A} \simeq \mathcal{U}_{X\times B}$, by showing that both are equivalent to $\mathcal{U}_X$.
  It suffices to consider $A$.
  We have $(Z\mapsto Z\times A) : \mathcal{U}_X \to \mathcal{U}_{X\times A}$, and since both types are connected it suffices to show that it induces an equivalence of loop spaces $\Omega\mathcal{U}_X \to \Omega\mathcal{U}_{X\times A}$, or equivalently that the induced map $L:(X\equiv X) \to (X\times A \equiv X\times A)$ is an equivalence.
  Since $A$ is $n$-connected for $n\ge -1$, we have $\trunc A$; so since being an equivalence is a proposition we may assume given $a_0:A$.

  We claim that for all $a:A$, $x:X$, and $f:X\times A \to X\times A$ we have
  \begin{equation}
    \operatorname{pr}_1(f(x,a)) = \operatorname{pr}_1(f(x,a_0)).\label{eq:rigid-prod-star}
  \end{equation}
  Since this goal is an equality in the $n$-type $X$, it is an $(n-1)$-type.
  And since $A$ is $n$-connected, the map $a_0:\mathbf{1}\to A$ is $(n-1)$-connected by~\cite[Lemma 7.5.11]{hottbook}.
  Thus, by~\cite[Lemma 7.5.7]{hottbook}, it suffices to assume that $a=a_0$, in which case~\eqref{eq:rigid-prod-star} is clear.

  It follows from~\eqref{eq:rigid-prod-star} that if we define $M:(X\times A \to X\times A)\to (X\to X)$ by $M(f)(x) = \operatorname{pr}_1(f(x,a_0))$, then $M$ preserves composition and identities.
  Thus it preserves equivalences, inducing a map $(X\times A \equiv X\times A)\to (X\equiv X)$.
  We easily have $M\circ L = \operatorname{id}$, so to prove $L\circ M = \operatorname{id}$ it suffices to show that $M$ is left-cancellable, i.e.\ that $(M f = M g) \to (f = g)$.
  Since $M$ preserves composition, for this it suffices to show that if $M f = \operatorname{id}$ then $f = \operatorname{id}$.
  But if $M f = \operatorname{id}$, then by~\eqref{eq:rigid-prod-star} we have $\operatorname{pr}_1(f(x,a)) = x$ for all $a:A$.
  Thus $f(x,a) = (x,g_x(a))$, where $g_x:A\equiv A$ for each $x:X$.
  But $A$ is rigid, so each $g_x = \operatorname{id}$, hence $f=\operatorname{id}$.
\end{proof}

For instance, we could take $n=0$ and $X=\mathbf{2}$, so that $X\times A \equiv A+A$.
Thus if $A$ and $B$ are any connected rigid types, an automorphism of $\mathcal{U}$ can swap $A+A$ with $B+B$.

There might also be rigid types that are not of the form $BG$, or types $A,B$ not built out of rigid ones but such that $A\not\equiv B$ and $\mathcal{U}_A\equiv \mathcal{U}_B$.
But now we will leave such questions and turn to the converse: when does an automorphism of $\mathcal{U}$ imply excluded middle?


\subsection{Excluded middle from automorphisms}
\label{sec:excluded-middle-from}

In fact, without function extensionality, we can only derive a slightly weaker form of excluded middle from a nontrivial automorphism of the universe.
As defined in the introduction, the \emph{law of excluded middle} (\ensuremath{\operatorname{LEM}}) is
\[
\prod_{P:\mathcal{U}} \operatorname{isProp}(P) \to P + \neg P.
\]
We will instead derive the law of \emph{double-negation elimination} (\ensuremath{\operatorname{DNE}}), which is
\[
\prod_{P:\mathcal{U}} \operatorname{isProp}(P) \to \neg\neg P \to P.
\]
Notice that if $\mathbf{0}$-valued function extensionality holds, then
$\neg P$ is a proposition (even if $P$ is not a proposition) and hence,
if $P$ is a proposition, $P+\neg P$ is a proposition equivalent to
$P\vee \neg P$.
In first-order or higher-order logic, the corresponding schemas or
axioms of excluded middle and double-negation elimination are
equivalent, but, in type theory, one direction seems to require some
amount of function extensionality:
\begin{lemma} \label{lem:is:dne} \leavevmode
  \begin{enumerate}
  \item \label{lem:gives:dne} \ensuremath{\operatorname{LEM}}\ implies \ensuremath{\operatorname{DNE}}.
  \item \label{dne:gives:lem} \ensuremath{\operatorname{DNE}}\ implies \ensuremath{\operatorname{LEM}}\, assuming $\mathbf{0}$-valued function extensionality.
  \end{enumerate}
\end{lemma}
\begin{proof}
  (\ref{lem:gives:dne}):~Assume \ensuremath{\operatorname{LEM}}\ and let $P:\mathcal{U}$ with
  $\operatorname{isProp}(P)$ and assume $\neg\neg P$.  By excluded middle, either
  $P$ or $\neg P$. In the first case we are done, and the second
  contradicts $\neg \neg P$.
  (\ref{dne:gives:lem}):~Assume \ensuremath{\operatorname{DNE}}\ and let $P:\mathcal{U}$ with
  $\operatorname{isProp}(P)$. By $\mathbf{0}$-valued function extensionality,
  $P + \neg P$ is a proposition, and hence \ensuremath{\operatorname{DNE}}\ gives $P + \neg P$,
  because we always have $\neg \neg (P + \neg P)$.
\end{proof}

\begin{lemma}
\label{dne:dne-negation}
\ensuremath{\operatorname{DNE}}\ holds if and only if every proposition is logically equivalent
to the negation of some type.
\end{lemma}
\begin{proof}
  ($\Rightarrow$):~\ensuremath{\operatorname{DNE}}\ gives that any proposition $P$ is logically
  equivalent to the negation of the type $\neg P$.
  ($\Leftarrow$):~For any two types $A$ and $B$, we have that
  $A \to B$ implies $\neg B \to \neg A$. Hence $A \to B$ also gives
  $\neg \neg A \to \neg \neg B$. And, because $X \to \neg \neg X$ for
  any type $X$, we have $\neg \neg \neg X \to \neg X$. Therefore, if
  $P$ is logically equivalent to the negation of $X$, we have the
  chain of implications
  $\neg \neg P \to \neg \neg \neg X \to \neg X \to P$.
\end{proof}

Our first automorphism of the universe constructed from excluded
middle swapped the empty type with the unit type.  We now show that conversely, any
such automorphism implies \ensuremath{\operatorname{DNE}}\, and hence, assuming $\mathbf{0}$-valued
function extensionality, also~\ensuremath{\operatorname{LEM}}.
In fact, not even an \emph{embedding} of $\mathcal{U}$ into itself that maps
the unit type to the empty type is possible without classical axioms:
\begin{theorem} \label{left:cancellable} Assuming propositional
  extensionality, if there is a left-cancellable map $f: \mathcal{U} \to \mathcal{U}$
  with $f(\mathbf{1})=\mathbf{0}$, then \ensuremath{\operatorname{DNE}}\ holds.
\end{theorem}
\begin{proof}
  For an arbitrary proposition $P$, we have:
  \begin{align*}
    P \,\!& \leftrightarrow  P = \mathbf{1} \quad
    && \mbox{(by propositional extensionality)}
    \\
        &\leftrightarrow  f(P)=f(\mathbf{1})
    && \mbox{(because $f$ is left-cancellable)}
    \\
        &\leftrightarrow f(P)=\mathbf{0}
    && \mbox{(by the assumption that $f(\mathbf{1})=\mathbf{0}$)}
    \\
        &\leftrightarrow \neg f(P)
          && \mbox{(by propositional extensionality).}
  \end{align*}
  (Note that if $\neg f(P)$, then $f(P) \leftrightarrow \mathbf{0}$, so $f(P)$ is a
  proposition and we can apply propositional extensionality to get
  $f(P)=\mathbf{0}$.)
  Hence $P$ is logically equivalent to the negation of the type
  $f(P)$, and therefore Lemma~\ref{dne:dne-negation} gives \ensuremath{\operatorname{DNE}}.
\end{proof}

\begin{corollary}
\label{thm:automorphism}
Assuming propositional extensionality, if there is an automorphism of the
universe that maps the unit type to the empty type, then \ensuremath{\operatorname{DNE}}\ holds.
\end{corollary}

Now let us further assume univalence and propositional truncations.
This implies function extensionality, so the difference between \ensuremath{\operatorname{DNE}}\ and \ensuremath{\operatorname{LEM}}\ disappears.
Furthermore, we can additionally generalize the result as follows.  Say
that a type $A$ is \emph{inhabited} if the unique map $A\to\mathbf{1}$ is
surjective. This is equivalent to giving an element of the propositional
truncation~$\trunc{A}$.
\begin{lemma}\label{lem:prop-equivalent}
  Assuming univalence and propositional truncations, if $A$ is an
  inhabited type, then any proposition $P$ is logically equivalent to
  the identity type $(P \times A) = A$.
\end{lemma}
\begin{proof}
  If $P$ then $P \equiv \mathbf{1}$, so $(P \times A) \equiv A$, and hence
  by univalence $(P \times A) = A$.  Conversely, assume $(P \times A)
  = A$.  Then $\trunc{P \times A} = \trunc{A} = \mathbf{1}$ by univalence,
  as $A$ is inhabited.  So $\trunc{P}\times\trunc{A}=\mathbf{1}$, and hence
  $P=\mathbf{1}$.
\end{proof}
Using this, we can weaken the hypothesis of Lemma~\ref{left:cancellable} to the requirement that $f$
maps some inhabited type to the empty type, and get the same
conclusion, at the expense of
requiring univalence rather than just propositional extensionality:
\begin{lemma} \label{left:cancellable:bis}
  Assuming univalence and propositional truncations, if there is a
  left-cancellable map $f: \mathcal{U} \to \mathcal{U}$ with $f(A)=\mathbf{0}$ for some
  inhabited type $A$, then excluded middle holds.
\end{lemma}
\begin{proof}
  For an arbitrary proposition $P$, we have:
  \begin{align*}
    P \,\!& \leftrightarrow  (P \times A) = A \quad
    && \mbox{(by Lemma~\ref{lem:prop-equivalent})}
    \\
        &\leftrightarrow  f(P \times A)=f(A)
    && \mbox{(because $f$ is left-cancellable)}
    \\
        &\leftrightarrow f(P \times A)=\mathbf{0}
    && \mbox{(by the assumption that $f(A)=\mathbf{0}$)}
    \\
        &\leftrightarrow \neg f(P \times A)
          && \mbox{(by propositional extensionality).}
  \end{align*}
  Hence $P$ is logically equivalent to the negation of the type
  $f(P\times A)$, and therefore Lemma~\ref{dne:dne-negation} gives
  \ensuremath{\operatorname{DNE}}. But univalence gives function extensionality, and hence
  Lemma~\ref{lem:is:dne} gives \ensuremath{\operatorname{LEM}}.
\end{proof}
\begin{theorem
\label{thm:automorphism:bis}
Assuming univalence and propositional truncations, if there is an
automorphism of the universe that maps some inhabited type to the
empty type, then excluded middle holds.
\end{theorem}

\begin{corollary}\label{cor:0:beers}
  Assuming univalence and propositional truncations, if there is an
  automorphism $g : \mathcal{U} \to \mathcal{U}$ of the universe with $g(\mathbf{0}) \ne
  \mathbf{0}$, then the double negation \[ \neg \neg \prod_{P:\mathcal{U}}
  \operatorname{isProp}(P) \to P + \neg P \] of the law of excluded middle
  holds.
\end{corollary}
(Note that this is not the same as
\[ \prod_{P:\mathcal{U}}  \operatorname{isProp}(P) \to \neg \neg (P + \neg P ), \]
which is of course constructively valid without extra assumptions.)

\begin{proof}
  Let $f$ be the inverse of $g$. If $g(\mathbf{0})$ then
  $\trunc{g(\mathbf{0})}$, and because $f$ maps $g(\mathbf{0})$ to
  $\mathbf{0}$, we conclude that excluded middle holds by
  Theorem~\ref{thm:automorphism:bis}.  But the assumption
  $g(\mathbf{0}) \ne \mathbf{0}$ is equivalent to $\neg \neg g(\mathbf{0})$ by
  propositional extensionality, and so it implies the double negation of
  excluded middle.
\end{proof}

It is in general an open question for which $X$ the existence of an
automorphism $f:\mathcal{U} \to \mathcal{U}$ with $f(X)\neq X$ implies a non-provable
consequence of excluded middle~\cite{automorphisms:escardo:bet}. Not
even for $X=\mathbf{1}$ do we know whether this is the case. However, the
following two cases for $X$ follow from the case $X=\mathbf{0}$ discussed
above:
\begin{corollary}\label{cor:lem:beers}
  Assuming univalence and propositional truncations, for universes
  $\mathcal{U}:\mathcal{V}$, if there is an automorphism $f:\mathcal{V} \to \mathcal{V}$ with
  $f(X) \ne X$ for $X=\ensuremath{\operatorname{LEM}}_\mathcal{U}$ or $X=\neg \neg \ensuremath{\operatorname{LEM}}_\mathcal{U}$, then
  $\neg \neg \ensuremath{\operatorname{LEM}}_\mathcal{U}$ holds.
\end{corollary}
\begin{proof}
  Suppose that $\neg\ensuremath{\operatorname{LEM}}_\mathcal{U}$, and hence $X=\mathbf{0}$.  By
  Corollary~\ref{cor:0:beers}, we obtain $\neg\neg\ensuremath{\operatorname{LEM}}_\mathcal{V}$, which
  implies $\neg\neg \ensuremath{\operatorname{LEM}}_\mathcal{U}$, contradicting the assumption.
\end{proof}

\typesorarxiv{
  \subparagraph*{Acknowledgements.}
}{
  \paragraph*{Acknowledgements.}
}

The first-named author would like to thank Uday Reddy for discussions
about parametricity.
We would also like to thank Jean-Philippe Bernardy for helpful comments, and Andrej Bauer for
discussions and questions.
The fact that the implication $\ensuremath{\operatorname{DNE}} \to \ensuremath{\operatorname{LEM}}$ requires $\mathbf{0}$-valued
function extensionality was spotted by one of the referees. Since
then, we have formalized the results to make sure we didn't miss
similar assumptions. All results of the paper, except
Section~\ref{sec:autom-that-do}, are formalized in
Agda~\cite{auke:development}. All results of
Sections~\ref{sec:autom-that-do} and~\ref{sec:excluded-middle-from}
are formalized in Coq~\cite{hottcoq} 
(in the files \verb+Spaces/BAut/Rigid.v+ and \verb+Spaces/Universe.v+).
(So some results have been formalized twice, and no numbered result has been left unformalized.)

