@antidote@mathstodon.xyz
@antidote@mathstodon.xyz avatar

antidote

@antidote@mathstodon.xyz

Reading for DPhil Computer Science @ University of Oxford, UK. Interested in category theory, type theory and foundations.

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

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?

ColinTheMathmo, to random
@ColinTheMathmo@mathstodon.xyz avatar

Which letter in 'Scent' is silent? The 'S'? Or the 'C'?

antidote,
@antidote@mathstodon.xyz avatar

@ColinTheMathmo it depends on the scent in question: a good perfume is worth every (s)cent, whilst any unpleasant stink must be s(c)ent away and cleaned.

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

I may buy a flat in Edinburgh! The one remaining obstacle is that the wooden beams in the attic feel wet to me. But we hired a roof inspection company and they wrote:

"staining to timber trusses inside of attic space in our opinion have been historical and rectified with previous repairs, no signs of new water ingress at time of roof report."

which contradicts my impression. I have to talk to them.

But here's my question for you, good citizens of Mastodon. The report also says:

"Main felt wall head gutter was found to be in good condition along with inner felt roof but with a limited life span a full overhaul/replacement should be anticipated within 7 - 10 years (ref pictures 2, 3, 4, 5 & 8 )".

What is a "main felt wall head gutter"? Here is one of those pictures.

Regarding the "felt", here's one thing the inspectors wrote:

ROOF DESCRIPTION

Timber trusses with sarking boarded roof deck. Slatted panels with under slating felt consisting of original horse hair, 3B felt or similar, cast iron rainwater goods, traditional stone built and brick. Chimneys which some have been rendered. lead & zinc channels to chimney surrounds, flat torch on felt inner roof area with outlet surrounded by slatted panels, torch on felt wall head gutter.

antidote,
@antidote@mathstodon.xyz avatar

@johncarlosbaez it’s the flat quadrilateral in the middle with the hole in it

