I'm watching a CPP talk and, why are so many of the videos in the sidebar Christian church videos

CPP 2021

Lean's core type theory only has eliminators 👀 I didn't know any of the proof assistants actually did that

re: CPP 2021

omg Lean 4 is implemented in Lean 4 👀 Haskell is to Idris as OCaml is to Lean...

re: CPP 2021

@vdash you've heard of locally-nameless, get ready for popl21.sigplan.org/details/CPP anti-locally-nameless

re: CPP 2021

I remember seeing somewhere else that 𝒫(X) := X → ℙ represents powersets in type theory with impredicative ℙrop but I don't remember the reasoning anymore

re: CPP 2021

Does it have to be an impredicative ℙ? Can it be a definitionally proof-irrelevant ℙ? Or even a Type in general?

re: CPP 2021

I did it myself here and I no longer remember how I convinced myself of the fact (if I did at all)

re: CPP 2021

This is only somewhat related to the talk on category theory in Agda but sometimes I get the impression that there's a lot of proofs where people will be like "oh this relies on axiom K and proof irrelevance and blah blah blah" as an argument for why the proof is ungood but to me this feels more like an argument for why more type theories should have such axioms etc. (or at least the possibility to enable them)
There was probably a design decision somewhere to use those axioms because it simplified proofs etc. which means they were helpful in making proofs easier to write and understand
There's a lot of the "what's the smallest set of axioms we can work off of" that I feel like comes from set theory and it's a valid desire but adding justifiable, intuitive, and consistent (ofc) axioms should be just as valid for practical purposes

re: CPP 2021

This is just a longwinded way of saying tbh

re: CPP 2021

How strange, there doesn't seem to be any cubical talks in CPP this year
No tori as the product of two circles this year, alas

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