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.

195 questions
Filter by
Sorted by
Tagged with
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 ...
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. ...
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)...
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}$ ...
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 ...
97 views

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 ...
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 ...
98 views

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. ...
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 ...
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. ...
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$ ...
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 ...
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 ...
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 ...
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?
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 ...
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 ...
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 ...
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,...
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 ...
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 ...
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 ...
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"...
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} \...
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 ...
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 ...
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 ...
$\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 ...