­jonoodle­ @ionchy@types.pl

I didn't like how I blasted through naturals and lists so instead I'm redoing them with "Tees" and adding the ugliest colours because I can

Doing some very insightful and thoughtful annotations

I just wanna ϵ: ok today

A very important question for the PList

Really going in with this onion metaphor

By transitivity, datatypes are like ogres

Today's mood
I really thought Sizes were just going to be inductives and that's that

what is this going on about
I'm very Jared, 19

How should I fix that second sentence? ⊡!A⊢Γ and !⊡!A⊢Γ imply each other (by maximality, as it says), I'm trying to figure out what the intent of "for then" was

Since when did I need a licence??

Oh here's the rules I settled on
The first two "facts" are derivable by induction and the third one is basically a macro for a derivation where you stick those Ds where the ps are in your tree, but I'm not sure about the fourth fact or how it's proven
It makes sense that you can replace a formula by an equivalent one but idk how to get "inside" C to do the replacement
I suppose it must be some proof by induction too

I'm proud of the double pun in this one

Okay I don't get this fourth one
Like I can see why it's invalid because B is just a random arbitrary formula unrelated to A but I don't get why they decided to state this particular schema
Like ?? what's the point of stating it

Excuse me, ticks are sizes
(slides)