­jonoodle­ @ionchy@types.pl

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

CTT (cringe type theory)

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)

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

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

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

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

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

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