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

237 questions
Filter by
Sorted by
Tagged with
102 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 ...
92 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 ...
83 views

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

I'm reading Introduction to Homotopy Type Theory by Egbert Rĳke 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 ...
1 vote
119 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$ ...
105 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 ...
53 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 ...
41 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/...
49 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 ...
1 vote
48 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" ...
512 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:...
90 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 ...
2k 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 ...
74 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 ... 1 vote
93 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 ...
1 vote
69 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 ...
1 vote
60 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 ...
1 vote
38 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 ...
1 vote
71 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 ...
99 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 ...
80 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 ...
76 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,...
1 vote
57 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 ...
147 views

119 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-...
1 vote
36 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 ...
158 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 ...
1 vote
95 views

185 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 ...
315 views

### What is problematic with formalizing higher category theory directly in HoTT

This is a soft-question. But please let me know if its not suitable. My question is essentially what the title asks but I want to elaborate on a few things. I know Emily Riehl uses a type theory to ...
211 views

### Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
170 views

### Categorical Intuition of Path Induction

I am trying to understand path induction from the trinitarian point of view. So far I understand the informal intuition of path induction from a homotopical and computational point of view. But I am ...
1 vote
78 views

### Proof relevant relation

Let $$ac : \left( \prod_{(x:A)}\sum_{(y:B)}R(x,y) \right) \rightarrow\left( \sum_{(f : A \rightarrow B)}\prod_{(x:A)}R(x,f(x)) \right)$$ defined by ac(g) :\equiv \Big( \lambda x.pr_1(g(x)), \lambda ...
238 views

### Recursor and induction functions in dependent type theory

I'm reading HoTT book and I'm not sure if I really understand how the recursor function is related to the induction function. It is stated that product types are said to be : a degenerate example of ...
1 vote
93 views

### Propositional Uniqueness for Coproduct Types?

I'm working through the HoTT book and have just finished the section on coproducts. In short, I am wondering if there is a uniqueness principle for coproduct types. I can not find mention of one in ...
426 views

### Object Classifier implies Univalence in Type Theory?

There is a correspondence between univalence in Type Theory and object classifiers in $\infty$-toposes. This, for example, is suggested in the article Univalent Foundations for Mathematics on nlab. ...
65 views

### Definition of a map of (pre)spectra in HoTT

I'm trying to pick up some homotopy theory by reading various HoTT sources (I find it much easier than reading classical homotopy theory books). In Floris Van Doorn's PhD thesis he defines (pre)...
105 views

### How to show the double cover of $S^1$ is a circle in HoTT

Consider the family $E : S^1 \to \mathcal{U}$ so that $E(\mathtt{base}) = \mathbf{2}$ $\text{apd}_E(\mathtt{loop}) = \mathtt{ua}(\lnot)$ where, of course, $\lnot : \mathbf{2} \simeq \mathbf{2}$ ...
1 vote
Context. In what follows, we work in Martin-Löf type theory (MLTT). We denote dependent product types by $\forall$, the identity type over a type $T$ by $\equiv_T$, and let $U$ stand in for arbitrary ...
According to the HoTT book [6.9], the propositional truncation $||A||$ of a type $A$ can be viewed as a higher inductive type generated by A map $|-|: A \to ||A||$ A path in $x = y$ for any \$x,y: ||A|...