@boarders@mathstodon.xyz
@boarders@mathstodon.xyz avatar

boarders

@boarders@mathstodon.xyz

Interested in mathematics (homotopy theory, category theory, topos theory), programming languages and philosophy

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

mevenlennonbertrand, to random
@mevenlennonbertrand@lipn.info avatar

I just realised that inductively defining an indexed inductive family T : B -> Type and then quotienting each T x by a family of relations R : Π x : B, T x -> T x -> Type is not the same as the corresponding quotient inductive type: if R is not a congruence, then the quotient-after-the-fact is not right, because it does not know that you also want to quotient the other fibers by their relation.

Is this the whole point of QITs that had completely gone over my head until now?

boarders,
@boarders@mathstodon.xyz avatar

@mevenlennonbertrand yes! If you do raw syntax quotiented by beta/eta then that is not the same as the QIT with these equalities

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling @mevenlennonbertrand that is what I meant and actually I had in mind the situation of the syntactic category of a dep type theory where you must quotient all things together (contexts, types and terms) and you can’t add in congruence after the fact (maybe that’s technically wrong but adding it in after the fact is beyond brutal)

boarders, to random
@boarders@mathstodon.xyz avatar

I think “active learning”/“student-centred learning” and other new ideas for how university teaching might work are great. A model for learning based too much around “propositional knowledge” and too little around capacities and practices leaves us in the same decrepit situation as analytic philosophy’s view of epistemology (“justified true belief”). It is slightly sobering however that the gold standard of a “flipped classroom” is how high school mathematics works, and I don’t think many people would view that as any kind of ideal of education, to say the least

ltratt, to random
@ltratt@mastodon.social avatar

One thing I think about a lot is "how much time should this organisation spend making tools to help with its main software tasks?" Experience has taught me that most invest far too little in this, but I've struggled to find a good way of defining what "too much" might look like.

boarders,
@boarders@mathstodon.xyz avatar

@ltratt in the context of CI then I would say too much is indicative of situation where CI is far too slow and has enough false positives to create distrust

boarders, to random
@boarders@mathstodon.xyz avatar

https://www.experimental-history.com/p/how-to-get-7th-graders-to-smoke

"You cannot plonk someone in front of a computer screen for an hour and expect them to become a better person. Well-meaning researchers have tried way, way harder than that and gotten way, way less."

shwestrick, to random
@shwestrick@discuss.systems avatar

Very excited to announce that I will be starting in September as an assistant professor of computer science at NYU!

Can't wait to move to New York this summer!

boarders,
@boarders@mathstodon.xyz avatar

@shwestrick if you want to grab a coffee some time once you’re here and talk about PL/type theory/mathematics/etc. then I’d be more than happy to do that

boarders,
@boarders@mathstodon.xyz avatar

@shwestrick great, I’ll reach out with a DM later on

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

I think the reason so many "personal knowledge management" products are starting to integrate LLMs might be that many people who “use” these things (or try to be influencers in this area) really have filled them with the kind of content that could be generated by LLMs. And it seems plausible to me that a chat session with one of those LLMs might be kind of similar to a chat session with a happy user of such tools — utterly devoid of intellectual content and just saturated with vapidity.

If you look in these people's knowledge bases, it's all meta-crap about success and business and knowledge or something, without any actual area of practice. In the end, people get sold on a hopeless get smart quick scheme.

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling always taken aback by how far one can get (e.g. one can have a sensible conversation with a researcher or graduate student in a given area) on almost any topic simply by properly reading one or two more technical/serious books over the course of a few months or year (important that doing this is simple, but it is not easy) - no one wants to hear the boring answer for how to progress at many things is “iterative deepening”

