@MartinEscardo@mathstodon.xyz
@MartinEscardo@mathstodon.xyz avatar

MartinEscardo

@MartinEscardo@mathstodon.xyz

Professor at the University of Birmingham, UK.
I am interested in constructive mathematics and (constructive and non-constructive) homotopy type theory and univalent foundations, connections of topology with computation, (infinity) topos theory, locale theory, domain theory, combinatorial game theory and much more.

This profile is from a federated server and may be incomplete. Browse more on the original instance.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

The main duty of the programmer, in practice, is to implement bugs, and then debug the resulting programs.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

Paulo Oliva and I, in our work on combinatorial game theory, ended up needing to use relative monads, as opposed to just monads as in our previous work.

I had never paid much attention to relative monads, but they were on the back of my mind, and when something went wrong, we looked at them, and this is what was needed to sort out our troubles.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

The first paper on the subject has a very descriptive title:

Monads need not be endofunctors.
https://link.springer.com/chapter/10.1007/978-3-642-12032-9_21

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

I would like to advertise the PhD Thesis of my former student, and recently, new colleague, @todd

His thesis explores optimisation and regression in constructive univalent mathematics.

https://arxiv.org/abs/2401.09270

For this, he applied the theory of searchable types to real numbers.

Moreover, he formalized his results in TypeTopology in Agda.

https://www.cs.bham.ac.uk/~mhe/TypeTopology/TWA.Thesis.index.html

