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

CTT (cringe type theory)

XTT

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

QXTT (quantitative cubical type theory for bishop sets)

XTT

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

XTT

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

XTT

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

XTT

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

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

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

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

Idris but it's XTT underneath

Cubical Idris

Semaphore? I hardly know 'er

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

oh it does! very neat

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

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

pwoofs and pwogwams uwu

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

Show older

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