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
1
vote
1answer
49 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 ...
5
votes
1answer
96 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. ...
0
votes
1answer
55 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)...
4
votes
1answer
81 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
1answer
144 views

Ordinary mathematical uses of Axiom K

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 ...
1
vote
2answers
97 views

Translating the induction principle from verbal form into rigorous one

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

Confusion about quasi-inverses and equivalences in HoTT

I'm reading the HoTT book, section 2.4, where for $f : A \to B$, they define $$\mathsf{qinv}(f) = \sum_{g:B\to A} \big( (f \circ g \sim \mathrm{id}) \times (g \circ f \sim \mathrm{id}) \big)$$ $$\...
0
votes
0answers
50 views

Syntax independent presentation of Homotopy Type Theory

By "syntax independent" I mean no explicit reference to variables. For example, Lambda Calculus is syntax dependent because the notions of "variable", "variable renaming",...
3
votes
1answer
142 views

Propositional truncation vs. Zero Knowledge Proofs

Disclaimer: This question is vague. It reports on a curious similarity in the hope that discussion might perhaps turn it into something more rigorous, but it's entirely possible that there's nothing ...
1
vote
1answer
87 views

How to derive $\prod x: \text{Nat}, Id(S(x), O) \to \bot$ in Intensional Type Theory

In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule: $$ \Gamma \vdash M : Nat ~~~ ...
0
votes
1answer
81 views

In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
1
vote
0answers
70 views

Homotopy type theory: what is «path induction» useful for?

I am reading the HoTT book. At page 49 path induction is introduced. Let us recap it. Given a family $$ C: \displaystyle \prod_{(x,y:A)} x =_A y \rightarrow 𝓤 $$ and a function $$ c: \displaystyle \...
1
vote
2answers
90 views

Formalizing constant symbols as terms in type theory.

In type theory, we usually define each type with a constant symbol, e.g., the dependent product uses '$\Pi$', the dependent sum uses '$\Sigma$', the sum/coproduct uses '$+$'. I noticed that we could ...
2
votes
2answers
146 views

judgmental and propositional statements in homotopy type theory

In homotopy type theory one has to distinguish between judgmental and propositional statements, eg in case of $a: A$ ("$a$ has type $A$") and equalities $a =_p b, a=_A b$. That is, are a ...
4
votes
1answer
60 views

Why is coherence important in the LCCC interpretation of substitution in dependent type theory?

