@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

@christianp Could we have polls with more than four options here on mathstodon?

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@christianp What is the problem if other instances reject them? And, yes, I have seen longer polls in my timeline.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

Because proofs are programs, I don't say "formalize" any more.

I don't formalize proofs - I implement them, in the same way that I don't formalize algorithms and I implement them instead.

Algorithms exist before any programming language, and proofs exist before any so-called foundation.

Algorithms can be implemented in programming languages, and (some) proofs can be implemented in (some) foundations.

BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

Next time an imperative programmer tells you that, unlike in functional programming, in real life things are constantly mutated; remind them that in real life there is no destructive assignment.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@BartoszMilewski

My whiteboard is mutable.

A light switch is mutable.

The ram of my computer is mutable.

My memory is mutable (I forget lots of things).

Just playing devil's advocate.

boarders, to random
@boarders@mathstodon.xyz avatar

does the category Set have more than one elementary topos structure? In the definition we have to pick a representable object for Sub(-), but Sub(-) has typically had an automorphism which flips the ordering and so there are different choices of how 2 represents it (corresponding to not : 2 -> 2). Maybe the structure of a power set object only says there is some choice, but any choice will do.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@boarders The subobject classifier is unique up to unique isomorphism.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

Today I got to my office at 7:30 to get ready for my 10am lecture. It worked. I said everything I wanted to say, I didn't run out of time, I didn't finish too early, and, I think, I managed to answer all student's questions, one of which was a very good one, and took 10 minutes to answer.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@larstiq It was too specific to make sense in a public forum like this without basically repeating half of the lecture - sorry! I've already given the lecture today. Don't feel like doing it again. 🙂

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez I think I'll watch a movie. I tried to read a book but I didn't manage.

JadeMasterMath, to random

Hey check this out: https://jadeedenstarmaster.wordpress.com/2024/02/21/can-enriched-category-theory-compute-an-experiment-in-idris2/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@johncarlosbaez @JadeMasterMath

Sometimes "semi" things are (1) defective, and (2) interesting in their own right, and (3) central to a theory.

One example is "semidecidable" as opposed to "decidable" in computability theory. And in practice too: we always aim for decidability, but sometimes we have to live with semidecidability as the next best thing.

But I agree, in general, that "semi", "quasi", "pseudo" are terms that arise by lack of imagination for better terms.

And "rig" shows good imagination for naming.

christianp, to random
@christianp@mathstodon.xyz avatar

Still playing whack a mole with the spammers.

Is anyone making a bayesian spam filter for mastodon?

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@christianp Thanks for your work on this.

On my end I have reported more than 10 spam posts, and this is getting very annoying. It must be much more annoying for you.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@christianp Yeah, I think so! When I tried to report them, they didn't exist any more. Thanks!

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

https://www.cl.cam.ac.uk/events/syco/12/

The Symposium on Compositional Structures (SYCO) is an interdisciplinary series of meetings aiming to support the growing community of researchers interested in the phenomenon of compositionality, from both applied and abstract perspectives, and in particular where category theory serves as a unifying common language.

SYCO 12 will be hosted on the 15-16 April at the University of Birmingham, UK; abstract submissions and registration are now open.

The local organizers are @todd and @georgejkaye and the invited speakers are Miriam Backens (INRIA) and Sean Moss (Birmingham).

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

https://www.cs.le.ac.uk/events/mgs2024/

The Midlands Graduate School (MGS) provides an intensive programme of lectures on the Mathematical Foundations of Computing Science. It has run annually since 1999 and has been held at either the University of Birmingham, the University of Leicester, the University of Nottingham, or at the University of Sheffield. The lectures are aimed at postgraduate/PhD students, typically in their first or second year of study for a PhD. However, the school is open to anyone who is interested in learning more about mathematical computing foundations, and all such applicants are warmly welcomed. We very much encourage students from abroad to attend, participants from industry, and many have done so in the past.

Celebrating 25 Years, MGS 2024 will be held at the School of Computing and Mathematics, University of Leicester, U.K.

1/

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

The MGS'2024 programme includes

  • Kevin Buzzard (Imperial) as a guest lecturer on the formalisation of mathematics.

  • Thorsten Altenkirch (Nottingham) on category theory.

  • Abishek De and Iris van der Giessen (Birmingham) with an introduction to proof theory.

  • Todd Ambridge (Birmingham) with an introduction to type theory with Agda.

  • Sonia Marin (Birmingham) on session types.

  • Ulrik Buchholtz (Nottingham) on synthetic homotopy theory with HoTT/UF.

  • Reiko Heckel (Leicester) on foundations and applications of graph rewriting.

  • Tom de Jong (Nottingham) on categorical realisability.

Registration is open until 8th March.

2/2

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

I have a cold and a terrible headache and a sore throat. I tested negative for covid. Should I go to work and infect staff and students, or should I work from home?

level98, to random
@level98@mastodon.social avatar

It's easy to understand why people struggle to apply logic, rationality etc. in discussions, when my (essentially) advanced maths students struggle with learning about various proofs.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@level98

This is a tangential comment. In maths departments, students are expected to learn how to prove by osmosis. Nobody tells them what is allowed and what is not allowed in a proof. Teaching them a bit of logic is considered a sacrilege. They just should know logic from birth, full stop.

ProfKinyon, to random
@ProfKinyon@mathstodon.xyz avatar

