time to draw some category theory diagrams. I wonder how I'm supposed to do this when none of the types are written down... you're saying I need to derive them myself? smh

feeling bad about not doing the intro type theory exercises despite likely already knowing everything in them

It's like 1984, type theory is like newspeak: you can't say anything evil

When lowercase f is used for both the functor/type and a function: kill kill kill die die die

Using out for both the constructor "on paper" and the destructor "in Haskell": die die die die

Doing functors in "category theory" but then doing bifunctors in "Haskell": kill kill kill kill

This bifunctor stuff is confusing me so much. Can we go back to functors

Why use Bifunctor instead of like.
Okay so we want that Mu f is a functor so f needs to be a Bifunctor bc f is a Functor in its second argument
But you could just say that (\x. Mu (f x)) is a functor instead

I'm thinking of (after all the lectures are over) rewriting all of my notes with notation that I prefer (and that is consistent throughout!) bc this material is really interesting but just so confusing when mixed with Haskell's limitations on names

It bothers me that all this machinery is set up to use bifunctors but you only ever bimap id over the first type and the only time it's useful is to make the fixed point of the bifunctor a functor

I bet later on we'll do something more interesting than merely id... but I don't see it yet

Wait a minute. If there exists a unique x such that P(x) and I can show that P(y) for some y, then x = y right
I was so caught up in the category theory I forgot how logic works

I still can't sleep properly and I feel like I'm racking up a sleep debt that will get me in week 2

Every time I see "NilF" — you know, the empty constructor for the functor whose fixpoint generates lists — I read it like "dilf" in my head

Nullary list I'd like to functor

Debating whether this one is going on Twitter

I need a lil screenshot for context... and I think it'll work

Hmm usual type theory is a mix of natural deduction and sequent calculus
Does it have a name

First positive covid of the summer school... it was a lecturer 😳

"Agda checks that I only do reasonable recursion" size-preserving recursion is reasonable 😤

ordinals ❤️

ngl despite knowing formally how guardedness for coinductive types works it's rather challenging to actually define functions for them lol

paramorphisms are ezpz, it's just a cata with extra

...in Haskell. I fear what this will look like in the diagrams

You lost me at histomorphisms

I don't like zygomorphisms
para and mutu are fine

I've figured out the universal property for para and mutu but I don't see it for zygo

mutu phi psi . in = (fork phi psi) . fmap (mutu phi psi)
Isn't that lovely

Idk if that's a universal property. It's an equation alright

Two ppl I just met, immediately after shaking hands: "I guess we shouldn't be doing that"

What do I do now. I wanted to draw out mutumorphisms but what after...

Perhaps I shall get a souvenir

Nope itchy itchy. Back to the dorms it is

how tf do I draw a histomorphism

What is a function Mu F -> Cofree F A ???

We've got our fourth positive COVID test today... unless they were already included in the count idk. I only know one of the lecturers caught it

I'm so fucking itchy I hate this I wanna be OUTSIDE but the outside HATES ME

There's someone in our group whose first exposure to pattern matching might be Agda... oof
Come to think of it though, everything we've been doing could've been done in Haskell, idk when we're going to get to dependent types