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.
You have now added also here exactly what we just discussed in the other thread here.
Why the confusion? I see it’s done correctly already in the HoTT book, p. 201. You could copy from there.
I have reverted the edit from #2 (which was an incomplete duplication of just the same material we just criticized in another thread here).
I’d like to appeal to all “Anonymous” contributors on type theory matters to think twice before making edits: If you don’t dare to sign your contribution with your name, then maybe that means you are not ready yet to edit here. You can still discuss on the nForum, ask questions etc.
1 to 5 of 5