ncfavier

4 ms·

1. 1.▲
   by ncfavier 1y ago

   There arguably has been a failure of communication between type theorists and "traditional" mathematicians, but Buzzard unfortunately has a bit of a history of vocally spreading less-than-accurate information about type theory. I&
2. 2.▲
   by ncfavier 1y ago

   Note that this proof doesn't require the axiom of choice, only excluded middle.
3. 3.▲
   by ncfavier 1y ago

   That sounds about correct. The naïve interpretation of AC that interprets ∃ as Σ and ∀ as Π amounts to the trivial fact that Π distributes over Σ, which has little to do with any choice principle. If you instead interpret it in setoids, as