fairly confident i came up with a viable strategy to fix cubical agda's awful handling of interaction metas... fingers crossed

had this half-formed thought yesterday that induction on derivation trees is hard because it expresses initiality of the category of contexts (of your theory) in a (higher?) category of models (of your theory), and that's why it's hard. thoughts?

i'm so glad i never think about syntax anymore

Amy boosted

Löb induction is when I lob the induction hypothesis across the room

this is a subtoot of like two things at once. one of them is *me*. i've gotta stop talking to jon

Show thread

logical relations? that's when you glue along the global sections functor, right?

Amy boosted

me: ah yes, it's so cold that my fingertips are tinted blue.

my diet coca cola addiction: time for a cold drink

cubical without glue thats like [two things which are inseparable]

syntax? is that like an initial lccc?

constructing a right adjoint to f^* from cartesian closure of all slices... "fun"

You know when you have little a problem, then you say "eh, I'll deal with it later", then suddenly it's "later" and the problem is now a massive problem

github.com/plt-amy/1lab/issues

announcement (boosts appreciated) 

We're delighted to announce the HoTTEST Summer School, which will take place online everywhere in the world during the months of July and August 2022.

The school will run both synchronously and asynchronously. The lectures will be delivered live (between 2:30-4pm UTC) and paired with various tutorial sessions run by teaching assistants. The course will also feature a discord-based all-hours Q&A and an online archive of all course materials so that participants can follow along on their own schedule.

This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory. Our goal is to make homotopy type theory accessible to, and inclusive of, everyone who is interested, regardless of cultural background, age, ability, formal education, ethnicity, gender identity, or expression. We believe HoTT is for everyone, and are committed to fostering a kind, inclusive environment.

Read more: groups.google.com/g/homotopyty
Join the Discord: discord.gg/tkhJ9zCGs9

we're at 39785 lines of prose+code, 17k of just code

think im gonna do ends tomorrow. also remember when i said i'd do an easy theorem today instead of thinking too hard? i ended up writing ~1000 lines about abelian categories. woops

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.