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.
FYI, you can just type "choice operator" in double brackets here on the forum, just like on the lab, and it will become a link choice operator. Thanks; your discussion looks relevant enough to go in the main text rather than in a query box.
I added a comment at the bottom of choice operator that it is inconsistent with the univalence axiom.
Added generalized the as an alternative in the case of unique specification.
1 to 7 of 7