Because he was a member of staff when he defended his thesis, he needed two external examiners (and wasn't allowed to have an internal examiner) in the UK system. They were John Longley and Ulrich Berger.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

Tomorrow morning I am going to talk about Pataraia's fixed point theorem in an internal seminar.

Every monotone endomap of a directed complete poset with a least element has a least fixed point.

The proof is constructive in the sense of topos logic.

What happens when we dissect this proof in MLTT, or less generally in MLTT with HoTT/UF extensions?

I may write a thread about this here in the next few days, based on my talk.

This is joint work with @de_Jong_Tom

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

The northern lights are visible from our garden and from our bedroom window right now.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

It is just me? The following definition of category hurts my categorical instincts, because it uses object equality.

A category consists of

  1. A collection of objects.

  2. A collection of morphisms.

  3. Each morphism f has two assigned objects, its source s(f) and its target t(f).

  4. For each pair of morphisms f,g such that t(f)=s(g) there exists a specified morphism g ∘ f such that [it doesn't matter what]

  5. [Some axioms are satisfied.]

It is (4) that hurts my categorical instincts.

There is no reason to have "evilness" (in the categorical sense, rather than the emotional sense) built-in in the definition of category!

This definition is, for example, adopted by Freyd.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez @oantolin

I think the nuances matter, because most people stick with faith to the first definitions they have seen, regarding them as sacrosanct.

typeswitch, to random
@typeswitch@gamedev.lgbt avatar

maybe a better way to say "judgmental equality" is "coincidence" 🤔

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@typeswitch

I prefer to call it "definitional equality" rather than "judgmental equality".

There is a difference between having "0 + x = x" by definition, and "x + 0 = x" by proof.

People complain that type theory "suffers" from this "defect".

But this is the case even in Peano arithmetic. The definition gives one of the equalities, and a proof is required for the other (by induction).

What is different in type theory from e.g. Peano arithmetic, and more generally first-order logic with equality, is that we can "literally" substitute along both definitional and "proved" equality in Peano arithmetic, while in type theory we can substitute "literally" along definitional equalities, but only via transport along "proved" equalities.

This may be seen as a "defect" of dependent type theory (and many people view it like that), but it may also be seen as a virtue, allowing the existence of HoTT/UF.

I am among the people who see this as a virtue.

This view is very reasonable if you see dependent type theory as "proof relevant as articulated by the Curry-Howard interpretation". Why should "proved" equality be different from other "proved" things?

Definitional equality is "literally" substitutional, while "proved" equality is substitutional "up to (proof) transport".

Definitional equality doesn't have witnesses, and this is why it can be "substituted literally".

Proved equality does have witnesses, which may not be definitionally equal themselves.

It is rather remarkable how "proof relevant" equality matches ∞-categorical thinking quite precisely. It is the kind of mathematical coincidence that makes me love mathematics.

BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

I'm struggling with the definition of the category of elements--the direction of morphisms. Grothendieck worked with presheaves (C^{op} \to \mathbf{Set}), with a morphism ((a, x) \to (b, y)) being an an arrow (a \to b) in (C). The question is, what is it for co-presheaves? Is it (b \to a)? nLab defines it as (a \to b) and doesn't talk about presheaves. Emily Riehl defines both as (a \to b), which makes one wonder what it is for (𝐶ᵒᵖ)ᵒᵖ→𝐒𝐞𝐭 , not to mention (C^{op}\times C \to \mathbf{Set}).

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez @BartoszMilewski

This reminds me that two different communities write the specialization order for points x and y of a topological space as x ≤ y and y ≤ x respectively.

It is just a matter of convention.

But it does make papers from the other community very hard to read, as we need to flip the order every time in our heads to match our intuition and previous knowledge.

christianp, to random
@christianp@mathstodon.xyz avatar

Should I be concerned that my phone has stopped showing Microsoft access code requests?
I can't log in to Outlook or Teams on anything that isn't already logged in.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@christianp My phone also stopped getting these requests a few months ago. But I can use Authy instead - you should be able to, too.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

What is a topological space?

It is a mathematical device to define what a continuous function is, in a general setting.

  1. A topological space is a set X together with a collection of subsets of X, called open, such that finite intersections of open sets are open, and arbitrary unions of open sets are open.

  2. A function of topological spaces is continuous if inverse images of open sets are open.

What is the intuition behind (1) and (2)?

I claim that it is better to ask, instead, how mathematicians came up with (1) and (2).

1/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

At the beginning, people considered continuous functions ℝ → ℝ.

One of the wrong intuitions, at that time, was that such a function is continuous if "you can draw it without lifting the pen".

A counter-example is Cantor's devil's staircase. This function you can't draw, with or without lifting the pen.

https://en.wikipedia.org/wiki/Cantor_function

Mathematicians spoke of continuous functions for a long time before there was a precise definition of continuous function. This was a vague idea, which, nevertheless, was useful.

At some point the definition of continuity for a function f : ℝ → ℝ was elucidated.

∀ x ∈ ℝ , ∀ ε > o, ∃ δ > 0 , ∀ x' ∈ ℝ, ∣ x - x' | < δ → | f(x) - f(x') | < ε.

This definition allowed a lot of theorems to be proved rigorously. This is why it was useful.
A lot of theorems that were claimed, could now be proved.
2/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

This definition does have an intuition.

Suppose you want to calculate f(x₀), for example because you are an engineer and want to build a bridge, where x₀ is a physical quantity. Unfortunately, we can't measure x₀ exactly.

But you still want to know what y₀ = f (x₀) is, at least approximately.

But "approximately" doesn't mean anything. You want to know y₀, say, with two correct decimal digits. This will do to build a robust bridge.

Then the question is, how many correct digits of x₀ do you need to know, in order to get the desired two decimal digits of y₀?

More generally, we want the following to be the case. In order to know n digits of output of the function, it is enough to know m digits of the input, where m depends on the input and on n.

This is possible if and only if the function is continuous.

So one intuition about continuity is that "finite amounts of output depend on only finite amounts of input".

3/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

But this was for functions ℝ → ℝ only.

Soon people started to consider continuous functions "of two variables", that is, functions ℝ × ℝ → ℝ, and then of n variable, so ℝⁿ → ℝ, and in each case a different definition was needed.

Moreover, because people were trying to e.g. solve differential equations, which amounts to given one input function (called the initial condition) to figure out an output function (the solution), people came across functions mapping continuous functions to continuous functions, which, themselves, may or may not be continuous.

So a general definition of continuity was needed to clean up the mess and be able to make progress more efficiently.

A first, rather useful, general setting was that of a metric space. You say what the distance between two things (e.g. real numbers, tuples of real numbers, continuous functions) is. The axioms for metric spaces are very intuitive, and I won't reproduce their statement here.

But I want to say this.

  1. The definition of continuity is the same as above, with the absolute value of the difference replaced by the distance function d. A function f : X → Y is continuous iff

∀ x ∈ X , ∀ ε > o, ∃ δ > 0 , ∀ x' ∈ X, d(x,x') < δ → d(f(x),f(x')) < ε.

  1. We can then define a set U to be open if for every x ∈ U there is ε > 0 such that every x' with d(x,x') < ε is in U.

  2. The open sets are closed under finite intersections and arbitrary unions.

  3. A function is continuous in the above ε-δ sense iff inverse images of open sets are open.

4/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

This, and much more, is beautifully explained in the book

George F. Simmons. Topology and modern analysis
https://archive.org/details/introduction-to-topology-and-modern-analysis-simmons

which I highly recommend.

What happens next is that metric spaces are not enough. There are sets on which we want to consider continuous functions which can't be metrized so that metric continuity coincides with the notion of continuity we want.

I like this book because it starts from trivial things, making them less and less trivial as we progress, until it gets eventually to many things, including Stone duality. I self-learned topology from this book as an undergrad.

5/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

Then comes computer science. Smyth, Abramsky and Vickers propose a radically different intuition for the axioms of topology and the definition of continuous function.

I will stop this post at this point, at least for now, giving four seminal references.

Michael .B. Smyth. Power domains and predicate transformers: a topological view.
https://link.springer.com/chapter/10.1007/BFb0036946

Michael .B. Smyth. Topology.
https://dl.acm.org/doi/10.5555/162573.162536

Samson Abramsky. Domain Theory and the logic of observable properties
https://arxiv.org/abs/1112.0347

Steve Vickers. Topology via logic.
https://www.cambridge.org/gb/universitypress/subjects/computer-science/programming-languages-and-applied-logic/topology-logic?format=PB&isbn=9780521576512

I started my PhD after reading the above, and I was lucky to have had Smyth as my supervisor.

6/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

But one should say the following. Actually, the connection of topology with computation started with Brouwer, who was a topologist himself, in fact one of the founding fathers of topology before Hausdorff come up with the axiomatization of topological spaces which I described above.

7/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

And finally, in the same way metric spaces were not enough, and so we moved from metric spaces to topological spaces, Grothendieck found that topological spaces were not enough for him, and so he needed, more generally, toposes.

And recently condensed sets and pyknotic sets have also been proposed as a convenient generalization of the notion of (topological) space.

It is easy to lose track of the original intuitions. It is also easy for new intuitions to replace the original ones, when we move to more general settings. And we always move to more general settings in mathematics.

8/

ProfKinyon, to random
@ProfKinyon@mathstodon.xyz avatar

A mathematics paper without open problems is like... uh... a ma(th)stodon post without a punchline.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@ProfKinyon

If you want your paper to be cited, it must have at least one tricky open problem.

johncarlosbaez, (edited ) to random
@johncarlosbaez@mathstodon.xyz avatar

One of my favorite philosophers of mathematics is David Corfield. He rejects the "foundationalist filter": the idea that philosophers need only concern themselves with the foundations of math. He believes not only traditional logic and set theory but many branches of modern math are full of mind-blowing ideas that philosophers should study. And that's what he's done, starting in his book "Towards a Philosophy of Real Mathematics" and continuing on with "Modal Homotopy Type Theory".

His position was not always popular. While his work is great, it took him 12 years after his PhD to land a permanent job.

In 2007 he got one at the University of Kent. But then the Tories began starving universities of funding, forcing them to rely more and more on tuition from foreign students. And now, following the narrow-minded spirit of Brexit, the Tories have decided to "clamp down" on foreign students, denying them visas. This has produced a dramatic drop in foreign students, and massive budget shortfalls.

Already a quarter of UK universities are laying off staff. The University of Kent has decided to close down their philosophy department. So now, through no fault of his own, David needs to find a new job.

He's a really smart guy with a remarkable track record. If you have any job ideas or just want to wish him well, you can drop a comment on this blog article:

https://golem.ph.utexas.edu/category/2024/04/moving_on_from_kent.html

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez

A university without a philosophy department is sad.

I am sorry for him.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

This looks interesting for PhD students flirting with univalent foundations:

https://unimath.github.io/minneapolis2024/

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

What does "mute conversation" on a post do?

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez

Thanks.

Anyway, I deleted the post.

But it's good to know how things work.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez

Nobody was annoying, but the post was getting too many boosts and favourites, polluting my notifications.

Also, it was intended to be more rhetoric than factual, but, when we put things in writing here in this medium, the rhetoric and irony get lost.

I am here for the maths, cs and logic, and this impromptu thought got on the way of my objectives here.

andrejbauer, to random
@andrejbauer@mathstodon.xyz avatar

What is the correct reply to a mathematician, who has never formalized anything, asking how they would go about formalizing a research paper of theirs?

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@joshuagrochow @11011110 @andrejbauer

Because formalizing Turing Machines is, indeed, a "huge pain", as you say, back in 2017, my former student Cory Knapp and I came up with "Abstract Turing Machines" to ease the pain.

You may want to check whether this suits you.

A joint paper with him:

https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.21

His thesis:

Partial Functions and Recursion in Univalent Type Theory
https://arxiv.org/abs/2011.00272

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • JUstTest
  • GTA5RPClips
  • DreamBathrooms
  • thenastyranch
  • magazineikmin
  • everett
  • InstantRegret
  • Youngstown
  • mdbf
  • slotface
  • rosin
  • modclub
  • kavyap
  • Leos
  • normalnudes
  • cubers
  • osvaldo12
  • tacticalgear
  • Durango
  • khanakhh
  • ngwrru68w68
  • provamag3
  • anitta
  • tester
  • cisconetworking
  • ethstaker
  • megavids
  • lostlight
  • All magazines
    •