Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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.

1
vote
1answer
41 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
27 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\...
6
votes
1answer
85 views

Higher inductive type: what for?

The typical example of higher inductive type (HIT) is the circle $S^1$ that is nicely described here. I understand HITs are convenient if you want to do homotopy theory within type theory. But what ...
1
vote
1answer
27 views

HoTT informal path induction

As before I'm still exploring HoTT. While turning more to the informal everyday view on it, I have found an issue I cannot solve by my own. Proving by path induction can be done formal by invoking ...
1
vote
1answer
35 views

Transporting via an identity type when inducting along the higher inductive type $S^1$

I am reading the HoTT book https://hott.github.io/book/nightly/hott-online-1198-geeccc59.pdf and my question is regarding page 281, where the book says: When $x$ varies along loop, we need to prove ...
2
votes
1answer
59 views

Why should we adopt the cumulative universe convention?

In various sources on intuitionistic type theory, the universe of types is taken to be cumulative, i.e. $A:\mathcal U _i$ implies $A:\mathcal U_j$ whenever $i\le j$. The question is: why do we have ...
0
votes
1answer
30 views

Path Induction over HIT

I'm still trying to figure out things around higher inductive type in the setting of the HoTT Book. Setting Given the definition of $\mathbb{S}^1$ as it is stated in the HoTT Book, i.e. $\mathbb{S}^...
2
votes
1answer
70 views

In HoTT, does $\prod_{T : \mathcal{U}} T \to T$ have only one element?

In Homotopy Type Theory, I can define $id : \underset{T : \mathcal{U}}{\prod} T \to T$ by $id(T, t) \equiv t$ But, are there any other elements of $\prod_{T:\mathcal{U}}T \to T$ ? I have been able ...
1
vote
0answers
54 views

Induction over HIT (HoTT)

Setting Currently I try to formulate the simply typed $\lambda$-calculus in HoTT which results in quite involved inductive type families. Since I'm still new, I'm often unsure if my induction ...
0
votes
1answer
56 views

relation between inquisitive logic and logic as games?

In the very intriguing thesis "Questions in Logic" Ivano A. Ciardelli shows how to build a semantics of questions that reduces to Truth Conditional logic for factual statements where ¬¬p = p, but has ...
2
votes
2answers
65 views

Properties over partly specified inductive families (HoTT)

At the moment I'm about to get my head around homotopy type theory as a new perspective into mathematics. Insofar, I'm trying to mess around with it, prove some simple things and see where it gets; ...
0
votes
1answer
65 views

In homotopy type theory, is judgemental equality $x \equiv y$ the same as a proof of equality being judgementally equal to reflection (and so on)?

In homotopy type theory, there are two notions of equality. There's the internal propositional equality, $=$, and the stronger, more-meta judgemental equality, $\equiv$. My question is, is $x \equiv y$...
1
vote
0answers
113 views

Constructing a map from the 3-sphere to the 2-sphere from a link

Edit: As Qiaochu remarks, the following is a special case of the Pontryagin-Thom construction. It's done wrong, though, because the framing of links is being ignored. If nobody beats me to it, I'll ...
1
vote
0answers
51 views

Prospects of teaching/learning elementary math with computed-checked type theory

I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where ...
5
votes
1answer
113 views

Prove that in HoTT if types $A$ and $B$ are connected and $\Omega A = \Omega B$, then $A = B$

In Homotopy Type Theory, suppose that $A, B : \mathcal{U}$, and $a_0 : A$ and $b_0 : B$. Further, suppose that A and B are connected, so we have $\prod_{a:A}||a_0 = a||$ and likewise for B. Finally ...
1
vote
4answers
117 views

Constructivity and Piecewise Functions

I'm currently exploring homotopy type theory and intuitionistic mathematics. In constructive/intuitionistic mathematics, 2 features arise: A proof of $\neg \neg A$ is not a proof of $A$. All ...
0
votes
0answers
25 views

Reference of material regarding both simplicial stuff and HoTT

I am currently reading both the HoTT book and "Stuff on quasicategories" by Rezk, and recently I am feeling that some thoughts of them looks similar. Could someone please point out something to let me ...
1
vote
1answer
89 views

In HoTT, if $A$ and $B$ are both sets, then $A=B$ is a set

