oh my god it's a typo. it's supposed to be a cdot, not a .

The name is pretty funny though. because it's represented by a type, haha get it

A cwf is democratic provided each context Γ is represented by a type Γ in the sense that there is an isomorphism γ_Γ : Γ ≃ 1.Γ̅

what is. what's this 1. notation. pleas

From the definition of ucwf it is immediately clear that an
initial ucwf Tucwf can be generated inductively

no it's not! show me!

And I thought I was extra pretentious about ice cream in listing places that serve single scoops over 6$OH about a restaurant I'm like oh East is East is a little pricey but I would go time to time and it's totally worth it to me. But 75$ for dinner????

no

"It was 75$a head" "Oh! That's doable" 75$??????

Tired: de Bruijn indices
Wired: whatever this is

presheaves have a universal property whose statement I can't read so I'm going to ignore it until they bring it up

Like at this point if you're saying things like "D-valued presheaf over C" you can just say a contravariant functor from C to D
I'm guessing D is typically Set but in a cwf it's Fam instead so clearly it can be other categories that aren't Set-like

Is a presheaf just a contravariant functor or are there additional properties I can assume that they haven't mentioned here beyond the functor

a key feature of the notion of cwf is
that it can be presented as a generalized algebraic theory

you're really gonna make me learn One More Thing huh

Waking up tired disease. Dependency on coffee disorder

Why am I so tired all the time

I hate the AC so much it's so cold all the time

I've already been yelled at by two people on the street I've had enough of the day

I'm so tired

I'm gonna be freezing in the lab

I left my hoodie at home
Do I go back to get it? I'm literally halfway to campus

literal quote from Haskell bytestring package documentation

# Deprecated and unmentionable

accursedUnutterablePerformIO :: IO a -> a

This "function" has a superficial similarity to unsafePerformIO but it is in fact a malevolent agent of chaos. It unpicks the seams of reality (and the IO monad) so that the normal rules no longer apply. It lulls you into thinking it is reasonable, but when you are not looking it stabs you in the back and aliases all of your mutable buffers. The carcass of many a seasoned Haskell programmer lie strewn at its feet.

Witness the trail of destruction:

Do not talk about "safe"! You do not know what is safe!

Yield not to its blasphemous call! Flee traveller! Flee or you will be corrupted and devoured!

Show older

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