Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added pointer to:
Originally said “Infinite sets cannot be constructed from finite sets, so their existence must be posited as an extra axiom.”
Now says “In set theory and set-level type theory, infinite sets cannot be constructed from finite sets, so their existence must be posited as an extra axiom.”
This is because in univalent type theory with coequalizer types one automatically gets the circle type - whose loop space type around the basepoint is the integers via univalence, even without the natural numbers type. See elementary (infinity,1)-topos for more details.
Anonymouse
“the circle type - whose loop space type around the basepoint is the integers via univalence, even without the natural numbers type”
This is false. If one adds axiom K or UIP to the univalent universe $U$ (not the whole type theory) than every type in the univalent universe is a set, and so will a circle type in the universe be a set. The univalent universe itself is a groupoid. The type theory is still consistent so long as the induction principle of the circle type or coequalizers in the universe only apply to families of $U$-small types, indexed by $U$-small types.
It’s maybe not so useful to speak of “false” for what amounts to hair-splitting of terminological conventions. You could just add the adjective which you find missing (“homotopy TT” instead of “univalent TT”).
1 to 4 of 4