Marcelo Fiore is engaging in an experiment: how many times can you formulate the wish for inductive families in the presheaf category before @pigworker materialises in the room.

· · Web · 1 · 0 · 3

@gallais The answer would be different, were I not half a sleep and under a ton of marking. Is this talk being recorded?

@pigworker I don't think so. It's based on but during the talk Marcelo has been really emphasising the tension between the mathematics done in CT and the encoding in proof assistants.

@gallais @pigworker Too bad it wasn't recorded - I would have like to have heard that.

@JacquesC2 @pigworker Next SPLS should be in October & you'll be around so I guess we could think of inviting Marcelo.

Sign in to participate in the conversation
La Quadrature du Net - Mastodon - Media Fédéré est un serveur Mastodon francophone, géré par La Quadrature du Net.