Skip to main content

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
2 votes
1 answer
130 views

Definite description in homotopy type theory

I asked this question there and I have been suggested to ask it here. In a paper by David Corfield, we have an account of definite description in homotopy type theory. The author gives the following ...
Bruno's user avatar
  • 308
0 votes
1 answer
42 views

Internal vs External in type theory

I'm learning type theory, and at one point in the HoTT book, is mentionned "external" constructions. I was wondering what precisely means internal/external in type thoery.
Maxime's user avatar
  • 329
-1 votes
2 answers
164 views

What is a "type" in type theory?

Types are taken as atomic in type theories like homotopy type theory. But what is the best way to conceptualize what a type is? Is it appropriate to think of them as a property that defines a category?...
Justify 's user avatar
2 votes
1 answer
48 views

Circularity in the definition of natural numbers with homotopy type theory

I am reading HoTT's book, I am interested in this theory because it is said that it works as a foundation of mathematics, so I want to see how this foundation works. I am interested in the definition ...
RataMágica's user avatar
1 vote
1 answer
77 views

For any module with vector set $V$ and scalar set $C$, must there exist a set $X$ such that $V$ and $(X → C)$ are isomorphic?

Here's some evidence that suggests the affirmative to my question. There exists an isomorphism between: $\mathbb{R}^{n}$ and $(\mathbb{N}^{<n} \to \mathbb{R}$) $\mathbb{R}^{\infty}$ and ($\mathbb{...
Nuclear Catapult's user avatar
2 votes
2 answers
111 views

HoTT and isomorphisms

I have heard that Homotopy Type Theory makes it so that isomorphic objects are “equal”. I wonder how this squares with a lot of mathematical examples from Algebra and Set Theory, where the nature of ...
mbsq's user avatar
  • 2,049
3 votes
1 answer
64 views

Why aren't $\infty$-groupoids commutative in HoTT?

I'm trying to read through HoTT, but I'm confused by the path induction principle, it seems too strong at the first glance. I tried "proving" that all suitable paths commute, and it looks ...
Aleksei Averchenko's user avatar
1 vote
1 answer
56 views

Is the set-indexed wedge of connected $1$-types a $1$-type?

We are working in homotopy type theory. Given a type $I$ and a family of pointed types $P : \prod i : I, \sum T : Type, T$, we can define the wedge product $\bigvee\limits_{i : I} P(i)$ as a certain ...
Mark Saving's user avatar
  • 32.2k
0 votes
0 answers
108 views

What are the axioms of homotopy type theory?

The primitive notions of Zermelo-Fraenkel set theory are those of set and membership, i.e. we don't define what we mean by 'set' neither what we mean by '$\in$', rather, the axioms define what we mean ...
RataMágica's user avatar
4 votes
2 answers
215 views

LEM and the curry-howard correspondence

The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
user avatar
0 votes
0 answers
91 views

Classicalities of Homotopy Type Theory

What are statements of HoTT that are not provable therein and thus may or may not be true in specific models, specifically models in $(\infty,1)$- topoi? I've also seen the term "classicalities&...
Secher Nbiw's user avatar
6 votes
1 answer
232 views

What does it mean for a model category to present a higher category

A model category serves as an abstract/ axiomatic framework for homotopy theory. A higher category, in particular an $(\infty,1)$ category, I'm using the model of quasicategories, is a category with ...
Secher Nbiw's user avatar
3 votes
0 answers
193 views

What is the essence of infinity category theory?

*I understand that there are similar questions on this site and on the web, but I've failed to find any that give a satisfactorily plain enough answer for me to understand, given my background, and ...
Joseph_Kopp's user avatar
3 votes
2 answers
116 views

What's the difference between a section and a dependent function?

I'm reading Introduction to Homotopy Type Theory by Egbert Rijke and get confused by the notions of a section and a dependent function. A section is defined as: Definition 1.2.2 Consider a type family ...
user144765's user avatar
1 vote
0 answers
124 views

What can we say about the collection of sets $\{s_{ij}\}$ for some particular topos $T$?

Let $X$ be some space and let $T$ be topos on $X$ (e.g. Grohtendieck topos on the topological space). Topos $T$ is the category of sheaves ${S_i}$, where each sheaf $S_i$ maps each open subset $O_j$ ...
TomR's user avatar
  • 1,323
0 votes
1 answer
125 views

Circularity in the proof of uniqueness principle for product types in HoTT book

This is possibly something I've overlooked while reading the HoTT book (section 1.5), on defining the product types and proving the uniqueness principle for it (every element of a product type is a ...
Xiaojia Rao's user avatar
0 votes
1 answer
60 views

What collections of sets are appropriate for the "HoTT: Logic of spaces" and are they models?

There is very nice article https://arxiv.org/abs/1703.03007 "Homotopy type theory: the logic of space" which provides mapping among 1) Types of Homotopy Type Theory; 2) objects and morphisms ...
TomR's user avatar
  • 1,323
1 vote
0 answers
44 views

How category of diffeological spaces is related to the classifying category of HoTT? Maybe they are the same?

