I think the heart of free software is really great!! It's just... some of the people....
ok, so set theory relies heavily on second-order logic to function, and second-order logic/set theory are two main levels on top of which most of mathematics is built, right?
i see type theory as championed by not having this hierarchy by "properties-as-types", however all the type theories i've seen have "judgements" of typing rules and equality that dictate how the type theory function. Is this not also a "two-level hierarchy" on which type theory is built? or am i thinking about the relationship wrong
why does it figure out judgemental equality for lambdas but not functions in `where` blocks
2.1/2.2 is kinda getting me. So I have to prove equality of these three proofs using path-induction
but clearly they don't use path induction in the same way, so they aren't judgmentally equal.
But each of these are functions, so don't I need funext to prove non-judgmentally-equal functions as equal?
i like topology, tea and type theory
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.