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