Reading about the categorical models of dependent type theory (DTT) I have faced many articles pointing out the coherence problem for the interpretation of DTT in locally cartesian closed categories (...
1
vote
1answer
60 views

Is it possible to prove induction over a setoid quotient?

I've been playing with some homotopy stuff in category theory. It's possible to define a "circle" with a sort of Scott encoding along the lines of ...
0
votes
1answer
74 views

Law of the Excluded Middle for Mere Propositions

In the Homotopy Type Theory book, they define the (non-contradictory) law of the excluded middle as $$\operatorname{LEM}:\prod_{A:\mathcal U}\big(\operatorname{isProp}(A)\to(A+\lnot A)\big).\tag{3.4.1}...
1
vote
0answers
72 views

Polynomial functors, Type Theory and Homotopy

I am finding that there is a bit of a battle going on to provide a "foundation" of Type Theory, and perhaps for Mathematics, either with polynomial functors or Homotopy Type Theory. There ...
1
vote
1answer
49 views

Derivation of term conversion rule

I've started to read Egbert Rijke's HoTT lecture notes which can be found here. In the first lecture, some inference rules and structural rules are given, and in Exercise 1.1 it is asked to derive ...
8
votes
1answer
111 views

Intensional identity

I have some basic questions about intensional identity. Two types are said to be (intensionally) identical iff “they have the same objects and identical objects of one of the types are also identical ...
2
votes
0answers
59 views

$\eta$-rules of inductive types in homotopy type theory

I'm currently reading Appendix 2 in HoTT-Book, which is a formal presentation of homotopy type theory, and I found that we don't have $\eta$-conversions of inductive types (e.g. the coproduct types). ...
0
votes
0answers
46 views

uses and proofs of the cardinality of the continuum

after reading this https://en.wikipedia.org/wiki/Cardinality_of_the_continuum I wonder what good is it as a tool in mathematics if there is no proof. is it merely useful to prove that it is ...
7
votes
1answer
91 views

From $\textsf{Prop}$ to $\textsf{Type}$

Let $P,\top:\textsf{Prop}$ (where $\textsf{Prop}$ is the universe of mere propositions), $A=\{P,\neg P\}:\textsf{Type}$ and $B$ is an identity function such that $B(x)=x$. Given the above definitions, ...
0
votes
1answer
250 views

Difference between Propositional and Judgmental Equality

I'm reading the HoTT book and actually I'm a bit confused on core difference between propositional equality (noation: $a=_A b$ where $a, b:A$ and judgmental equality $ a \equiv b $. The ...
1
vote
0answers
50 views

Transport operation on $\Sigma$-types in cubical type theory

In Exercise 4.3 of "Cubical Methods in Homotopy Type Theory and Univalent Foundations'', It sais that we run into problems when we try to define computation rules for transport operation on $\...
6
votes
1answer
56 views

Truncation and fixed finite domain

Let $P$ be a type, $||P||$ denotes a mere proposition obtained by truncating $P$. Let $D$ be a type and $A:D\rightarrow\textsf{U}$, then $\Pi x:D.A(x)$ is a well-formed type. Assuming that we are ...
2
votes
1answer
58 views

Truncation and $\Pi$-types (ii)

I just read Ximei's post Truncation and $\Pi$-types. Can anyone explain in simple terms why ($\star$) implies ($\star\star$) but not vice versa. In other words, I wonder why ($\star$) is stronger than ...
1
vote
1answer
98 views

In homotopy type theory, prove that law of excluded middle implies reduction ad absurdum

It's about Excercise 2 from here: While the principle of excluded middle $P\vee\neg P$ ( tertium non datur) is not provable, prove its double negation using the propositions as types translation: $\...
6
votes
1answer
74 views

Truncation and $\Pi$-types

Truncated types or bracket types are used to recover traditional logic within type theory. I have a question about truncating $\Pi$-types. The question is very basic. Let $A:\textsf{U}$ and $B:A\...
3
votes
2answers
139 views

In what sense does Homotopy type theory "model types as spaces"

I've read at multiple points (e.g. here) that homotopy type theory "models" types as spaces. I can understand informally that we can "think of" types as spaces, in a vague sense. ...
2
votes
2answers
220 views

In Homotopy Type Theory, how do the continuous notions of spaces and paths, match the discrete notions of constructible terms and proofs?

Context: I'm starting with being interested in type theory as a framework within which to do mathematics (e.g. practically, using proof assistants based on type theory), and my understanding is that ...
2
votes
0answers
78 views

Grammar for homotopy type theory?

The HoTT book says: We will not attempt to give a formal presentation of the grammar of a valid inductive definition and its resulting induction and recursion principles and pattern matching rules. ...
5
votes
1answer
80 views

Truncation and $\textsf{isProp}$

In type theory, in particular, homotopy type theory. We have a notion of $\textsf{isProp}$ defined as follows (where we let $A:\textsf{Type}$): $$\textsf{isProp}(A):=\Pi x,y:A.x=_Ay.$$ In words, $A$ ...
1
vote
1answer
68 views

Cohomology vs. Reduced Cohomology in homotopy type theory

I just read Mike Shulman's blog post the other night, discussing the definition of cohomology in Homotopy Type Theory. I really enjoyed the new (to me) perspective, but I had a few questions on ...
1
vote
1answer
117 views

Relation Between Dependent Type Theory And Categories

I have been trying to understand the relationship between a dependent type theory and a corresponding locally Cartesian closed category $\mathbb C,$ as described in R. A. G. Seely, Locally cartesian ...
1
vote
1answer
82 views

Type Theory Rules For The Empty Type

I would like some help choosing the rules for the empty type. I am trying to setup a typed lambda calculus with sums like in Extensional Normalisation and Type-Directed Partial Evaluation for Typed ...
1
vote
1answer
44 views

Concerning the $\eta$-rule

In Martin Lof's type theory, one has a term $$ x:A, y:A, z: Id_A(x,y) \vdash J(r(x);x,y,z): Id_A(x,y) $$ can one derive judgemental equality $J(r(x);x,y,z)=z$ without the $\eta$-rule?
0
votes
0answers
95 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
48 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 ...
1
vote
0answers
79 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 ...
0
votes
1answer
108 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
61 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
85 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 ...
8
votes
1answer
303 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
83 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
80 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
59 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
91 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 ...
7
votes
2answers
196 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
111 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 ...