There is a model of ZFC in homotopy type theory
Does exist a model of homotopy type theory in ZFC?
Is there a proof of "equal logical expressivity" of these theories?
p.s. I use word "model" in common sense, because I don't know model theory
2025-01-13 02:06:07.1736733967
Model of homotopy type theory in ZFC
781 Views Asked by georgy_dunaev https://math.techqa.club/user/georgy-dunaev/detail At
1
There are 1 best solutions below
Related Questions in SET-THEORY
- Why is the intersection of countably many homogeneously Suslin subsets of $\,^{\omega} \omega$ homogeneously Suslin?
- Countable Elementary Submodels $M \preccurlyeq H ( \theta) $.
- König's theorem (set theory) implication
- Measure theory Vitali nonmeasurable set.
- Real numbers for beginners
- On the Axiom of Choice for Conglomerates and Skeletons
- Showing extensionality for Mostowski collapse
- on the continuum hypothesis: only finitely many cardinals between $\aleph_0$ and $2^{\aleph_0}$
- Product of metric outer measures
- If $\kappa$ is regular, is $\prod^{\text{fin}}_{\alpha<\kappa}\operatorname{Fn}(\omega,\alpha)$ $\kappa$-cc?
Related Questions in FOUNDATIONS
- Is math fool-proof?
- Is there any solution to Frege's criticisms of Hilbert's Geometry without the application of Model Theory?
- Multiplication in $\mathbb{N}$ from two simple laws
- $\mathbb{Z}$: Unique operation s.t. $1\star m=m$ and right distributivity hold?
- Minimal foundations for Cardinal Arithmetic
- The diagonal product of the family $\{f_\alpha:\alpha\in I\}$ is injective.
- Is it possible to formulate category theory without set theory?
- Was Ramsey mistaken in thinking that the same proposition can be both elementary and non-elementary in form?
- Intensional vs. extensional equality (or something like this)
- Proving that the existence of strongly inaccessible cardinals is independent from ZFC?
Related Questions in HOMOTOPY-TYPE-THEORY
- Intensional vs. extensional equality (or something like this)
- Does propositional resizing preserve truth of propositions in HoTT?
- Axiom of choice in HoTT without sethood requirement
- Finding a type such that $X + 1 \not\simeq X$ and $X+2\simeq X$
- Identity type between A and B being non-empty implies non-emptiness of A and B?
- Identity type between A and B being non-empty implies non-emptiness of A and B?
- universal properties of dependent types
- Definition of "set" in HoTT
- HOTT proof of transitivity of ordering of natural numbers
- Case analysis in theorem 4.1.3 of the HoTT book
Trending Questions
- Induction on the number of equations
- How to convince a math teacher of this simple and obvious fact?
- Refuting the Anti-Cantor Cranks
- Find $E[XY|Y+Z=1 ]$
- Determine the adjoint of $\tilde Q(x)$ for $\tilde Q(x)u:=(Qu)(x)$ where $Q:U→L^2(Ω,ℝ^d$ is a Hilbert-Schmidt operator and $U$ is a Hilbert space
- Why does this innovative method of subtraction from a third grader always work?
- What are the Implications of having VΩ as a model for a theory?
- How do we know that the number $1$ is not equal to the number $-1$?
- Defining a Galois Field based on primitive element versus polynomial?
- Is computer science a branch of mathematics?
- Can't find the relationship between two columns of numbers. Please Help
- Is there a bijection of $\mathbb{R}^n$ with itself such that the forward map is connected but the inverse is not?
- Identification of a quadrilateral as a trapezoid, rectangle, or square
- A community project: prove (or disprove) that $\sum_{n\geq 1}\frac{\sin(2^n)}{n}$ is convergent
- Alternative way of expressing a quantied statement with "Some"
Popular # Hahtags
real-analysis
calculus
linear-algebra
probability
abstract-algebra
integration
sequences-and-series
combinatorics
general-topology
matrices
functional-analysis
complex-analysis
geometry
group-theory
algebra-precalculus
probability-theory
ordinary-differential-equations
limits
analysis
number-theory
measure-theory
elementary-number-theory
statistics
multivariable-calculus
functions
derivatives
discrete-mathematics
differential-geometry
inequality
trigonometry
Popular Questions
- How many squares actually ARE in this picture? Is this a trick question with no right answer?
- What is the difference between independent and mutually exclusive events?
- Visually stunning math concepts which are easy to explain
- taylor series of $\ln(1+x)$?
- Determine if vectors are linearly independent
- What does it mean to have a determinant equal to zero?
- How to find mean and median from histogram
- Difference between "≈", "≃", and "≅"
- Easy way of memorizing values of sine, cosine, and tangent
- How to calculate the intersection of two planes?
- What does "∈" mean?
- If you roll a fair six sided die twice, what's the probability that you get the same number both times?
- Probability of getting exactly 2 heads in 3 coins tossed with order not important?
- Fourier transform for dummies
- Limit of $(1+ x/n)^n$ when $n$ tends to infinity
Yes, as long as by "ZFC" you include its extension with some inaccessible cardinals, or (perhaps) are willing to play games with natural models. In other words, the only difference in consistency strength is that "ZFC" by default doesn't include any universes, while "HoTT" by default includes countably many.