Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!

Administered by:

Server stats:

2.9K
active users

mathstodon.xyz: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

Public
julesh

I'm doing the MSP101 seminar next monday. Here is my abstract... I'm very excited to finally be talking about dependent optics!

Title: We solved dependent optics! Abstract: There are two major generalisations of lenses. First there are optics, which require almost nothing of their base category and give you something in return. And then there are dependent lenses (aka container morphisms, aka natural transformations of polynomials), which require a lot of their base category but give you even more in return. One day several years ago I innocently twote the question of how to unify these two constructions, which is motivated for mathematical, computational and sociological reasons. The problem ended up occupying us (joint work with Dylan Braithwaite, Matteo Capucci, Bruno Gavranović, Eigil Rischel and André Videla) for several years, and its difficulty became a meme. I will explain the answer that finally satisfied us. This involves first constructing a category of "dependent adaptors" and then freely adjoining a particular family of monoidal costates using a technique we call "weighted coparametrisation" that we reinvented. The definition began life as a prototype in Idris using QTT features, and was then translated back into category theory using what might or might not be a novel semantics of polymorphic dependent type theory.
🇨🇦 Joey Eremondi

@julesh What is polymorphic dependent types theory? One with a universe?

Jan 27, 2025, 09:20 PM·Public·Elk
1boost·1favorite
Public *
julesh

@joey What I actually mean by it is the (0, infinity) fragment of QTT. I have no idea yet how that relates to the thing that is called polymorphic dependent type theory, which for example is the title of one of the later chapters in Jacobs' categorical logic book

Public
Tito

@julesh @joey In that book "polymorphic type theory" just means System F or Fω. Type dependency is treated in later chapters

Public
julesh

@tito @joey Sorry yes, I meant to say "polymorphic dependent type theory". It's one of the last chapters in the book (and it has prerequesites on multiple earlier chapters that I already can't understand)

Public
Tito

@julesh @joey Hm, I have to confess I never read that last chapter until now, but judging from its intro the scope includes the Calculus of Constructions

SearchLive feeds
About