Differential Geometry in Modal HoTT

Posted on 21 August 2018 by

As some of you might remember, back in 2015 at the meeting of the german mathematical society in Hamburg, Urs Schreiber presented three problems or “exercises” as he called it back then. There is a page about that on the nLab, if you want to know more. In this post, I will sketch a solution to some part of the first of these problems, while the occasion of writing it is a new version of my article about this, which now comes with a long introduction.

Urs Schreiber’s problems were all about formalizing results in higher differential geometry, that make also sense in the quite abstract setting of differential cohesive toposes and cohesive toposes.
A differential cohesive topos is a topos with some extra structure given by three monads and three comonads with some nice properties and adjunctions between them. There is some work concerned with having this structure in homotopy type theory. A specialized cohesive homotopy type theory concerned with three of the six (co-)monads, called real-cohesive homotopy type theory was introduced by Mike Shulman.

What I want to sketch here today is concerned only with one of the monads of differential cohesion. I will call this monad coreduction and denote it with \Im. By the axioms of differential cohesion, it has a left and a right adjoint and is idempotent. These properties are more than enough to model a monadic modality in homotopy type theory. Monadic modalities were already defined at the end of section 7 in the HoTT-Book and named just “modalities” and it is possible to have a homotopy type theory with a monadic modality just by adding some axioms — which is known not to work for non-trivial comonadic modalities.

So let us assume that \Im is a monadic modality in HoTT. That means that we have a map \Im:\mathcal U\to \mathcal U and a unit

\iota:\prod_{X:\mathcal U} X\to \Im X

such that a property holds, that I won’t really go into in this post — but here it is for completeness: For any dependent type E:\Im X\to\mathcal U on some type X, such that the unit maps \iota_{E(x)} are equivalences for all x:X, the map

\_\circ\iota_X:\left(\prod_{x:\Im X}E(x)\right)\to\prod_{x:X}E(\iota_X(x))

is an equivalence. So the inverse to this map is an induction principle, that only holds for dependent types subject to the condition above.
The n-truncations and double negation are examples of monadic modalities.

At this point (or earlier), one might ask: “Where is the differential geometry”? The answer is that in this setting, all types carry differential geometric structure that is accessible via \Im and \iota. This makes sense if we think of some very special interpretations of \Im and \iota (and HoTT), where the unit \iota_X is given as the quotient map from a space X to its quotient \Im X by a relation that identifies infinitesimally close points in X.
Since we have this abstract monadic modality, we can turn this around and define the notion of two points x,y:X being infinitesimally close, denoted “x\sim y” in terms of the units:

(x\sim y) :\equiv (\iota_X(x)=\iota_X(y))

where “\_=\_” denotes the identity type (of \Im X in this case). The collection of all points y in a type X that are infinitesimally close to a fixed x in X, is called the formal disk at x. Let us denote it with D_x:

D_x:\equiv \sum_{y:X}y\sim x

Using some basic properties of monadic modalities, one can show, that any map f:X\to Y preserves inifinitesimal closeness, i.e.

\prod_{x,y:X}(x\sim y)\to (f(x)\sim f(y))

is inhabited. For any x in A, we can use this to get a map

df_x:D_x\to D_{f(x)}

which behaves a lot like the differential of a smooth function. For example, the chain rule holds

d(f\circ g)_x = df_{g(x)}\circ dg_x

and if f is an equivalence, all induced df_x are also equivalences. The latter corresponds to the fact that the differential of a diffeomorphism is invertible.
If we have a 0-group G with unit e, the left tranlations g\cdot\_:\equiv x\mapsto g\cdot x are a family of equivalences that consistently identify D_e with all other formal disks D_x in G given by the differentials d(g\cdot\_)_e.
This is essentially a generalization of the fact, that the tangent bundle of a Lie-group is trivialized by left translations and a solution to the first part of the first of Urs Schreiber’s problems I mentioned in the beginning.

With the exception of the chain rule, all of this was in my dissertation, which I defended in 2017. A couple of month ago, I wrote an article about this and put it on the arxiv and since monday, there is an improved version with an introduction that explains what monads \Im you can think of and relates the setup to Synthetic Differential Geometry.
There is also a recording on youtube of a talk I gave about this in Bonn.
 

