extremely ignorable post ahead
im trying to write A Post™ about my dumb programming language im making and why i think it's cool. and. it's hard
it is primarily a combination of two things, and one i think i kinda got something for, but the other.............
people's eyes already glaze over when you say the phrase "equality proof". how am i gonna say how inductive equality isn't good enough, but univalence goes too far for my purposes, and there is a nice middle ground called xtt, and
uhhhhhhhhh you know how minecraft has cubes. well what if your type system had cubes too. but also only the corners exist
