Two Queries about Univalent Foundations
Timothy Y. Chow
tchow at math.princeton.edu
Mon Feb 20 17:57:18 EST 2023
Adam Epstein wrote:
> I hadn't realized this: "However the majority of entries in this table
> are proved using techniques which rely on the analytic interpretation.
> The univalent people don't have access to this analytic interpretation
> and hence they seem to be currently far more limited in what they can
> Can you be more explicit here? Which arguments do you have in mind?
> Presumably, "analytic" refers to the use of the actual unit interval of
> real numbers, as opposed to some formal categorically formulation via
> lifting properties? Can you signpost some operation, some long exact
> sequence, etc. that requires analytic tools?
Again, I recommend Brunerie's thesis. He gives a simple example on page
1. Probably the simplest classical way to compute the fundamental group
of a circle S^1 is to use the covering map R -> S^1. But this map is
homotopic to a constant function, so in a totally homotopy-invariant
setting, it cannot tell you anything nontrivial.
More information about the FOM