Posted in Uncategorized | 8 Comments

HoTT 2019

Posted on 7 June 2018 by

Save the date!  Next summer will be the first:

International Conference on Homotopy Type Theory
(HoTT 2019)
Carnegie Mellon University
12 – 17 August 2019

There will also be an associated:

HoTT Summer School
7 – 10 August 2019

More details to follow soon!

Here is the conference website.

Posted in News | 6 Comments

UF-IAS-2012 wiki archived

Posted on 7 May 2018 by

The wiki used for the 2012-2013 Univalent Foundations program at the Institute for Advanced Study was hosted at a provider called Wikispaces. After the program was over, the wiki was no longer used, but was kept around for historical and archival purposes; much of it is out of date, but it still contains some content that hasn’t been reproduced anywhere else.

Unfortunately, Wikispaces is closing, so the UF-IAS-2012 wiki will no longer be accessible there. With the help of Richard Williamson, we have migrated all of its content to a new archival copy hosted on the nLab server:

Let us know if you find any formatting or other problems.

Posted in News | 2 Comments

A self-contained, brief and complete formulation of Voevodsky’s univalence axiom

Posted on 7 March 2018 by

I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web.

For some time I was a bit upset about this. But maybe this is our fault, by often trying to explain univalence only imprecisely, mixing the explanation of the models with the explanation of the underlying Martin-Löf type theory, with none of the two explained sufficiently precisely.

There are long, precise explanations such as the HoTT book, for example, or the various formalizations in Coq, Agda and Lean.

But perhaps we don’t have publicly available material with a self-contained, brief and complete formulation of univalence, so that interested mathematicians and logicians can try to contemplate the axiom in a fully defined form.

So here is an attempt of a  self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom in the arxiv.

This has an Agda file with univalence defined from scratch as an ancillary file, without the use of any library at all, to try to show what the length of a self-contained definition of the univalence type is. Perhaps somebody should add a Coq “version from scratch” of this.

There is also a web version UnivalenceFromScratch to try to make this as accessible as possible, with the text and the Agda code together.

The above notes explain the univalence axiom only. Regarding its role, we recommend Dan Grayson’s introduction to univalent foundations for mathematicians.

Posted in Uncategorized | Leave a comment

HoTT at JMM

Posted on 13 November 2017 by

At the 2018 U.S. Joint Mathematics Meetings in San Diego, there will be an AMS special session about homotopy type theory. It’s a continuation of the HoTT MRC that took place this summer, organized by some of the participants to especially showcase the work done during and after the MRC workshop. Following is the announcement from the organizers.

We are pleased to announce the AMS Special Session on Homotopy Type Theory, to be held on January 11, 2018 in San Diego, California, as part of the Joint Mathematics Meetings (to be held January 10 – 13).

Homotopy Type Theory (HoTT) is a new field of study that relates constructive type theory to abstract homotopy theory. Types are regarded as synthetic spaces of arbitrary dimension and type equality as homotopy equivalence. Experience has shown that HoTT is able to represent many mathematical objects of independent interest in a direct and natural way. Its foundations in constructive type theory permit the statement and proof of theorems about these objects within HoTT itself, enabling formalization in proof assistants and providing a constructive foundation for other branches of mathematics.

This Special Session is affiliated with the AMS Mathematics Research Communities (MRC) workshop for early-career researchers in Homotopy Type Theory organized by Dan Christensen, Chris Kapulkin, Dan Licata, Emily Riehl and Mike Shulman, which took place last June.

The Special Session will include talks by MRC participants, as well as by senior researchers in the field, on various aspects of higher-dimensional type theory including categorical semantics, computation, and the formalization of mathematical theories. There will also be a panel discussion featuring distinguished experts from the field.

Further information about the Special Session, including a schedule and abstracts, can be found at: http://jointmathematicsmeetings.org/meetings/national/jmm2018/2197_program_ss14.html.
Please note that the early registration deadline is December 20, 2017.

If you have any questions about about the Special Session, please feel free to contact one of the organizers. We look forward to seeing you in San Diego.

Simon Cho (University of Michigan)
Liron Cohen (Cornell University)
Ed Morehouse (Wesleyan University)

