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.
Added to distributivity pullback a mention of how it specializes in the internal type theory to the non-axiom of choice. (Also added a mention of the non-axiom of choice at axiom of choice.)
Also added a mention
Where? I couldn’t find it using ctrl-F.
under “connection to distributivity”, at the end.
Todd, in such cases you can click on “see changes” at the bottom, which yields this.
Thanks. Yeah, I know about “see changes” (use it all the time), but for some inexplicable reason didn’t use that time. I see now why Mike said “non-axiom of choice”; originally I was expecting to see the words “non-axiom”.
1 to 7 of 7