To quote one of the original AI people (from this excellent essay: https://www.norvig.com/21-days.html)

“So go ahead and buy that Java/Ruby/Javascript/PHP book; you'll probably get some use out of it. But you won't change your life, or your real overall expertise as a programmer in 24 hours or 21 days. How about working hard to continually improve over 24 months? Well, now you're starting to get somewhere...”

julesh, to random
@julesh@mathstodon.xyz avatar

Obviously not everything can be understood with just category theory, although I'm starting to kinda suspect that everything can be understood with a mixture of category theory and statistical physics

boarders,
@boarders@mathstodon.xyz avatar

@julesh statics + dynamics

marioguzman, to random
@marioguzman@mastodon.social avatar

Ooooof 🥵 the new iPad Pro is hot! It is noticeably thinner and feels much nicer. But at the end of the day, I really just want the new Magic Keyboard with the Function Keys row. The OLED is alright. Just wanting the keyboard is not enough to justify my configuration of $2,000. Maybe in a couple months when discounts go online at other retailers. Pretty solid & very refined iPad.

I will say the keyboards give me that cheap, Amazon-sold wannabe Apple Magic Keyboards though. Just a vibe though.

boarders,
@boarders@mathstodon.xyz avatar

@marioguzman I do really like the iPad, but the closed garden nature of it is so rough that I am reluctant to put more money into it - for example, the best epub reader app has been broken by OS updates and the maintainer seems to have abandoned it - in the app ecosystem that just means it never gets fixed since they don’t seem to care about backwards compatibility

carapace, to random
@carapace@mastodon.social avatar

1/7

I love science, so it's strange and frustrating that healing modalities with which I have personal experience (including Reiki, Feldenkrais, NLP, EFT, hypnosis, and others) are "unreproducible" by mainstream scientists, to put it mildly.

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

@carapace I do think science, especially as typified by “double blind studies” and in the realm of medical knowledge, can be a flawed methodology (the biggest cause of mental health is poverty, but that is too messy to causal stories about brain chemistry), however I don’t take much credence from someone saying they know something from personal experience (since people say this about astrology or other gibberish) - we are easily able to fool ourselves with fake causality and randomness (for instance, see all of the people telling you that CEOs wake up early so it must lead to success)

That said, I think it is also the case that some things are simply not easily subject to quantitative measure - how could we scientifically measure the impact of reading Dickens, perhaps one would do better on a reading comprehension exam, but one would hope what a person gets from it is far beyond that

antidote, to random
@antidote@mathstodon.xyz avatar

Everything I do academically is some combination of:

  • tiny to the point of unpublishability;
  • for someone else and not relevant to anything I’m doing;
  • wholly incorrect;
  • treading on someone’s toes.

Is it time to throw in the towel?

boarders,
@boarders@mathstodon.xyz avatar

@antidote [not in a place to offer advice as I quit academia after not getting far] a PhD, postdoc, professorship etc. is not worth hating yourself over, it’s the number one truth of academia that no one will say - none of this is worth despising who you are or what you have to offer

Moreover, the important thing to do now is to cultivate your own taste and your own sense of what is valuable - start writing up the “unpublishable results” and I bet you’ll see how once you flesh everything out and expand all the natural examples explaining what you have, it becomes a fully publishable result and one you can be happy with

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.

boarders,
@boarders@mathstodon.xyz avatar

@MartinEscardo this is a definition of categories as monads in the bicategory of spans using some specific choice of construction of pullback in Set, but it is naturally a weak 2-category - so we should state it for pullbacks, but then we can’t even state the associativity law as it is a naturally a dependent equality (unless we use some kind of unbiased pullbacks)

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

Thinking about how to teach students about isomorphisms (between sets).

It is easy to teach them about bijection (injective + surjective): you can give an example about checking that two piles are equinumerous, and walk through how you want to match each widget from one pile with one from the other without leaving any left over.

But isomorphism (in the sense of left and right inverse) is somehow much more abstract and hard to think about for someone who doesn't already get it.

Have any of you got a successful way to teach this concept without first introducing bijection?

boarders,
@boarders@mathstodon.xyz avatar

@jonmsterling some ideas but not fleshed out to usable slogans:

  • draw a function via its cograph, that is the formalization of “potato diagrams”, where we have a set A on the left, a set B on the right and an edge from any element a to where it is sent. From this we can take the mirror image diagram (reverse all edges) and ask if this is a function - the inverse function

  • draw the graph of a function and consider the reflection in the diagonal (lots of people will be used to this idea as log is the “mirror image” relation of exp or sqrt and square functions etc.) - this relation may also be functional, and is the inverse

  • more speculative: the ur-family of isomorphisms arise from the first isomorphism theorem of sets, a set quotiented by the kernel pair equiv relation is iso to the image is iso to the equalizer of the cokernel pair. I feel like there must be some way to make this idea palatable to get a deeper perspective e.g. this describes the iso between Z/nZ and [n], but this is notoriously hard to get across in an intro course

boarders, to random
@boarders@mathstodon.xyz avatar

Moderately interesting (to me!) that in mathematics a magma is basically a useless idea that you wouldn’t even define in an undergraduate degree, but the typed analog - an applicative structure - is a very useful starting point for realizability, semantics of type theory / HOL etc.

j2kun, to random
@j2kun@mathstodon.xyz avatar

Now that I have a static site with hugo, I wonder if people would like reading shorter-form thoughts, and they can be cordoned off into their own part of the site and/or their own RSS feed.

I feel like there are a lot of small mathematical tidbits I learn about that I don't have the time/energy to put into a proper article, but are still worth spreading.

boarders,
@boarders@mathstodon.xyz avatar

@j2kun please do, often at work I have a short period of time (compiling, waiting for CI etc.) in which it is great to have a supply of shorter form thoughts that are not social media or news (both of which I’d often prefer to avoid viewing in an unrestrained way) - this probably used to be fulfilled by webcomics

jonmsterling, to random
@jonmsterling@mathstodon.xyz avatar

Ultimately we have to ask ourselves if it was overall a good thing that computer science as a discipline ceased to be part of mathematics — rather than broadening the horizons of mathematics and bridging the gap between mathematics and social science. I am not speaking purely rhetorically, as there are legitimate arguments to be made on both sides.

boarders,
@boarders@mathstodon.xyz avatar

@antoinechambertloir @jonmsterling
Can't resist this immortal Girard quote:
"Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in the area obeys a kind of “wedding cake” paradigm: for instance language design is reminiscent of Ptolomeic astronomy — forever in need of further corrections. There are, however, some limited topics such as complexity theory and denotational semantics which are relatively free from this criticism.

In such a situation, methodological remarks are extremely important, since we have to see methodology as strategy and concrete results as of a tactical nature."

boarders,
@boarders@mathstodon.xyz avatar

@sprout @antoinechambertloir @jonmsterling I can’t say it looks from the outside like computer science is drowning in mathematicians or mathematical input. More generally, no field has ever done well out of limiting its mathematical analysis. Einstein famously came to accept this fact as a result of Weyl, and it led to our best formulation of general relativity as being about free particles following geodesics on a Lorentzian manifold which we could now teach to undergrads if we had professors that weren’t scared of mathematics

boarders,
@boarders@mathstodon.xyz avatar

@sprout @antoinechambertloir @jonmsterling John Von Neumann, Alan Turing, and Alonzo Church - three mathematicians - created computer science, maybe cool it a little on who is worthy

boarders, to random
@boarders@mathstodon.xyz avatar

So many aspects of current culture are simply different versions of: “lottery winner endorses lottery as path to success”

julesh, to random
@julesh@mathstodon.xyz avatar

Please can somebody inform MS Word that the accusative form of "who" is "who" in modern English, it's not 1924 anymore and I'm not writing in German

boarders,
@boarders@mathstodon.xyz avatar

@julesh @jer_gib also why stop here? why not use ‘thou’ and ‘thee’ if we don’t care about language as speakers actually speak it, but merely about pretending modern English is Latin

julesh, to random
@julesh@mathstodon.xyz avatar

Someone should write "mathematics for the working category theorist", to teach a bit of algebraic topology to those of us who started out in functional programming

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

@julesh Peter May already wrote two volumes of this book (‘a concise course in algebraic topology’ and ‘more concise algebraic topology’)

boarders,
@boarders@mathstodon.xyz avatar

@brokenix @julesh use a search engine

counting_is_hard, to random
@counting_is_hard@mathstodon.xyz avatar

Time to write the code: 5 minutes.
Time to figure out the types: 50 minutes.

boarders,
@boarders@mathstodon.xyz avatar

@counting_is_hard makes sense. My python experience is indeed:
Time to write code: 5 mins
Time to add types to code: 50 minutes
Time to get out that last buggy behaviour: tbd

Joemoeller, to random
@Joemoeller@mathstodon.xyz avatar

This summer I'm starting a postdoc at CalTech! I'm working with the roboticist/control theorist Aaron Ames on using category theory to study stability of dynamical systems.

I got verbal confirmation a month ago, but I've been holding back on saying anything until I got bureaucratic confirmation.

boarders,
@boarders@mathstodon.xyz avatar

@Joemoeller congrats, I hope it’ll allow for writing “control theory for category theorists” instead of the converse which is more usual :)

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