Two Queries about Univalent Foundations

[Timothy Y. Chow]

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 
> prove;"
>
> 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.

Tim