/sci/ - Science & Math

>>11507045
ring is not for circle, but - akin to "group", "set" or "category" - denotes a collection of thing. Think crime ring.

The proof term is

[math] \lambda x.\, \langle x, \mathrm{refl_x} \rangle [/math]

i.e. for each x take y:=x, assuming reflectivity of equality.

By restricting the comprehension axiom. The naive one being "State a property P and I collect all sets with that property into a set Y for you".
The restriction is to one that is restricted to subsets. "State a property P, give me a set X and I collect all sets FROM THAT SET X with that property into a set Y for you".

The above is a bit too restrictive and so another axiom is added, the scheme of replacement, that also allows for searching for parameters fulfilling a property and also guarantees that those are sets. You can think of it as "The image of a function that you can define on X also gives set Y"

>>10226306
>what did he/she mean by this?
It says in the about section that it's by Lurie.
Which is good and bad. Bad because I doubt he knows how to write an accessible text.
But the whole book as a web page concept is interesting, strangely I never saw it realized.

https://kerodon.net/tag/0008

I think it's pretty clear that it's one of the highest, if not the highest, production quality of animations on math out there.

If you force me to criticism, I'm personally more interested in higher level math and he also has a fetisch for certain topics, especially let's say 2'nd year analysis and autistic (but more or less pretty) proofs. His topology argument proofs are cool but forcibly finding geometric representations of this and that series and transformation is..forced. But that's complaining on a high level. Also, it's a double edged sword to criticise innovative visualizations, because otherwise nobody would do them.