Asserting that
∀a∈A ∃b∈B s.t. P(a, b)
implies
∃f : A ⟶ B s.t. ∀a∈A P(a, f(a))
is just the same as asserting the Axiom of Choice.
This Tweet was deleted by the Tweet author. Learn more
Conversation
I feel like they also have different computational content in a constructive setting? Although nothing jumps out at me for a proof
2
3
They mean different things constructively because the Axiom of Choice isn't constructive. Constructively,
∃f : A ⟶ B s.t. ∀a∈A P(a, f(a))
implies
∀a∈A ∃b∈B s.t. P(a, b)
(just take b = f(a)), but not the converse (since you can't pull f out of thin air).
5
This Tweet was deleted by the Tweet author. Learn more
This Tweet was deleted by the Tweet author. Learn more
I don't really understand your first tweet, but your second has made me finally /feel/ the connection to Choice, so thank you.
Also, under what system is your final remark (about P(a, b1) and P(a, b2))?
1
1
This Tweet was deleted by the Tweet author. Learn more
is there a dual notion to "squash" called "smoosh"?
2
In the world of animation, it’s called “stretch”
I guess if you say squashing is like “the proof is irrelevant, but I can prove I had it”, then stretching could be “I haven’t got it (yet), but it’s irrelevant anyway”—iow, lazily skipping evaluation of irrelevant proofs is sound
1
2
oh yeahh! gotta love the principles of animation. Type theory needs more overlapping motion and follow-throughs!
Replying to
overlap ≅ parallelism ?
follow-through ≅ asynchrony ?
Aside: I take it you didn’t know I was an art major at university
2