# Questions tagged [homotopy-type-theory]

For questions about homotopy type theory, including the homotopy theoretic interpretation of type theory or univalent type theory, univalence axiom, higher inductive types or related.

158 questions
Filter by
Sorted by
Tagged with
65 views

### General Idea of HoTT from the use of HoTT Library

I don't have a deep understanding of homotopy type theory, but I'm curious about the difference between coq and HoTT library. When proving with coq, instead of trying tactics brute force, we roughly ...
40 views

### ''Relax Type'' in Computational Logical Framework

I am reading a nlab article about Matt Oliveri's computational logical framework. It introduces new type constructors such as $\textsf{Relax}$. I tried to read the author's justification for the ...
40 views

### Is it not impossible to define self-interpreter in Homotopy Type Theory?

I've been exploring approaches to defining semisimplicial types in a variation of HoTT (as far as I know, it's equivalent to Book HoTT). If this construction succeeded, it would be a major step ...
41 views

### What is the relation between (and status of) the Univalent Foundations and Homotopy Type Theory?

It appears as though UniMath and HoTT on GitHub are both active up til and including today. The Wikipedia pages have both linking to each other. Without being steeped in both areas, how do they relate,...
46 views

### What's the difference between Fraïssé Theorem and the Univalence Axiom?

I used to be studying homotopy type theory where there's an axiom called "univalence", stating that $(A\simeq B)\simeq(A=B)$ where $\simeq$ stands for equivalence/isomorphism, $=$ stands for ...
75 views

### types which behave like sets

I'm reading the homotopy type theory book and this sentence is giving me trouble. "We can define a class of types which behave like sets. Homotopically, these can be thought of as spaces in which ...
136 views

### Computational Type Theory For Topos Logic

My question is basically, what approaches have been made to make computer proof assistants which can handle the internal logic of a topos ? To explain: while learning topos theory I was struck by the ...
66 views

### Do we always have $(A\times (A \to 0)) \simeq 0$?

I'm skimming through the HoTT book. Let $A:\mathcal U$. We have a function $\phi:\equiv((x,f)\mapsto f x):A\times(A\to 0)\to 0$ witnessing the principle of non-contradiction, and the "absurd"...
59 views

71 views

### HOTT and computer science [closed]

Is Homotopy Type Theory geared towards work in the foundations of mathematics only, or is it also useful in computer science?
63 views

### Judgemental equalities of path composition

I have yet another question about Cubical Type Theory, this time involving path composition. I think I have grasped the face systems and formation of the comp ...
63 views

### Every mere proposition is a set?

In the HoTT Book, lemma 3.3.4 states that "every mere proposition is a set", where a mere proposition is a type $A$ such that $IsProp(A) = \prod_{x,y: A}(x=_Ay)$ holds, and a set is a type $A$ such ...
100 views

### How do you apply $\Sigma$-typing to the definition of a category? (new to type theory here)

Here's a previous answer in which the author states that the definition of category is the following $\Sigma$-type. I'm not sure how that would look formally, so can you explain? You don't have to ...
295 views

### Motivation for particular definition of contractible type

There is a mainstream definition of a contractible type and it goes like this: $\textrm{isContr} (A) = (x:A) \,\#\, (y:A) \to (x == y)$, where $\#$ means dependent pair (precedence and associativity ...
57 views

### Consistent ways/ rules to define types with generators.

Is there a way/ set of rules to define types with their generators which is proven to be consistent (obviously the proof need not be in the same type theory). For example (I think) the following way ...
57 views

137 views

### Why such a complicated definition of recursion for $\mathbb{N}$ in HoTT?

The HoTT book defines $\mathbb{N}$ to have $0:\mathbb{N}, succ: \mathbb{N\to N}$ and a recursion constructor $\prod_{C:\mathcal{U}}C\to (\mathbb{N}\to C\to C)\to \mathbb{N}\to C$ with a certain ...
It is conjectured here that homotopy type theory is the internal language of an elementary $(\infty,1)$-topos. I have no idea what these are, but my naive understanding is the following: Homotopy ...
Equivalences in HoTT can be defined using bi-invertible maps. For a function $f : A\to B$ this is defined to be  \mathsf{biinv}(f) :\equiv \left(\Sigma_{h : B\to A}(h\circ f \sim id_A)\right)\times\...