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”.
]]>Todd, in such cases you can click on “see changes” at the bottom, which yields this.
]]>under “connection to distributivity”, at the end.
]]>Also added a mention
Where? I couldn’t find it using ctrl-F.
]]>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.)
]]>