Ancestors

Written by julesh on 2025-01-27 at 19:54

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

=> View attached media

=> More informations about this toot | More toots from julesh@mathstodon.xyz

Written by Joey Eremondi on 2025-01-27 at 21:20

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

=> More informations about this toot | More toots from joey@mathstodon.xyz

Written by julesh on 2025-01-27 at 21:23

@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

=> More informations about this toot | More toots from julesh@mathstodon.xyz

Written by Tito on 2025-01-27 at 22:12

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

=> More informations about this toot | More toots from tito@sciences.re

Toot

Written by julesh on 2025-01-27 at 22:13

@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)

=> More informations about this toot | More toots from julesh@mathstodon.xyz

Descendants

Written by Tito on 2025-01-27 at 22:51

@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

=> More informations about this toot | More toots from tito@sciences.re