Questions tagged [homotopy-type-theory]
For questions about the field of study known as homotopy type theory.
27
questions
5
votes
1
answer
245
views
How do we use directed univalence in directed type theory?
In directed type theory of Riehl and Shulman, we have a new type, $hom_A\:x\:y$ representing arrows between elements $x$, $y$ of type $A$, note that these are not a priori functions.
I will call the ...
- 841
0
votes
0
answers
151
views
What is wrong with the "obvious" approach to function extensionality by providing context-aware rewrites?
There is an obvious, dirty and probably wrong approach that allows one to prove function extensionality in a straight-forward manner: provide an equality primitive with a context-aware rewrite. For ...
- 3,035
4
votes
1
answer
181
views
Effect of HoTT/Univalence Axiom on equality between terms of inductive types?
It is well known that Univalence contradicts Axiom K,
for example there are two ways $\mathbf{2} = \mathbf{2}$ may be proved using Univalence, via $\mathtt{id}_{\mathbf{2}}$ or $\mathtt{not}$.
But ...
- 151
3
votes
2
answers
365
views
How does axiom K contradict univalence?
I have seen it claimed several times that axiom K is inconsistent with univalence (e.g. here and here), but I have never seen a proof sketch. Specifically, I'm curious about how this manifests in the ...
11
votes
1
answer
824
views
Why is regularity a problem in cubical type theory?
In my current understanding, regularity in cubical type theory is the following definitional equality (I'm using $A~\textbf{type}$ to emphasize the fact that $i \notin FV(A)$):
$$
\cfrac{A~\textbf{...
- 945
4
votes
0
answers
172
views
Abstract stone duality and cohesive homotopy type theory
I have been reading the real-cohesive homotopy type theory paper and one of the remarks has sparked an interest. In this paper a string of monadic and comonadic modalities is introduced together with ...
- 841
4
votes
0
answers
169
views
Model of homotopy type theory where propositional & judgmental equality coincide for closed terms
In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal.
Is there a non-empty model of homotopy type theory ...
user61651
2
votes
1
answer
75
views
Surjection from a type to a universe
We work in homotopy type theory. Can there be a type $A:U_m$ and a map $f:A\to U_n$ for some $n\geq m$ such that the type $\prod_{T:U_n} \|\mathrm{fib}_f(T)\|$ is inhabited?
user61651
5
votes
1
answer
187
views
Choose term of coproduct type
We work in homotopy type theory. Denote the propositional truncation of a type $A$ by $\|A\|$ and the function type between types $A$ and $B$ by $A \to B$.
Can you construct a term of the following ...
user61651
16
votes
2
answers
1k
views
Proof relevance vs. proof irrelevance
I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance.
Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
- 565
0
votes
2
answers
251
views
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
I've been curious about the 'geometric situation' that one has when considering the type
$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$.
Here, addition is defined in the ...
3
votes
0
answers
103
views
Request for an update on a discussion about coinductive types in HoTT (or anywhere else)
Googling something else I stumbled on a conversation titled "coinductives" initiated by Vladimir Voevodsky on Google groups in 2014. It lasted for three days, invloved a dozen people, and ...
- 131
15
votes
1
answer
1k
views
Can we derive Cubical Type Theory from Self-Types?
Self Types are known for being a simple extension to the Calculus of Constructions that allow it to derive all inductive datatypes of a proof assistant like Coq and Agda, without a "hardcoded&...
- 3,035
6
votes
0
answers
119
views
Programmatic higher inductive/inductive-inductive types with equalities between equalities
I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and ...
- 841
7
votes
1
answer
196
views
Obtaining the Axiom of Choice through a modality in HTT
In (constructive) homotopy type theory, the law of excluded middle is not derivable. Moreover, assuming parametricity it is refutable.
But, one can work inside the double negation modality to obtain (...
- 173
9
votes
0
answers
282
views
Model of Coq (pCuIC) in higher toposes?
Can the type theory of Coq (pCuIC) be modeled in all higher Grothendieck toposes?
First of all, even the set theoretical model is not complete (e.g. inductive types in Prop). Although, this is ...
- 195
1
vote
1
answer
233
views
What is the coproduct: A + A? [closed]
In the HoTT book, it is said
The type of booleans 2 : U is intended to have exactly two elements. It is clear that we could construct this type out of coproduct and unit types as 1 + 1.
I don't ...
- 121
15
votes
2
answers
929
views
In the Hott book, are the most of the type formers redundant? And if so, why?
In chapter 1 and Appendix A of the Hott book, several primitive type families are presented (universe types, dependent function types, dependent pair types, Coproduct types, Empty Type, Unit type, ...
- 546
7
votes
4
answers
1k
views
Do I have to give up the Law of the Excluded Middle in order to Learn $\lambda$-Calculus?
I know very little about what I am talking about in what follows, so I appreciate any all help in pointing out all of my mistakes -- otherwise I won't be able to learn more and advance in my knowledge ...
- 503
13
votes
3
answers
834
views
What are the negative consequences of extending CIC with axioms?
Is it true that adding axioms to the CIC might have negative influences in the computational content of definitions and theorems? I understand that, in the theory's normal behavior, any closed term ...
- 777
6
votes
2
answers
353
views
In homotopy type theory, is there a IsManifold predicate?
Any type $A: \mathcal{U}$ can be thought of as a homotopy type, or a sufficiently nice topological space up to homotopy equivalence. Now, manifolds are topological spaces with some extra structure.
...
- 584
4
votes
0
answers
336
views
Category theory in plain MLTT
I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of:
a type of objects with equivalence relation (Obj : Set)
a type of arrows ...
- 1,732
8
votes
1
answer
680
views
Squash type vs Propositional truncation type
Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf ...
- 1,732
17
votes
1
answer
2k
views
Formalizing Homotopy Type theory in Idris
Looking at the homotopy type theory blog one can easily find a lot of library formalizing most of Homotopy Type Theory in Agda and Coq.
Is there anyone aware if there is any similar attempt to ...
- 454
7
votes
1
answer
319
views
How Univalence can be used for proofs about algorithm correctness
I read a book on homotopy type theory. HoTT has the univalence axiom. This axiom seems to simplify working in category theory, but which other fields of mathematics it simplifies? I.e. how can I use ...
- 1,732
10
votes
1
answer
187
views
Relating univalence for a theory of cateogries to the skeleton concept
Say I work in homotopy type theory and my sole objects of study are conventional categories.
Equivalences here are given by functors $F:{\bf D}\longrightarrow{\bf C}$ and $G:{\bf C}\longrightarrow{\...
- 505
13
votes
1
answer
2k
views
Homotopy type theory and Gödel's incompleteness theorems
Kurt Gödel's incompleteness theorems establish the "inherent limitations of all but the most trivial axiomatic systems capable of doing arithmetic".
Homotopy Type Theory provides an alternative ...
- 2,551