In the HoTT book, it is mentioned that if $A,B$ are sets, then so does $A=B$ of paths between $A$ and $B$. Could someone tell me about how to prove this, please? Thank you. With the help of the ...
0
votes
0answers
136 views

Calculus in Homotopy Type Theory

My understanding is that homotopy type theory is intended as a new mathematical foundations, as is notably being written up at https://github.com/UniMath/UniMath. I am wondering whether there has been ...
0
votes
0answers
26 views

Any path factor through the canonical lift uniquely

I am reading the HoTT book and have question regarding the following: Lemma 2.3.2 : (Path lifting property). Let $P : A → U$ be a type family over A and assume we have $u : P(x)$ for some $x : A$. ...
1
vote
1answer
99 views

Is HOTT, a new attempt at foundation of mathematics, free from incompleteness theorem or is it still suffering? [closed]

Do mathematicians who study Homotopy Type Theory think that it can be completely free from Godel-Rosser theorem?
3
votes
1answer
84 views

In Homotopy Type Theory, where does the lambda expression reside?

Background I am trying to develop a visual language for doing higher level mathematics. The language is essentially the language of categories with some allowances since this thing runs on a ...
3
votes
0answers
145 views

How to Prove Homotopy Equivalence in a Discrete Topology

In order to understand what exactly is meant by path in homotopy type theory, I am looking into homotopies. This led to the following questions (some definitions follow): Intuition for how "...
1
vote
0answers
60 views

Primitive notions for positiv types

I am currently trying to understand how to formalize homotopy type theory in Church-style as proposed in the second appendix of the HoTT book. How am I supposed to interpret the constructors of ...
1
vote
1answer
51 views

Type former as primitive constants

in the first appendix of the HoTT book the type formers (or connectives) are defined to be primitive constants, e.g. $\sum_{x:A}B$ is defined as $c_{\sum}(A,\lambda x.B)$. I was wondering what the ...
4
votes
2answers
145 views

Define $\neg\neg A$ to be truncation using LEM

I am currently reading the HoTT book and came across exercise 3.14: Show that assuming $\mathrm{LEM}$, the double negation $\neg \neg A$ has the same universal property as the propositional ...
1
vote
0answers
54 views

Dependent type theory: universes may have a type?

In Dependent Type Theory, as described in Appendix A of Homotopy Type Theory, it is immediate to prove that $\Gamma \vdash \mathcal{U}_i : \mathcal{U}_j$ with $j > i$. So every universe has another ...
-1
votes
1answer
75 views

Homotopy Type Theory contradictions in definitions of propositions?

Perhaps I'm just not understanding how the definitions are actually supposed to work. In particular, the definition of $\mathbb{S}^{1}$ confuses me. So first, we have $\text{base}:\mathbb{S}^{1}$ and ...
1
vote
2answers
312 views

What in general is a recursor?

I've been reading the Homotopy Type Theory Book, and in the first section is lists out all the kinds of types (function, pair, dependent function ...). Each time that it mentions a new type, it ...
2
votes
1answer
177 views

Can everything in category theory be restated in a sufficiently expressive type theory?

I've been reading the homotopy type theory (HoTT) book as well as some articles on ncat lab, particularly this article < https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+...
0
votes
1answer
78 views

Isn't definition of types in type theory as spaces, viewed from the perspective of homotopy theory a circular definition?

