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.

Filter by
Sorted by
Tagged with
0
votes
0answers
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 ...
3
votes
0answers
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 ...
0
votes
0answers
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 ...
1
vote
1answer
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,...
0
votes
0answers
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 ...
3
votes
0answers
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 ...
7
votes
1answer
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 ...
2
votes
1answer
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"...
1
vote
1answer
59 views

Equivalence of Cauchy Sequences and Cauchy Approximations, HoTT

In HoTT book (Homotopy Type Theory), in order to construct Cauchy reals they introduce the notion of Cauchy approximation, which are defined as : $$x \hspace{0.1cm} \colon \mathbb{Q} \to \mathbb{R} \...
1
vote
0answers
53 views

Path induction for homotopies between functions

Consider a version of HoTT where every type former specifies the "shape" of its identity type definitionally (e.g. an equality of pairs is a pair of equalities, equality of types is ...
3
votes
2answers
70 views

Missing (important?) substitution rule

I am reading The HoTT Book and I noticed that there is an extensive use of a very reasonable principle: if we have $b \equiv c : A$ then we can conclude $(a =_A b) \equiv (a =_A c) : \mathcal{U}$, for ...
6
votes
2answers
143 views

Propositional truncation $||$-$||$ and double negation $\neg\neg$

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$. According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a ...
2
votes
1answer
89 views

$\textsf{isStable}(A)\rightarrow\textsf{isProp}(A)$?

I meet both $\neg\neg$-stable and proof-irrelevant types in Harper's handouts on homotopy type theory. I know clearly that proof irrelevance does not imply stability, but does stability imply proof ...
2
votes
1answer
135 views

Proof-irrelevant $\exists$

Under the principle of propositions-as-types, existential propositions in logic are compared to $\Sigma$-types, and we have two projection rules $\pi_1$ and $\pi_2$ to make proof extraction. If we ...
1
vote
1answer
49 views

Propositional truncation and information hiding

I have a question regarding propositional truncation $||$-$||$ in homotopy type theory. According to the introduction rule of $||$-$||$, if $a:A$, then $|a|:||A||$. My question is, if $||A||$ is ...
0
votes
0answers
25 views

Proof that the type of homotopy equivalence is not a proposition

I've seen in The HoTT Book that assuming univalence for homotopy equivalences is inconsistent (this is Exercise 4.6). On some page, I've read that this is because without this "qinv-univalence&...
0
votes
1answer
49 views

What are the consequences of alternative type-theoretic definition of homotopy equivalence?

The standard definition of homotopy equivalence in HoTT is a quadruple of: $f: A \rightarrow B$ $g: B \rightarrow A$ $p: \operatorname{id} A = g \circ f$ $q: \operatorname{id} B = f \circ g$ ... ...
2
votes
1answer
56 views

Homotopy Type Theory: How long is the computer-assisted proof that concatenation of paths is associative?

My question refers to Lemma $2.1.4\ (\text{iv})$ of the HoTT book. I chose this lemma because it is simple to understand yet tedious to prove by hand. I have never used a proof assistant before, so I'...
1
vote
0answers
30 views

How is dependent function type for a constant family equal to ordinary function type?

On page 34 of the Homotopy Type Theory book, they say if $B : A \to \mathcal{U}$ is the constant family $B(x) = B_0$, then $\Pi_{(x:A)}(B(x))$ still takes $x \in A$ into $\mathcal{U}$ namely to the ...
0
votes
0answers
46 views

Is any function proof of equality of its range and domain elements according to HoTT?

According to wikipedia article on HoTT: In HoTT, the type a=b is the type of all paths from the point a to the point b. (Therefore, a proof that a point a equals a point b is the same thing as a ...
2
votes
1answer
109 views

What is the proof theoretic ordinal of Homotopy Type theory?

The proof theoretic ordinal of Martin-Löf type theory is $\Gamma_0$. What about HoTT and what about other flavors of type theory (the ones related to the lambda cube for instance)?
2
votes
1answer
60 views

Type theory for $\infty$-categories: retracts of shapes?

Here's another question about the formalities of Riehl and Shulman's A type theory for synthetic $\infty$-categories, and in particular about the role that "shapes" play in this type theory. In Prop 5....
1
vote
2answers
55 views

Construct function from a truncated proposition

In the remark below Cor 3.9.2 in HoTT book it says to construct a function from $ ||A|| $ to $ B $, we define a predicate $ Q:B\to\mathcal{U} $ such that $ \Sigma_{x:B}Q(x) $ is a mere proposition. ...
7
votes
1answer
134 views

Type theory for $\infty$-categories: how do we inhabit $\text{hom}$ types?

I've started reading Riehl and Shulman's A type theory for synthetic $\infty$-categories, which looks like it develops some beautiful theory, but I want to make sure I'm not misunderstanding some of ...
6
votes
1answer
154 views

“Size Issues” and Cantor's Paradox in HoTT

Section 3.5 of the homotopy type theory book describes the type $\text{Set}_{\mathcal{U}_{i}}\equiv\sum_{(A:\mathcal{U}_i)}\text{isSet}(A)$, which can be thought as the "type of all sets in the ...
2
votes
1answer
62 views

Path-Lifting in HoTT

Lemma 2.3.2 of the HoTT book defines a kind of path-lifting for "fibrations" (ie type families): The proof is left as an exercise, but I'm struggling to understand what the last propositional ...
0
votes
0answers
57 views

Definition of $\left(\infty, 1\right)$-category in context of homotopy type theory

It has been proven that any locally presentable, locally cartesian closed $\left(\infty, 1\right)$-category models constructive dependent type theory (CDTT). From what I gather, this is supposed to ...
4
votes
0answers
60 views

Typos in HoTT appendix A.1.2?

I've started reading the HoTT book and am trying to understand its formal treatment of Martin-Löf type theory. Something small in the "first presentation" of the appendix has tripped me up; see the ...
1
vote
1answer
90 views

Curry-Howard: Types with Logic vs Types as Logic

In the paper Knowledge Representation in Bicategories of Relations there is a short remark on p47 that makes a distinction that seems quite far ranging regarding the Curry-Howard Correspondence. The ...
2
votes
1answer
74 views

Subtypes in Cubical Type Theory

I have yet another question about CuTT. In the CCHM paper, a notion of cubical subtypes is introduced. A term of a subtype is generally written $\Gamma \vdash x : A[\phi \Rightarrow u]$ and is a ...
0
votes
0answers
62 views

Universes indexed by Integers

Can we assume universes to be indexed by integers. That is, assume a sequence of universes infinite on both sides, $$ \dots \mathcal{U}_{-n-1} : \mathcal{U}_{-n} \dots\mathcal{U}_{-1} : \mathcal{U}...
0
votes
1answer
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?
1
vote
1answer
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 ...
1
vote
2answers
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 ...
0
votes
2answers
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 ...
2
votes
1answer
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 ...
1
vote
1answer
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 ...
2
votes
1answer
57 views

Path type constructors in Cubical Type Theory

I have a question about the Path type in CuTT. As far as I know, they are basically functions (not really, since the interval isn't really a type; I'll abuse notation) of the form: $\textrm{Path} : (i:...
8
votes
1answer
269 views

Glue types in cubical type theory

Recently, I've been reading about Homotopy Type Theory. I haven't yet finished the book (in fact, I'm reading "Introduction to Homotopy Type Theory" by Egbert Rijke), but from the Univalence Axiom, I'...
3
votes
1answer
236 views

What's “higher level” than type theory as far as implementing a different kind of proof assistant goes?

I'm in the process of designing a better "logic framework" for BananaCats. Why do I seem limited to Type Theory (which is extremely "low level" for lack of better description). I don't care about ...
0
votes
2answers
54 views

Why values can not be replaced with their extensionally equal values in an intensional system?

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that: Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
5
votes
0answers
80 views

Cyclic lists in topology

Background: In computer science, there is a notion of cyclic lists, which are typically implemented using pointers or modular arithmetic. Mathematically, we may define the set of 2-cycles of elements ...
4
votes
1answer
200 views

Induction on identity types in HoTT and dependent type theory

In Homotopy Type Theory, and more fundamentally in Martin-Löf's dependent type theory, the induction principle for identity types seems to allow the following: Given some type $B(x,y,p)$ dependent on ...
1
vote
1answer
62 views

Property of well-formed contexts in Martin-Löf type theory

In Appendix A (p. 426) of the IAS book Homotopy Type Theory, you find the following remark. \begin{array}{l}{\text { Such judgments are sensible only for well-formed contexts, a notion captured by }} ...
2
votes
1answer
119 views

Constructive models of Martin-Löf type theory with extensionality

I am trying to find a justification for homotopy type theory. Of course, I understand that there is value for certain types of mathematicians, but I would like to understand why computer scientists ...
5
votes
1answer
93 views

How do synthetic homotopy groups relate to the usual homotopy groups?

In Homotopy Type Theory (HoTT in what follows) one may compute homotopy groups of objects that bear names that are the same as some usual spaces: for instance one may consider $S^1$ which is defined ...
1
vote
1answer
106 views

About the homotopy type of the path space

My sole question is: Given two homotopy equivalent topological spaces $X$ and $Y$ and points $p \in X$, $q\in Y$, then what do we know about the two associated loop spaces $\Omega(X;p,p)$ and $\Omega(...
2
votes
1answer
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 ...
1
vote
1answer
90 views

Subobjects in Homotopy type theory

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 ...
2
votes
0answers
47 views

bi-invertible maps is a mere proposition (HoTT)

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\...