Pinned toot

I would like to emphasize to everyone that I understand literally nothing and none of my word can be taken as authority on anything

thank you

Pinned toot

This message was sent from a non-IU address. Please exercise caution when clicking links or opening attachments from external sources.

Pinned toot
Pinned toot

reposting this from old account so I can pin it

Pinned toot

welcome to PL mastodon we have
- nobody

advent of code time. i am not ready but i will do it

my patience for people putting parentheses on their own line while writing lisp is at its end

hazel :ms_asleep: boosted

*points at you*

you are the cyclic group of order 2. there is nothing you can do

email protip: filter the word "Unsubscribe"

thanksgiving is a holiday meant to mask the US's horrid treatment of indigenous people. if we truly wished to give thanks we would give them their land back.

the cats are smelling each other. this is getting out of hand

Show thread

im in the cat room. there are cats

hazel :ms_asleep: boosted

that feel when you ..uh . y ou fucking. you fucking uh. you Set (A.ℓ ⊔ B.ℓ₁) != Set B.ℓ₁

squimsh : A ≡ A → A ≐ A
squimsh refl = refl

I have learned that doing any mathematics in type theory requires you to be a genius

this is either a post about politics or about type theory. up to you

Show thread

*slams desk* WHY IS EQUALITY SO COMPLICATED

I wish I could teach Agda to feel my suffering

that feel when you. uh . y ou fucking. you fucking uh. you

Coset : ∀ {ℓ} {T : Set ℓ} {S : NonemptySubset T} (G : Group T) (H : Subgroup G S) → Set ℓ
Coset G H = CosetRel G H // coset-~
Show older

hazel :ms_asleep:'s choices:

types.pl

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