Daniel R. Grayson
Daniel R. Grayson
What should our new notation for paths over be?
In this figure, it will seem odd to the student that the composed path doesn't lie on its two components.
In group theory, not only do we consider isomorphisms between G and H, but we also have the adjective "isomorphic", which corresponds to the propositional truncation of the identity type....
As suggested by Marc, perhaps we should split the introduction into two parts, so a chapter on symmetries can occur earlier.
Look at this: I think using a font change to indicate application of a function is too cute, and likely to cause confusion.
This lemma is rather special, and gets used only to show that we can form an injection from a predicate. Perhaps we should just prove more generally the the fibers...
Don't we need a proof that problems like the Goldbach conjecture are not decidable by an algorithm, before we assert this?
This looks possibly unintentional: ```diff diff --git a/intro-uf.tex b/intro-uf.tex index 6a7033a..2966b09 100644 --- a/intro-uf.tex +++ b/intro-uf.tex @@ -3052,7 +3052,7 @@ $R : A \to A \to \Prop$, we define the...
Rewrite finite types section (`\subsection{Finite types}`) by putting things into environments. Maybe refer forward to `\section{The type of finite types}` and to `\label{lem:isset-bool}`.