(The material is https://en.m.wikipedia.org/wiki/Bituminous_waterproofing)

antidote, to random
@antidote@mathstodon.xyz avatar

The key insight underpinning the Curry-Howard correspondence is that both mathematics and programming sit on a common foundation of people being pathologically incapable of naming things appropriately

julesh, to random
@julesh@mathstodon.xyz avatar

What the heck is really going on with foldl and foldr?

The first take is that folding is about the universal map from a free monoid (ie. lists) to some other monoid. That says you can fold something that's (1) a binary operation on a single set, (2) unital on both sides, and (3) associative, aka a monoid. In that case foldl and foldr are different implementations of the same function

I think the next step of abstraction is that foldl and foldr deal with left and right monoid actions (or possibly the other way round), which gives up (1), and weakens (2) and (3) while keeping them morally intact

But, like, foldl and foldr appear to work perfectly well with no associativity whatsoever. It doesn't even feel like a programming hack to me - left-folding or right-folding a non-associative operation over terms of a free monoid feels to me like a perfectly reasonable thing to do mathematically speaking. But I have no idea whether they have universal properties or if it's just a thing

I idly wonder, if you go from monoids to commutative monoids, ie. from lists to finite multisets, what happens to foldl and foldr? Intuitively I feel like left and right folds are no longer well defined, but why would imposing commutativity suddenly also require associativity as well?

antidote,
@antidote@mathstodon.xyz avatar

@julesh when using a non-associative operation, you’re folding in a magma. Really, you should be passing trees as input and folding these. When you restrict to lists, you’re only looking at a fragment of the expressible folds.

Two trees having the same leaves in the same order doesn’t guarantee that they’re going to fold to give the same answer unless the magma you’re looking at happens to be a monoid. However, if you reduce your tree to a list and then pretend it’s a tree and fold you will always get the same answer. In fact, if I have any chosen representation of the free monoid, I can interpret a tree there and then fold. The answer I get from my fold will therefore agree for any two trees (with the same leaves in the same order), but might differ based on my chosen representation of the free monoid.

The exact same situation happens when looking at commutative monoids except it’s even more obvious because now my chosen representation depends on a chosen ordering of the leaves of the tree and the answer I get is not invariant under these orderings!

christianp, to random
@christianp@mathstodon.xyz avatar

Huge sunk cost fallacy as I've spent all day hand-drawing every mathematical symbol in unicode, and even though my handwriting isn't very good I pretty much have to finish this t-shirt

antidote,
@antidote@mathstodon.xyz avatar

@christianp this is outrageously cool

julesh, to random
@julesh@mathstodon.xyz avatar

In our work on dependent optics we're following an idea of @bgavran that there's an extra hidden dimension: dependent lenses = morphisms of containers = natural transformations of polynomial functors are secretly connected components with respect to a lower dimension, and revealing it is very useful. But I was also just reminded by @zanzi that the 0-cells of this category are really functors so there's also another dimension upwards. This category is naturally 4-dimensional !!! 😰

antidote,
@antidote@mathstodon.xyz avatar

@zanzi @julesh @johncarlosbaez @bgavran there are weak tri-categories that are not tri-equivalent to any strict tri-category—strictification at dimension >2 is not possible in general and exciting when it is for any particular example!

ColinTheMathmo, to random
@ColinTheMathmo@mathstodon.xyz avatar

I don't expect anyone to be able to answer this, but someone I follow elsewhere says:

This is a simple lemma in my field, but I can't find a reference to a proof. I'd like to quote it ... can anyone point me at a place where it's proved?

"When Γ |- A,B : Type are two types in a category with families with base category S, then there is a natural bijection between
(a) terms Γ.A |- N : B[p_A]
(b) maps p_A -> p_B in the slice S/Γ.
p_A is the display map of A."

Does anyone know of a proof of this in the literature?

Assistance welcome ... boosts would be helpful to get this to travel to people who might be able to answer it.

Many thanks in advance.

antidote,
@antidote@mathstodon.xyz avatar

@ColinTheMathmo the intermediate step is to prove that there’s a natural bijection between terms Γ |- N : A and sections of p_A. Crucially: a section of p_A is a morphism from id_ Γ to p_A in the slice S/Γ. (This is a direct application of the UMP of Γ.A.)

Once you have this, a term Γ.A |- N : B[p_A] is a section of the display map p_A*(p_B) : Γ.A.B[p_A] -> Γ,A. Thus we have a morphism id_{Γ.A} -> p_A*(p_B) in the slice S/Γ.A. Changing base via p_A, we get the the required map p_A -> p_B in S/Γ (and vice versa).

BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

This is the conclusion of my upcoming blog post.

antidote,
@antidote@mathstodon.xyz avatar

@boarders @BartoszMilewski @dimsumthinking I don’t talk about it often, but I implemented the graphics pipeline for beta.homotopy.io. The image is a rendering of the 2-manifold diagram representing the associator.

While I don’t think this tool is particularly helpful as a ‘proof assistant’, I love using it to visualise my mathematics.

antidote,
@antidote@mathstodon.xyz avatar

@boarders @BartoszMilewski @dimsumthinking Even better: a rendering of the 3-manifold diagram representing the pentagon, sliced as an animation.

video/mp4

BartoszMilewski, to random
@BartoszMilewski@mathstodon.xyz avatar

So now I'm convinced that not every endofunctor in a CCC is self-enriched and, consequently, strong. So why are Haskell functors strong? What's the secret spice?

antidote,
@antidote@mathstodon.xyz avatar

@BartoszMilewski @MartinEscardo the type of fmap tells you that F is self-enriched

(Read the arrows as internal homs)

antidote,
@antidote@mathstodon.xyz avatar

@zanzi @BartoszMilewski @MartinEscardo I think you’re talking at cross purposes. The category of Haskell types is self-enriched so the global elements of the internal hom and the external hom are isomorphic. The issue that arose originally was a question of definability, not of the semantic interpretation of the arrow.

antidote,
@antidote@mathstodon.xyz avatar

@zanzi @BartoszMilewski @MartinEscardo
hom(1, [A,B]) ~ hom(A x 1, B) ~ hom(A, B)

Adding an extra piece of syntax to quantify over hom(A, B) is implicitly quantifying over hom(1, [A, B]). You’ve not gained the ability to talk about anything you couldn’t talk about before.

The problem boils down to the fact that whatever way you try to notate (a -> b) -> (F a -> F b), it can still be read as an element of hom(1, [[a, b], [F a, F b]]), all of which are definable.

Definability breaks when you have an arbitrary function (i.e., in your ambient mathematics) hom(a, b) -> hom(F a, F b), adding notation for hom still doesn’t let you write down a type corresponding to these

antidote,
@antidote@mathstodon.xyz avatar

@zanzi @BartoszMilewski @MartinEscardo (I was referring to your earlier point about trying to incorporate non-strong functors in Haskell by adding syntax for the external hom)

antidote,
@antidote@mathstodon.xyz avatar

@zanzi @BartoszMilewski @MartinEscardo I may have misread your message but I read it as saying that by separating notation for internal and external hom, we’d be able to use types to distinguish internally definable (necessarily strong) functors from more general functors. I was just trying to explain why you can’t do this sort of thing without a two-level type theory or similar ambient mathematical meta-language. The strength transports across the isomorphism I was talking about.

antidote, to climate
@antidote@mathstodon.xyz avatar

I really want to not eat meat; travel less and produce less waste, but every time I’m offered the choice in everyday life, it’s always too easy to do what I’ve always done. I want to vote for a government who will be the ‘grown up’ and tax all of my bad habits into oblivion, but major parties seem to think that I’d hate that — I really wouldn’t.

julesh, to random
@julesh@mathstodon.xyz avatar

"No, the Yoneda lemma doesn't solve the problem of qualia" by @mc
https://matteocapucci.wordpress.com/2023/07/15/no-the-yoneda-lemma-doesnt-solve-the-problem-of-qualia/

antidote,
@antidote@mathstodon.xyz avatar

@johncarlosbaez @julesh

antidote, to random
@antidote@mathstodon.xyz avatar

My parents’ faces for the brief moment they thought I’d spent ~£500 on books of illustrations of a safari animal almost justify the expense ✍️🐘

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