Having my students compute a quotient group today. I wonder what group it turns out to be? 😁

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@ProfKinyon Sometimes my students solve the Agda exercises by sudoking their way out without really understanding what they are doing. Or more like a video game, because the system is interactive. But I don't mind too much, because once they get used to it, it is easier to explain "what it means", rather than the other way round, it seems.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@ProfKinyon

In fact, I have thought a lot about that, not only with Agda, but with everything I have taught in my career.

Having children helps a bit. It is interesting how they learn to speak! Sometimes they can form the right sentences but you can see that they are not really confident about their "meaning", whatever "meaning" means.

Once they have learned enough words and enough ways of combining them, you can exploit this to explain what the words, or sentences, mean.

I think this happens too with university students. They first need to get used to concepts, and then at a later stage they can "really" understand them (to the extent that "really" makes sense)..

So, in particular, I am against the idea "first teach them the theory, and then use it to get practical results".

Practice comes first from a pedagogical perspective. It is impossible for them to make sense of the theory before they see the practice and get used to it.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

The patch of a spectral locale X has fewer points than X.

This is a quick remark on the patch topology for constructive point-free topologists.

There is a universal way of transforming a spectral locale into a Stone locale, known as the patch construction, which exhibits the category of Stone locales with continuous maps as a coreflective subcategory of that of spectral locales with spectral maps.

Here a continuous map of spectral locales is called spectral if its defining frame homomorphism maps compact opens to compact opens.

In other words, for any spectral locale A there is a Stone locale Patch A and a spectral map ε : Patch A → A such that any spectral map X → A from a Stone locale X factors uniquely through ε.

Now specialize X to the terminal locale 1, whose frame of opens is the object Ω of truth values.

Then the above universal property says that the "spectral points of A", namely spectral maps 1 → A, are in canonical bijection with the points of Patch A, namely the continuous maps 1 → Patch A.

This is interesting because, classically, A and Patch A have the same points.

To see how badly this fails constructively, consider A = 𝕊 = Sierpinski locale.

The frame of opens of the Sierpinski locale, which classifies open sublocales, can be defined in the following two equivalent ways, as is well known:

(1) The free frame on one generator.

(2) The Scott topology of Ω.

Now we have that Patch 𝕊 ≃ 𝟚 := 1+1.

We know that the frame of the locale 𝟚 is simply the powerset of the set 1+1 (which type theorists may write as Fin 2).

The easiest way to see this is to check that the evident map ε : 𝟚 → 𝕊 satisfies the above co-universal property.

1/

joshuagrochow, to random
@joshuagrochow@mathstodon.xyz avatar

Rogers's Equivalence Theorem (https://en.wikipedia.org/wiki/Admissible_numbering#Rogers'_equivalence_theorem) is more amazing than it sounds.

(Plus a question about it at the end)

It says that any two admissible numberings (aka programming languages: https://en.wikipedia.org/wiki/Numbering_(computability_theory)) of the partial computable functions are computably isomorphic.

To see how amazing this is: it's standard that you can write a program to compile Python programs to Java programs and vice versa. Just from those two compilers, Rogers's Equivalence Thm implies that there is a total computable function f that transforms Java programs into input-output-equivalent Python programs that is 1-to-1 (not so surprising) and onto - every Python program arises as f(p) for some Java program p, and p and f(p) compute the same function. That is pretty surprising!

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@andrejbauer @joshuagrochow

I am sceptical of theorems given as exercises. I've found mistakes in e.g. the exercises of the Compendium of Continuous Lattices, and subsequently published a paper with Klaus Keimel fixing the formulation of the exercises, which were wrong claims, and actually proving the fixed versions.

I'd never seen the claim of the above exercise. I won't believe it until I see an actual proof, rather than a claim by an authority, either here or in the published literature.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@andrejbauer @joshuagrochow

So did the compendium, but it was wrong.

MartinEscardo,
@MartinEscardo@mathstodon.xyz avatar

@joshuagrochow @andrejbauer

Nice! Thanks for writing this up. Now I believe the exercise. 🙂

boarders, to random
@boarders@mathstodon.xyz avatar

Idle question: does every infinite set have a bijection with a proper subset without choice?

MartinEscardo, (edited )
@MartinEscardo@mathstodon.xyz avatar

@boarders

"Idle question: does every infinite set have a bijection with a proper subset without choice?"

I am sure somebody here knows the answer.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

So I measured and computed the cost of electricity to run my ebike to commute to work.

I do 8 miles per day, for about 20 days a month.

The ebike charges at 90kwh for less then 3 hours each day.

The cost is less than £2 per month, or $2.50 USD. I am surprised.

MartinEscardo, to random
@MartinEscardo@mathstodon.xyz avatar

Some formal systems, such as ZFC, MLTT, CZF, CoC, HoTT/UF, and many more, are sometimes proposed as "foundations" of mathematics.

But the truth is that, in order to be able to both conceive and write down any of the above formal systems, one already has to know a lot of mathematics.

And the same is the case to be able to understand, use and accept/reject any of them, when they are presented to you.

Mathematics comes before any of the formalisms proposed to regulate it.

In fact, in my view, foundational systems, in their proliferation, only barely manage to catch-up with what people are already doing in mathematics, ignoring them.

But I still think they are very useful. They describe possible mathematical worlds that we may contemplate and explore, with possible ways of exploring them.

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