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

Baby's First Category Theory Proof 😌

Omg new exercises posted... but it's 11:30 pm aaa but I wanna do them

Very suspicious of my para from cata

Me: *coughs once* is it COVID

lmao. technical difficulties

also at some point someone told me cut elim was let-bound expressions and I was surprised but hearing Frank Pfenning explain it, it makes total sense and I don't remember why I was surprised

If sequent calc without cut is natural deduction in normal form doesn't that mean proving cut elimination is proving normalization

Lmao. It was the next thing he said

Here we go. By induction on the derivations. The thing I've been doing for the past four months

Huh. Lexicographical induction on the cut premises
I wonder how he's going to frame that concept bc I've never seen it in a proofy context

Maybe sum of the heights of the derivations. Ew

I am always hearing about hereditary substitution

Oh negative/positive types is codata/data
That's easier to remember than negative/positive

If an ana then a cata is a hylo then what's a futu then a histo called

There's hylo but no meta?? smh

Somehow doing a concrete example has gotten me more confused. Maybe I'm just sleepy

I forgot Thorsten follows me on Twitter
I quoted smth he said in lecture in my OPLSS shitposting thread 💀

hold on. what is an isomorphism in category theory lol

that's like. two morphisms and two laws

I cannot pay attention to this type theory lecture lol

I look up at the screen and suddenly we're doing cubical equality in agda. what happened

send help I'm being haunted by hcomp

hcomp is defined by recursion on types?? like type casing??

The last speaker is a good speaker but the content is so boring I can't pay attention

Oh no he picked the same arrow for function types and for reduction

Running out of space in my notebook lol
Now OPLSS 2022 is going to be awkwardly divided across two notebooks

ugh I wanna sit outside and work bc it's so nice out but I know if I stay too long out I'll start leaking everywhere again... the AC is so strong inside I'm COLD

idk how some people have the time to go out for drinks and socialize bc there are literally so many homework exercises I want to do lmao
I'm STILL doing the algebra of programming ones but I want! to write! the abstract machine compiler!! and I probably will be up a little late to do that lol
I played some card games after dinner with ppl and that was fun so I don't regret that at all but each day is so long while there's still not enough time for everything

but I also want to clean up my slides and I want to edit the POPL paper and I want to look over the JFP feedback HELP

wth is a futumorphism supposed to do