also:

I think the heart of free software is really great!! It's just... some of the people....

logic thonk

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

HoTT exercises

hmmm

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

Joined Dec 2020