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.
I think there was a typo in that the section With identity induction switched from using “B” in the first two instances, to “R” in following instances.
I changed it to all “B“s, assuming that the intention was that the following section uses the same “B“s.
But I am on my phone which makes it hard to harmonize larger chunks of text. Please have a look and double-check.
The claim in the proof that conditions (1-2) are equivalent cannot be true as-stated — namely that for any two families B,C over A the type of equivalences between the total types of B and C is equivalent to the type of pointwise equivalences between B and C. Indeed, one needs in the former case that the equivalences commute with the first projection.
1 to 5 of 5