ME: this theory is good, but it has... how can one say ... too many types? there are in fact, only so many types one can inhabit in the course of a proof. I think I'm right in saying that, aren't I?

PER MARTIN-LÖF: this is absurd!

ME: my good man, don't take it too hard. it's quality maths. there are simply too many types. just remove a few, and it will be perfect.

PER MARTIN-LÖF: which few did you have in mind?

Follow

HOFMANN: this axiom is good, but it has... how can one say ... not enough identity proofs? there are in fact, many ways one can identify a term with another. I think I'm right in saying that, aren't I?

STREICHER: this is absurd!

HOFMANN: my good man, don't take it too hard. it's quality maths. there are simply not enough proofs. just add a few, and it will be perfect.

STREICHER: which few did you have in mind?

· · Web · 0 · 1 · 0
Sign in to participate in the conversation
Vachtnoes

Mastodon is a server for a federated social network: everyone can run a server if they want to, including me. So this is a Mastodon server for me (Vierkantor) and my friends.