# Questions tagged [homotopy-type-theory]

The homotopy interpretation of constructive dependent type theory, the univalence axiom, higher inductive types, internal languages of higher toposes, univalent foundations for mathematics, and implementations of such theories in proof assistants.

**2**

**1**answer

### Assuming decidable equality but not LEM in HoTT

**1**

**0**answers

### The difference between Agda and Idris for programming using Homotopy type theory [closed]

**3**

**0**answers

### Intuitive (topological) explanation of a proof from the HoTT book [closed]

**5**

**1**answer

### Using HoTT, why is twisted cohomology of BG group cohomology?

**2**

**1**answer

### Higher-dimensional paths as parametrizations of 1-dimensional paths

**7**

**2**answers

### Construction of Dedekind reals using higher inductive-inductive types

**7**

**2**answers

### Explicit different proofs of the same identity type in MLTT

**8**

**1**answer

### 3 questions about basics of Martin-Löf type theory

**1**

**1**answer

### Cohomology with local coefficients in homotopy type theory

**2**

**1**answer

### What do UF and ZF do to each other?

**3**

**1**answer

### Applications of opetopes

**15**

**2**answers

### Formal definition of homotopy type theory

**3**

**1**answer

### Defining (infinity,1)-categories in HoTT using only an interval type

**9**

**2**answers

### natural metrics for proof length

**14**

**2**answers

### Appearance of proof relevance in “ordinary mathematics?”

**6**

**0**answers

### Inductive type constructors with the defined type appearing in non-strictly positive position

**5**

**1**answer

### Considering each half of factorization of weak equivalence separately

**1**

**1**answer

### Showing that a certain simplicial set has levelwise small cardinality

**0**

**0**answers

### Is there a foundational approach that takes “structure” as primitive?

**4**

**1**answer

### Checking the functoriality of an expression involving dependent sum and product

**4**

**1**answer

### Uniqueness principle for functions types in the HoTT book

**2**

**0**answers

### Categorical semantics of the identity type

**15**

**4**answers

### Practical example in using (homotopy) type theory

**28**

**1**answer

### Deligne's doubt about Voevodsky's Univalent Foundations

**6**

**2**answers

### Progress towards a computational interpretation of the univalence axiom?

**60**

**4**answers

### Why did Voevodsky consider categories “posets in the next dimension”, and groupoids the correct generalisation of sets?

**21**

**0**answers

### What's the point of cubical type theory?

**3**

**1**answer

### Definition of $(\infty,1)$-category in HoTT [duplicate]

**4**

**1**answer

### How much homotopy type theory should be modeled by the unstable motivic category?

**15**

**2**answers

### What kind of category is generated by Cubical type theory?

**35**

**2**answers

### Defining $SU(n)$ in HoTT

**6**

**3**answers

### (Co)limits of locally cartesian closed categories

**13**

**1**answer

### Constructive homological algebra in HoTT

**11**

**3**answers

### Can Homotopy Type Theory or algebraic geometry deal with homotopy fibers in terms of families?

**5**

**1**answer

### Models for Higher Inductive Types in Homotopy Type Theory

**19**

**2**answers

### Stable homotopy type theory?

**1**

**0**answers

### Synthetic type theory for virtual double category and its higher categories

**79**

**2**answers

### Vladimir Voevodsky's works

**11**

**1**answer

### The role of univalence in the homotopy interpretation of type theory

**6**

**2**answers

### Type Theory to Study $(\infty,n)$-Categories and $(r,n)$-Categories

**1**

**0**answers

### How can one define “punctured torus” in Homotopy Type Theory? Is its fundamental group the free product of the integers with themselves?

**1**

**1**answer

### Problems for a Homotopy excursion in HoTT

**4**

**3**answers

### Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

**2**

**1**answer

### Why are types in type theory unordered collections?

**3**

**1**answer

### Is the univalence of the canonical family over a universe small?

**4**

**1**answer

### The axiom $\Xi : \prod_{A:\mathcal{U}} \|A\| \to A$ and the $n$-truncation of a type

**1**

**1**answer

### Univalent Foundations and canonicity property are compatible?

**1**

**1**answer

### Help with simple homotopy type theory proof [closed]

**3**

**1**answer

### Are there types with nontrivial paths in all dimensions? (HoTT)

**2**

**2**answers