I am trying to read "Homotopy Type Theory: The Logic of Space" https://www.cambridge.org/core/books/abs/new-spaces-in-mathematics/homotopy-type-theory-the-logic-of-space/...
TomR's user avatar
  • 1,323
2 votes
0 answers
52 views

violation of Church Rosser with sum types

On https://ncatlab.org/nlab/show/sum+type the following $\eta$-reduction rule is given for sum types: $$\mbox{match}(p,x.c[\mbox{inl}(x)/z],y.c[\mbox{inr}(y)/z]) \rightarrow_{\eta} c[p/z]$$ This rule ...
provocateur's user avatar
1 vote
1 answer
52 views

Interpretation of HoTT in the Reedy model structure on bisimplicial sets [closed]

I was trying to understand the interpretation of HoTT in the Reedy model structure on bisimplicial sets. While going through, it suggests to think of bisimplicial sets as having a "spatial" ...
CAT's user avatar
  • 539
14 votes
3 answers
723 views

Help! I don't believe in the identity elimination rule for Martin-Löf type theory/HoTT!

I was watching this video this video "$\infty$-Category Theory for Undergraduates" by Emily Riehl, and was onboard with everything except the path induction principle for identity types (27:...
D.R.'s user avatar
  • 8,885
2 votes
1 answer
135 views

Is it fair to say that Martin Löf Type Theory is doing the same for maths as what type theory did for programming languages?

Let me clarify what I mean. I am currently writing a dissertation on ML/Homotopy type theory as someone who is more of a theoretical computer scientist than an Algebraist. My dissertation is focused ...
Dmitriy Filippov's user avatar
25 votes
3 answers
3k views

Approaching Type theory and Category Theory as a starting point in the study of mathematics?

I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas. It seems that many researchers in Type ...
Mateus Galdino's user avatar
2 votes
1 answer
80 views

On iterated sigma type

Just to make sure I understand the notation in the excerpt below (from Corfield's "Modal Homotopy Type Theory") correctly, is the "sum" over $x:Activity, y:Achievement$" the ...
user avatar
1 vote
1 answer
116 views

Why is the circle not contractible in homotopy type theory?

I know that the circle type is not supposed to be contractible in homotopy type theory. But by the definition of contractible, it seems like it is. Define the circle type $S^1$ as the higher inductive ...
Adrian's user avatar
  • 197
1 vote
2 answers
80 views

What is the point of "typal" computation rules?

The (recently created) page titled integers type on ncatlab.org, in the section "As the inductive type generated by an element and an equivalence of types", gives two different forms of the ...
Adrian's user avatar
  • 197
1 vote
0 answers
73 views

How does one prove that constructive type theory is isomorphism-invariant?

In his paper Structuralism, Invariance and Univalence (pdf), Steve Awodey makes the following claim about constructive type theory: The system of type theory has the important property that any ...
Penelope Clairmont's user avatar
1 vote
1 answer
41 views

univalence and indiscernibility

Given $A, B: U$ (where $U$ is a universe), define $\mathsf{Indis}(A, B)$ to be $\prod_{Q: U \rightarrow U} Q(A) \leftrightarrow Q(B)$. (This just says that $A$ and $B$ are in a certain sense ...
provocateur's user avatar
1 vote
1 answer
83 views

sum types in MLTT without universes

Suppose that $X$ and $Y$ are types that do not depend on anything else. Let $i$ be the usual function of type $X \rightarrow X+Y$ and $j$ be the usual function of type $Y \rightarrow X+Y$ discussed in ...
provocateur's user avatar
2 votes
0 answers
108 views

getting new results with universes

One remarkable thing about introducing a universe U (or many universes) into Martin-Lof Type Theory is that it allows us to show that certain types are inhabited that we would not otherwise be able to ...
provocateur's user avatar
2 votes
1 answer
91 views

An application of path induction

Does the rule of path induction (based or unbased, I don't care) allow us to infer $$u:A, \ v:A, \ p:u=_A v \vdash t: p = \mbox{refl}(u) \hskip 1 cm (*)$$ for some term $t$? It seems to me that this ...
provocateur's user avatar
0 votes
0 answers
91 views

Is there algebra (algebraic manipulation) of simplicial sets?

Is there algebra of simplicial sets? For example, symbolic representation of simplicial sets and operations on those representations that allow to construct new simplicial set from existing one – join,...
TomR's user avatar
  • 1,323
1 vote
1 answer
77 views

defintional equality types

If $a$ and $b$ are definitionally equal terms of type $A$ - i.e., $a$ and $b$ can be $\beta \eta$ reduced to identical terms - what follows about the structure of the identity type $a=_A b$? For ...
provocateur's user avatar
5 votes
1 answer
160 views

What's wrong with this "proof" involving' $n$-connectedness in HoTT?

okay, this is silly, but I can't for the life of me figure out what's wrong with the following "proof": Claim: if $B$ is an $(n-1)$-type, then $(n\text{-conn}(A) \to B) \simeq (\text{isCntr}(...
IsAdisplayName's user avatar
2 votes
1 answer
63 views

In Homotopy Type Theory, do $x, y$ exist such that $x = y$ is inhabited but $x \not\equiv y$?

I'm new to Homotopy Type Theory and am trying to understand the difference between judgemental and propositional equality. To my understanding, if $x,y: A$ for any type $A$ and $x \equiv y$, then one ...
Aron Schöffer's user avatar
1 vote
1 answer
148 views

Proving that W-algebra homomorphisms are contractible

I don't understand the conclusion of the proof of Theorem 5.4.7 of the Homotopy Type Theory text and would like a more detailed explanation of how it works. Here's my attempt at divining an answer. ...
Mark's user avatar
  • 47
4 votes
1 answer
255 views

The first-order metatheory of HoTT

Does there exist a (say, simply typed) first-order theory which axiomatizes a universe of $\infty$-groupoids, in a similar manner to how ZFC can be considered as an axiomatization of the universe of ...
ethanw's user avatar
  • 141
5 votes
0 answers
188 views

Reference for basic metatheory of Martin-Löf type theory

Section A.4 of the HoTT book states that the metatheoretic properties of Martin-Löf type theory (such as normalization and canonicity properties) can be proved using “standard techniques from type ...
simple jack's user avatar
15 votes
3 answers
1k views

In homotopy type theory, what are the intermediate values along a path?

I'm having a hard time understanding how the continuous notion of a path applies to homotopy type theory. I understand that from topology, a path is a continuous function $f : [0,1] \to X$ from the ...
LyleK's user avatar
  • 375
4 votes
1 answer
130 views

In homotopy type theory, why is function extensionality usually considered an axiom?

My understanding is that function extensionality follows from univalence. But I often see both function extensionality and univalence assumed as axioms, e.g., here. Wouldn't it be better to have fewer ...
Emma Hudson's user avatar
8 votes
0 answers
112 views

Is every homotopy equivalence a fibration over the interval?

It is a well known fact from homotopy theory that if $X\to Y$ is a Hurewicz fibration and $y_0,y_1$ are two points of $Y$ connected by a path $y_0\sim y_1$, then the fibers over $y_0$ and $y_1$ are ...
Robert Szafarczyk's user avatar
3 votes
1 answer
133 views

What are canonical injections in Martin Lof type theory

In the following paragraph from Martin Lof's 1972 paper... If $A$ and $B$ are types, then so is there disjoint union $A + B$, which is the type of objects of form $i(a)$ with $a:A$ or $j(b)$ with $b:...
Mark's user avatar
  • 399
0 votes
1 answer
141 views

Transport property

This question is prompted by Example 2.4.9 of the HoTT book. It is stated that, "for any $p:x =_A y$ and $P: A \to \mathcal{U}$ the function $\text{transport}^P(p,-): P(x) \to P(y)$ has a quasi-...
ToucanIan's user avatar
  • 209
1 vote
1 answer
38 views

Defining the n-glob as a HIT

I'm trying to define n-globs, for each n. I'm trying to do this in terms of an indexed family of higher inductive types. I think I have a working definition but it is almost intractable and hard to ...
IsAdisplayName's user avatar
3 votes
0 answers
172 views

There's Homotopy Type Theory so why not "Homotopy Set Theory?"

If you have "Homotopy Type Theory" than does a more traditional "Homotopy Set Theory" exist too? I think the simplest axiomization would be something like ZFC extended with a set ...
Ms. Molly Stewart-Gallus's user avatar
1 vote
1 answer
103 views

Homotopy Type Theory Path Lifting Property

Lemma 2.3.2 of the HoTT book states a path lifting property. I want to give a formal proof, in the sense that I want to inhabit a particular type, rather than just assume by path induction that $p \...
ToucanIan's user avatar
  • 209
1 vote
1 answer
108 views

HoTT Book: Proof of Lemma 4.1.1 and exerices 2.17, using univalence

I have a question about a certain method of proof used in the HoTT book. This question might just boil down to how univalence is used in practice. The method of proof I have in mind can be seen in one ...
IsAdisplayName's user avatar
1 vote
1 answer
76 views

Indiscernability of identicals (HoTT)

In 1.12 of the HoTT book it is mentioned that it is a simple exercise to show that indiscernability of identicals follows from path induction. I am getting the sense that it is a special case but I am ...
ToucanIan's user avatar
  • 209
2 votes
1 answer
34 views

Proving a proposition by inhabiting a type

I am working through HoTT and it was suggested (on page 43) that the reader prove the following proposition, if not(A or B) then (not A) and (not B) by exhibiting an element of the type $(A+B \to 0) \...
ToucanIan's user avatar
  • 209
4 votes
1 answer
243 views

Isomorphism vs. equivalence of types and homotopy vs. equality of functions

I am trying to build an understanding of the Univalence Axiom in HoTT and I am slightly confused about some definitions. If I was asked after reading of Chapter 1 of the HoTT book to formulate a ...
user1892304's user avatar
  • 2,828

1
2 3 4 5