­jonoodle­ @ionchy@types.pl

I swear it's harder to fall asleep the more important it is that you do

One day I'll figure out how ppl are quantifying the "power" of theories (or was it logics?) by assigning ordinals to them. Ordinal analysis or whatever

Okay maybe that's not a great example bc I think the way ppl were proving that was to define ordinals lol. Which are a set theory thing

He'll casually drop things like "the more universes you have the more endofunctions on naturals you have" and I'm like WHAT. how do you even BEGIN to prove something like that. and then not understand a single reply in the thread

Type theory has a lot of structure to it but disappointingly doesn't seem to have the same kind of semantic content as other branches of math without appealing to those branches. Except for those diagonal arguments which look like sleight of hand tricks, and every single tweet Martin Escardo makes about type theory that I don't understand

Every single "counterexample" in type theory that produces an inconsistency always does so via some other mathematical concept. Hurken's paradox is about set-theoretical universes and powersets. Berardi's paradox is about retracts which I think is some sort of topology thing. My proof using unrestricted large elimination of ordinals uses ordinals which is a set theory thing. Non-strictly positive types with impredicativity uses an injection from a powerset to itself which is a set theory thing. Then every other contradiction arises from a sort of diagonalization argument which I presume generalizes across all such instances but idk what the connection is, only that they all kind of look the same and have a sort of clever diagonal trick to them

I want a book like Counterexamples in Topology but it's a subject I understand

elim: forall P. (p: (x: f (Fix f)) -> f (P ?) -> P (In x)) -> forall x. P x

? ?

You can't really define an eliminator for Fix f can you
From an f (Fix f) there isn't really an interior Fix f you can apply to your predicate? idek what the type would be

Somehow learned about recursors and eliminators seperately after foldr foldl and never made the connection lmaooo

OH. fold IS the recursor lol

Dependent fold IS an eliminator lmao

I mean, a dependent recursion scheme that would then allow me to express an eliminator
Wait do dependent folds exist?

cata: forall P. (forall x. (fpx: f (P x)) -> P (In (? x fpx))) -> (x: Fix f) -> P x

but there's no f (Fix f) to stick into In, only f (P x) and (Fix f)

How do you express a dependent elimination principle using a recursion scheme bc I'm having trouble adding a dependency for the return type on the element of Fix itself
Like it's supposed to look like

cata: forall P. (f (P ?) -> P ?) -> (x: Fix f) -> P x

I imagine you'd need to fold it up once somewhere

Do you think paramorphisms deserve their own nLab page? I don't think they deserve their own page. It can be seen as a "generalization" of catamorphisms but it doesn't really count since you can literally implement a paramorphism using a catamorphism so there isn't really any extra expressivity
Now a histomorphism is different bc it's genuinely more expressive, and anamorphisms need their own page so that the eventual page on hylomorphisms can link to the two

Should I bring my Bachelor's diploma with me lmao
idk what the point would be, I'm gonna get my Master's diploma in the mail

No it'll wash off
I've had sharpie wash off of ceramic before

I should've gotten ppl to sign my mug