Show newer

I should be asleep but guess what I'm not because I am plagued by congruence of convertibility

I've decided that inductive types are wrong and bad about it

Show thread

I mean it's a little weird to have to say beforehand which universe you want to stick your type in when the universe it's "allowed" to be and therefore the "true" universe might be smaller

Show thread

Type theories without inductives are a little unusual in that they just infer the universe it belongs in for you
I'm not sure if this means it's really a family of inductives indexed by level or if inductives are just weird for not being sufficiently general

Show thread

Honestly this has nothing to do with sized types. This is entirely me not knowing how to type theory

Show thread

nvm I confused the constructor with the formator
Both parameters of W need to be in Prop for W to be in Prop

Show thread

Same with W types, since those can be in prop when the branching parameter is in Prop
Funny that B wouldn't need to be in Prop tho, what's up with that

Show thread

I don't know how to do it because it would have to be universe polymorphic as well as universe level polymorphic, i.e. products would be in Prop if both parameters are in Prop

Show thread

The feature list in my target is getting ridiculous. It's CIC but also it has match eta and equality reflection and universe polymorphism
Oh that's not as long as I thought it would be. I'm chill with that theb

Show thread

I don't think I can proceed with my proof before I iron out universe levels with inductive types, which might involve a little polymorphism
Just a little

Show thread

I forgot to consider universe levels 🤦‍♂️

Show thread

I am the reason this is going so slow lmao I'm always like "I don't wanna do that today"

Show thread

Only thing left to do is to start on type preservation but it's 5 pm and I don't want to start that

Show thread

real numbers in name only, for they are neither

never mind. the proof of substitution from reflection relies on the congruence of convertibility lmao

Show thread

oh my god congruence could follow from substitution

Show thread

it would be pretty strange to only add either contractibility of singletons, which is a weird little thing anyway, or UIP, which is unnecessary for my purposes

Show thread
Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.