Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
In the Definition-section (here) I have
added an illustrating graphics (the same that i just added at suspension, but with the labels matched to the inductive generators used here)
Also made some minor adjustments to the text:
Since this here is about un-reduced suspension, it seems a good idea to denote it by instead of by .
(This is more in line with tradition, more suggestive of the key fact , and, last not least, avoids the bad notational clash with the traditional type theoretic notation for dependent sums.)
1 to 3 of 3