book
book copied to clipboard
HoTT
A textbook on informal homotopy type theory
Here's the proof for easy reference  (In what follows, I've renamed the $f $ in the proof to $\varphi $) For two fibers $(f , eqf) ,(g , eqg)...
First I will provide a snippet of the text for easy reference.  The first thing I wish to address is the use of 'naturality' in the first line of...
In basics.tex, line 1372 (proof of 2.6.4 in the book), the proof concludes with ``` Thus, it remains to show $x = (\proj1 x, \proj2x)$. But this is the propositional...
On the Unimath agda library discord, Martin Escardo wrote: > When we discuss syntax, we do define the terms of a type inductively together with the types themselves, and together...
In the 'first proof' of this lemma the following is stated >  Here it is said, "We will instead define a function with the equivalent type...". What exactly is...
11.3.40 says that if we have `f : Q -> Q -> Q` non-expanding on both components then we can extend it to `f' : R -> R -> R`...
In Section 1.12.2 a proof of the equivalence of path induction and based path induction is provided. I am confused about two things in the latter direction (i.e. path induction...
In option 4 of the ways to construct the single type Ω in defining Dedekind cuts, it says: > On the other end of the spectrum one might ask for...
Following the events of #1101, I am opening an issue to discuss the adoption of a code of conduct. Please note that we already are bound by the [GitHub Community...