Posted in News, Publicity | Leave a comment

Impredicative Encodings of Inductive Types in HoTT

Posted on 11 October 2017 by

I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here.

Known impredicative encodings of various inductive types in System F, such as the type

\forall X. (X\rightarrow X) \rightarrow X \rightarrow X,

of natural numbers do not satisfy the relevant \eta-computation rules. The aim of this work is to refine the System F encodings by moving to a system of HoTT with an impredicative universe, so that the relevant \eta-rules are satisfied (along with all the other rules). As a result, the so-determined types have their expected universal properties. The main result is the construction of a type of natural numbers which is the initial algebra for the expected endofunctor X\mapsto X+\mathbf{1}.

For the inductive types treated in the thesis, we do not use the full power of HoTT; we need only postulate \Sigma-types, identity types, “large” \Pi-types over an impredicative universe \mathcal{U} and function extensionality. Having large \Pi-types over an impredicative universe \mathcal{U} means that given a type \Gamma\vdash A \:\mathsf{type} and a type family \Gamma, x:A \vdash B:\mathcal{U}, we may form the dependent function type

\displaystyle{ \Gamma\vdash \prod_{x:A} B:\mathcal{U}}.

Note that this type is in \mathcal{U} even if A is not.

We obtain a translation of System F types into type theory by replacing second order quantification by dependent products over \mathcal U (or alternatively over the subtype of \mathcal{U} given by some h-level).

For brevity, we will focus on the construction of the natural numbers (though in the thesis, the coproduct of sets and the unit type is first treated with special cases of this method). We consider categories of algebras for endofunctors:

T:\mathbf{Set}\rightarrow\mathbf{Set},

where the type of objects of \mathbf{Set} is given by

\mathsf{Set} :\equiv \displaystyle{\sum_{X:\mathcal{U}}}\mathsf{isSet}(X),

(the type of sets (in \mathcal{U})) and morphisms are simply functions between sets.

We can write down the type of T-algebras:

\mathsf{TAlg} :\equiv \displaystyle{\sum_{X:\mathsf{Set}}} T(X)\rightarrow X

and homomorphisms between algebras \phi and \psi:

\mathsf{THom}(\phi,\psi) :\equiv \displaystyle{\sum_{f:\mathsf{pr_1}(\phi)\rightarrow\mathsf{pr_1}(\psi)}} \mathsf{pr_2}(\psi) \circ T(f) = f \circ \mathsf{pr_2}(\phi),

which together form the category \mathbf{TAlg}.

We seek the initial object in \mathbf{TAlg}. Denote this by 0 and moreover let U be the forgetful functor to \mathbf{Set} and y:\mathbf{TAlg}^{\textnormal{op}}\rightarrow \mathbf{Set}^{\mathbf{TAlg}} be the covariant Yoneda embedding. We reason as follows:

U0 \cong \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(y0,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(1,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}^\mathbf{TAlg}}(\Delta 1,U) \\{}\:\,\,\,\,\,\, = \textnormal{Hom}_{\mathbf{Set}}(1, \textnormal{lim}_{\phi\in\textbf{TAlg}} U\phi) \\{}\:\,\,\,\,\,\, \cong \textnormal{lim}_{\phi\in\textbf{TAlg}} U\phi,

using the fact that the diagonal functor is left adjoint to the limit functor for the last step. With this, we have a proposal for the definition of the underlying set of the initial T-algebra as the limit of the forgetful functor.  Using the fact that U0 is defined as a limit, we obtain an algebra structure \epsilon:TU0\rightarrow U0. As U creates limits, (U0,\epsilon) is guaranteed to be initial in \mathbf{TAlg}.

But we want to define U0 in type theory. We do this using products and equalizers as is well known from category theory. Explicitly, we take the equalizer of the following two maps between products:

P_1,P_2 : \left(\displaystyle{\prod_{\phi:\mathbf{TAlg}}}U(\phi)\right) \rightarrow \displaystyle{\prod_{\phi,\psi:\mathbf{TAlg}}} \: \displaystyle{\prod_{\mu:\mathbf{THom}(\phi,\psi)}}U(\psi),

given by:

