🎯 Learning Objectives
Why QG Needs Type Safety
Understand why traditional approaches fail and how type errors plague semiclassical gravity.
Emergent Spacetime
Explore the conjecture that spacetime emerges from more fundamental structures via a functor.
Holography as Equivalence
See AdS/CFT as an equivalence of categories—same theory, different presentations.
Current Approaches
Survey loop quantum gravity, causal sets, and higher gauge theory from a type-theoretic view.
📖 Key Concepts
The Problem with Quantum Gravity
Why is quantum gravity so hard? From a type-safe perspective:
- Background dependence: Standard QFT assumes fixed spacetime—but in QG, spacetime itself is dynamical
- Type mismatch: Semiclassical gravity (G_μν = 8π⟨T_μν⟩) mixes classical and quantum types!
- Non-renormalizability: Infinities arise from treating gravity like ordinary QFT
Many proposed "quantum gravity effects" are actually type errors in disguise.
The Emergent Spacetime Conjecture
Conjecture: Spacetime is NOT a fundamental type.
Instead, spacetime emerges from more fundamental structures
via a functor:
Emergence : Quantum → Spacetime
Evidence:
- AdS/CFT: bulk spacetime emerges from boundary QFT
- ER=EPR: geometry emerges from entanglement
- Holographic entanglement entropy: S = Area/4GHolography as Functorial Equivalence
The AdS/CFT correspondence may be an equivalence of categories:
QG(AdS_{d+1}) ≃ CFT_d
This is not just "duality" but TYPE ISOMORPHISM:
- Same objects (physical states)
- Same morphisms (physical processes)
- Same composition (consistent physics)
Different presentations of the SAME theory!Type-Safe Approaches to QG
Loop Quantum Gravity: Spin networks are functors from graphs to SU(2)-representations. Type-safe: intertwiners at vertices must be compatible with edge representations.
Causal Sets: Spacetime as a locally finite poset. Causality is built into the type structure—no acausal compositions possible.
Higher Gauge Theory: 2-connections on 2-bundles for theories with strings and branes. Coherence conditions enforce consistency.
🤖 AI Learning Prompts
"Explain the fundamental difficulties of quantum gravity from a type-theoretic perspective. What does it mean that we can't 'just quantize gravity like other fields'? How does background dependence create type problems?"
"Explain the emergent spacetime conjecture. What evidence do we have that spacetime might not be fundamental? How would emergence work categorically—what functor takes us from 'quantum information' to 'spacetime geometry'?"
"Explain AdS/CFT as an equivalence of categories. What would it mean for quantum gravity in AdS to be 'the same category' as a boundary CFT? What are the objects, morphisms, and how does the equivalence work?"
"Explain the ER=EPR conjecture connecting wormholes (Einstein-Rosen bridges) to entanglement (Einstein-Podolsky-Rosen). How does this suggest geometry emerges from quantum information? What are the type-theoretic implications?"
"Explain loop quantum gravity from a categorical perspective. What are spin networks as functors? How does the type structure (representation labels on edges, intertwiners at vertices) enforce consistency? What are spin foams?"
"Explain causal set theory as a type-safe approach to quantum gravity. How does representing spacetime as a poset build causality into the type structure? What is the 'causal set action'? How might dynamics arise?"
"Explain 'it from qubit' approaches to quantum gravity. How does the Ryu-Takayanagi formula connect entanglement entropy to geometry? What does 'spacetime from entanglement' mean? How is this related to tensor networks and holography?"
"Explain higher gauge theory and its relevance to quantum gravity. What are 2-connections and 2-bundles? How do they describe theories with extended objects (strings, branes)? What categorical structures are involved?"
"What are the major open problems in applying type-safe methods to quantum gravity? What would a 'fully type-safe' formulation of quantum gravity look like? What categorical structures might characterize the final theory?"
"Explain the measure problem in quantum gravity and quantum cosmology. How do we define probabilities when 'everything happens'? How might type-theoretic approaches help with the problem of time and the interpretation of the wave function of the universe?"
✏️ Research Directions
Direction 1: Formalize Holography
Attempt to make precise the statement "AdS/CFT is an equivalence of categories." What are the objects and morphisms on each side? What structure must be preserved?
Direction 2: Emergent Dimension
Explore how the dimension of spacetime might emerge from more fundamental categorical data. What type of functor produces a manifold from abstract structures?
Direction 3: Quantum Causal Structure
Develop the type theory for "quantum causal sets"—where the causal order itself is in superposition. What categorical structures are needed?
📚 Resources
🔮 The Future
What Would Success Look Like?
A type-safe theory of quantum gravity would:
- Make background independence manifest in the type structure
- Have spacetime emerge functorially from quantum data
- Explain holography as a precise categorical equivalence
- Resolve singularities as type boundaries (geodesic incompleteness becomes non-totality)
- Be implementable in a proof assistant and computationally tractable
The crisis of foundations may be resolved—not by a new equation, but by a new understanding of what it means to have a physical theory at all.