In the introduction section of the "Homotopy Type Theory" (https://homotopytypetheory.org/book/) it is said that: One problem in understanding type theory from a mathematical point of view, however,...
4
votes
4answers
162 views

a basic univalence puzzle concerning the sup function on sets

if sup({1,2,3})=3, why can't I use univalence and the fact that {1,2,3}≅{4,5,6} to establish that sup({4,5,6})=3?
1
vote
0answers
157 views

isomorphism in the real world [closed]

This question has been reformulated and posted to a basic univalence puzzle concerning the sup function on sets If my wife gives me a set of things to buy, eg. A = { sugar, flour, eggs, milk } and I ...
0
votes
1answer
155 views

Defining the recursor for natural numbers using iterator (HoTT book exercise)

This is exercise 1.4 from the Homotopy Type Theory book: Assuming as given only the iterator for natural numbers: $$ iter: \prod_{C:U} C\to (C \to C) \to \mathbb N \to C$$ with defining ...
0
votes
1answer
67 views

Proving homotopy is equivalence relation in HoTT

So, this is maybe just details, just had some questions on how to correctly write the proofs. In the HoTT book lemma 2.4.2 says that homotopy is an equivalence relation on each dependent function type ...
0
votes
1answer
124 views

Some very simple Type Theory exercises

I started doing the exercises from a Homotopy Type Theory intoduction class by Thorsten Altenkirch. The first one is very simple, you just have to prove some logical propositions by mapping them to ...
3
votes
1answer
126 views

Model of the circle without HITs

While playing around with HoTT, I came across a type "$C$" which seems a lot like $S^1$: $$ C \equiv \Pi_{A:U} \Pi_{x:A} (x=x\rightarrow A) $$ It has values $$ \begin{align} \text{base}C &: C ...
-1
votes
1answer
103 views

“Realizing” Globular Sets in Homotopy Type Theory

[Apologies in advance if I don't have the right terminology down for some things -- I'm a bit of a novice, hopefully not at the stage where I know enough to be dangerous, but not enough to be useful.] ...
0
votes
2answers
102 views

Synthetic homotopy theory lecture question [closed]

In this lectureLogic and topology at 20:21 there is a statement that type isContr which means "is contractible" means that for a given type A and every element x and pointed element a of type A, ...
3
votes
1answer
171 views

Question about the Univalence axiom.

In my study of Type Theory, the univalence axiom has been introduced as the statement that "Isomorphic structures are equal." I haven't learned how to define any algebraic, combinatorial, or ...
1
vote
1answer
72 views

In a commutative diagram in Homotopy Type Theory, why the commutativity is expressed as equality between functions and not as a homotopy equivalence?

I assume that I employ Homotopy Type Theory. Let $f:A\rightarrow B, g: B \rightarrow D, h:A\rightarrow C, k: C\rightarrow D$ so that a commutative diagram is formulated. Commutativity is translated as:...
1
vote
1answer
125 views

Transitivity of Intuitionistic Propositional Logic

I've started working through Robert Harper's lectures on Homotopy Type Theory (here) and I have trouble understanding the solution given for one of the homework problems. The task is to prove ...
2
votes
0answers
87 views

Homotopy as purely abstract property

A lot of category theory work is consisting of taking definition of sone structure ( set theory, topological space, ordered set) and constructing category where object internal structure is completely ...
1
vote
1answer
73 views

From projection function to recursor and viceversa

In the HoTT book, page 37, the authors are defining a way to work with product types. They first define $$pr_1 : A \times B \to A, \quad pr_1 ((a,b)):\equiv a $$ $$pr_2 : A \times B \to B, \quad pr_2 (...
4
votes
2answers
107 views

How can I construct $\mathbb{S}^1$ in Homotopy Type Theory via pushouts?

Suppose I take the $0$-skeleton $X_0$ to have a single inhabitant $base$. Let $S_1$ have a single point $base'$, with attaching map $f(base', -)=base$. If I construct the pushout to the 1-skeleton $...
7
votes
1answer
617 views

Does Homotopy Type Theory have a computational interpretation?

In the Robert Harper's course on Homotopy Type Theory, he talks about how it would be desirable to find a computational interpretation of the Univalence Axiom, as it would provide a way of running ...
2
votes
1answer
129 views

How to understand a principal bundle in Homotopy Type Theory

In yang-Mills Theory, the interacting field is captured by a principal bundle $P$. In particular, let G the group which is homeomorphic to the fibers which it preserves upon acting on them. For fibers ...
1
vote
0answers
63 views

Does homotopy type theory teach us anything about imprecise models of the real world?

Models of the real world are necessarily imprecise. Let’s say the real world looks like $A$ the model’s assumptions are $A'$ the model derives that $A' \to B'$ Does adding deformations $A' \overset{\...
1
vote
1answer
271 views

Is this a valid proof that function composition is associative in type theory?

On page 56 of "Homotopy Type Theory" they give the first exercise of defining function composition and proving that it is a associative. So here goes: $$\circ :\Pi_{g:A\rightarrow B}\Pi_{f:B\...
5
votes
2answers
376 views

What are the different approaches to formalizing type theory in the usual model-theoretic context?

Usually when formalizing a system of type theory, from what I've seen, authors usually either simply take the basic ideas of working with derivations, rules, and judgements as basic notions, ...