Pinned toot

$\mathcal{things ~ are ~ just ~ other ~ things}$

Pinned toot

✨ 𝓲𝓽 𝓲𝓼 𝓪𝓵𝔀𝓪𝔂𝓼 𝓪𝓵𝓵 𝓽𝓱𝓮 𝓽𝔂𝓹𝓮𝓼 ✨

Pinned toot

"Computers are rocks we tricked into thinking" is entirely incorrect. Computers are rocks we tricked ourselves into believing they could think

XTT 

This only has 2D composition (bc paths are equal, so there's no extra structure) but already I struggle

Show thread

QXTT (quantitative cubical type theory for bishop sets)

Show thread

XTT 

It should be like code(bool) : set or smth right
Why aren't they in here

Show thread

XTT 

Wait there's formation rules for the set universe and what looks like an elimination rule but there's no... introduction rule...

Show thread

XTT 

Idk if face formulae can have a disjunction where both sides hold but if they can then partial elements reduce nondeterministically

Show thread

XTT 

The computation rule says all of that, no need to stick it in the types, if that's what it's actually doing

Show thread

XTT 

I dont get how this judgemental restriction works
Or how partial elements work
Like it feels like a departure from the usual cubical where you have just intervals and paths and you apply paths to intervals and that's that
The type of the eliminator for paths (applications) is a judgemental restriction to a partial element under the boundary of the applied interval element that is one end when the element is 0 and the other end when it's 1
And like, why

Show thread

I don't remember why I was reading XTT Friday night but I guess I'm continuing

I wonder how cubical agda is implemented
With rewrite rules around I don't think it would be difficult to make path types and coercions compute on the interval elements

Show thread

It's perfect. Idris already has typecase and axiom K, it's a natural fit
Idris is all about computing and dependently-typed programming and stuff rather than mathematics and proofs and guess what? XTT is good for that too
Presumably, I'm just repeating what the conclusion says I haven't personally verified this lol

Show thread

I didn't realize handin is a Racket package
tbh I always thought it was a collection of scripts or smth like it always is

Do screen readers read content from CSS ::after properly?

Filing my contribution to my lab's snack fund under "charity" in my double ledger

I somehow broke my installation of CoqIDE and had to install lablgtk3

Show older
types.pl

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