P_1 :\equiv \lambda\Phi.\lambda\phi.\lambda\psi.\lambda\mu.\Phi(\psi), \\ P_1 :\equiv \lambda\Phi.\lambda\phi.\lambda\psi.\lambda\mu. \mathsf{pr_1}(\mu)(\Phi(\phi)).

The equalizer is, of course:

E :\equiv \displaystyle{\sum_{\Phi : \prod_{(\phi:\mathbf{TAlg})} U(\phi)}} P_1(\Phi)=P_2(\Phi),

which inhabits \mathsf{Set}. Impredicativity is crucial for this: it guarantees that the product over \mathbf{TAlg} lands in \mathcal{U}.

This method can be used to construct an initial algebra, and therefore a fixed-point, for any endofunctor T : \mathsf{Set}\rightarrow\mathsf{Set}\,!  We won’t pursue this remarkable fact here, but only consider the case at hand, where the functor T is X\mapsto X+\mathbf{1}.  Then the equalizer E becomes our definition of the type of natural numbers (so let us rename E to \mathbb{N} for the remainder). Observe that this encoding can be seen as a subtype of (a translation of) the System F encoding given at the start.  Indeed, the indexing object \prod_{(\phi:\mathbf{TAlg})} U(\phi) of E is equivalent to \prod_{(X:\mathbf{Set})}(X\rightarrow X)\rightarrow X \rightarrow X, by

\begin{aligned} \quad\quad\displaystyle{\prod_{\phi:\mathbf{TAlg}}} U(\phi) \quad &\cong\quad \displaystyle{\prod_{\phi:{\displaystyle{\sum_{X:\mathsf{Set}}} T(X)\rightarrow X}}} U(\phi)\\ &\cong\quad \displaystyle{\prod_{X:\mathsf{Set}}}\, \displaystyle{\prod_{f:T(X)\rightarrow X}} X\\ &\cong\quad \displaystyle{\prod_{X:\mathsf{Set}}}\, (T(X)\rightarrow X) \rightarrow X\\ &\cong\quad \displaystyle{\prod_{X:\mathbf{Set}}}(X\rightarrow X)\rightarrow X \rightarrow X \,. \end{aligned}

With this, we can define a successor function and zero element, for instance:

0 :\equiv \left( \lambda\phi. \mathsf{pr_2}(\phi)\mathsf{inr}(\star), \lambda\phi.\lambda\psi.\lambda\mu. \mathsf{refl}_{\mathsf{pr_2}(\psi)\mathsf{inr}(\star)}\right)

(the successor function takes a little more work). We can also define a recursor \mathsf{rec}_{\mathbb{N}}(e,c), given any C:\mathsf{Set}, e:C\rightarrow C and c:C. In other words, the introduction rules hold, and we can eliminate into other sets. Further, the \beta-rules hold definitionally – as expected, since they hold for the System F encodings.

Finally we come to the desired result, the \eta-rule for \mathbb{N}:

Theorem. Let C:\mathsf{Set}, e:C\rightarrow C and c:C. Moreover, let f:\mathbb{N}\rightarrow C such that:

f(0)=c, \\ f(\mathsf{succ}(x) = e(f(x))

for any x:\mathbb{N}. Then

\mathsf{rec}_{\mathbb{N}}(e,c) =f.

Note that the \eta-rule holds propositionally. By Awodey, Gambino, and Sojakova we therefore also have, equivalently, the induction principle for \mathbb{N}, aka the dependent elimination rule. As a corollary, we can prove the universal property that any T-algebra homomorphism is propositionally equal to the appropriate recursor (as a T-algebra homomorphism). Again we emphasise the need for impredicativity: in the proof of \eta, we have to be able to plug \mathbb{N} into quantifiers over \mathsf{Set}.

A semantic rendering of the above is that we have built a type that always determines a natural numbers object—whereas the System F encoding need not always do so (see Rummelhoff). In an appendix, we discuss a realizability semantics for the system we work in. Building more exotic types (that need not be sets) becomes more complicated; we leave this to future work.

Posted in Applications, Foundations, Uncategorized | 5 Comments

In memoriam: Vladimir Voevodsky

Posted on 1 October 2017 by

VVinLyon

https://www.ias.edu/news/2017/vladimir-voevodsky

Posted in Uncategorized | Leave a comment