Questions tagged [homotopy-type-theory]
Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.
29
questions
2
votes
1answer
83 views
What does canonicity property mean in Type Theory?
The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property.
Would you please explain ...
4
votes
1answer
103 views
What types are propositions?
In the propositions-as-types paradigm, we are still faced with the question : what types are propositions ? I currently know 3 different answers :
Coq's sort Prop ...
1
vote
2answers
54 views
Propositional truncation of excluded middle
It is clear to me that it should be impossible to prove :
exclMidl = isProp A → ((A) ⊎ (¬ A))
Because it would give deciding oracle for every Proposition.
My ...
2
votes
3answers
72 views
How is functional property guaranteed in type theory when function type is defined?
I understand that functions are not defined in type theory the same way they are defined in set theory, hence functional property is not directly defined when defining function type in type theory. ...
6
votes
1answer
55 views
Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory
I am proving a kind of structure invariance principle for magmas in Cubical Type Theory with the Agda/Cubical library. This is done by constructing a path between two simple magmas and then ...
2
votes
1answer
36 views
Relationship between dependent sum type and dependent product type?
Since dependent sum type ($\sum_{n\in \mathbb{N}} P(n) $) is interpreted as ($\exists n\in \mathbb{N}:P(n) $) and dependent product type ($\prod_{n\in \mathbb{N}} P(n)$) is interpreted as ($\forall n\...
4
votes
1answer
78 views
Proof that type does not have decidable equality in Agda
Can one create such function in Agda ?
ℕ→ℕ-undecidable : ¬ ( (f g : ℕ → ℕ ) → Dec (f ≡ g))
ℕ→ℕ-undecidable = ?
I am particularly interested in proof using ...
5
votes
2answers
79 views
Identity types and universes
Let us consider Martin-Löf type theory with a cumulative hierarchy of universes
$$
\mathcal{U}_0\colon\mathcal{U}_1\colon\ldots
$$
If $A, B\colon \mathcal{U}_i$, we can form an identity type $A=_{\...
0
votes
0answers
25 views
If you can have cyclic base types, or if they need to be infinite types
I am confused how to properly think about classes of classes. Basically, you can have a dog "filo" which is an instance of the dog "class". But the dog class is itself not an instanceof of "animal", ...
5
votes
1answer
271 views
What should we return when pattern matching on a Higher Indutive Type and the case is a Path?
Context: Cubical Type Theory
Consider a simple HIT, say, an HitInt:
...
1
vote
1answer
52 views
Interval extensionality?
For example, in the proof of lemma 6.4.1 in the HoTT book, a function inductively defined over a function is simply applied on paths loop and ...
5
votes
1answer
54 views
Why is reflexivity enough in this HoTT formulation of quotient types?
In this formulation of quotient types in cubical type theory I was able to implement an eliminator and use that to implement basically curried function application. However, in all this, the only ...
7
votes
1answer
84 views
Flawed argument in the proof of function extensionality in cubical type theory?
I am reading the lectures about cubical type theory in this github repo. In lecture 1 the author defines function extensionality the following way:
...
0
votes
1answer
52 views
Can you automatically generate a parser for a type using type theory some how?
Was wondering since all the types are spelled out constructively, and the constructions can all be reflected symbolically on a computer, if you can automatically parse expressions in a type?
2
votes
1answer
65 views
Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)
The homotopy type theory book claims in section 1.3 that "As in naive set theory, we might wish for a universe of all types" but from this one could "deduce from it that every type, including the ...
4
votes
1answer
66 views
When do we need U(n+2) to solve a problem that can be formulated in U(n)?
I understand the need for a universe hierarchy, and that each new level brings additionnal proof-theoretic strength.
In the HoTT book there are examples of proofs that need to use the next level in ...
5
votes
1answer
140 views
Continuing the example of why it's hard to compute with univalence?
In "Towards a cubical type theory without an interval" Altenkirch and Kaposi motivate why it is hard to compute with univalence. They say:
For example, we can define the equivalence ...
11
votes
2answers
181 views
Reducing products in HoTT to church/scott encodings
So I am currently going though the HoTT book with some people. I made the claim that most inductive types we will see can be reduced to types containing only dependent function types and universes by ...
8
votes
1answer
1k views
Cubical type theory for dummies?
I read one of those popular papers on cubical type theory, but no wonder I could only see formulas and diagrams without being able to recognize them at all.
So here's what I want. I want a deep ...
2
votes
1answer
48 views
How do the unit intervals compose when generating higher order homotopies?
I'm trying to apply homotopy type theory as a theoretical foundation for describing how database query plans solve relational algebra queries. I'm modeling the problem as, given a set of input ...
3
votes
1answer
139 views
Is it possible that the universe of types could be closed?
I asked a pretty vague question. I wasn't able to make it precise, but I can now. It seems to be out of the scope of the previous question, so I open another one.
In dependently-typed languages such ...
8
votes
1answer
137 views
Why is `map insertionsort` not to equal to`map mergesort`?
In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
0
votes
0answers
96 views
Meaning of the univalence axiom on plain data types
I'm trying to wrap my head around HoTT and can't figure out the intuitive meaning and validity of the univalence axiom. IIUC this axiom says:
...
5
votes
1answer
75 views
How to understand equivalence of indexes of a family of types that are not definitionally equal
So I've been reading things about HoTT and trying to get solid on the foundations before getting too much further into the book. I am confused by a certain point; maybe I just haven't read far enough ...
5
votes
1answer
93 views
Constructing a sphere ($S^2$) in HoTT directly?
(this is a repost of https://stackoverflow.com/questions/29802501/constructing-a-sphere-s2-in-hott-directly, which was voted out of SO)
I understand the construction of $S^2$ as a suspension of $S^1$ ...
16
votes
4answers
801 views
Is path induction constructive?
I'm reading through the HoTT book and I have a hard time with path induction.
When I look at the type in the section 1.12.1:
$$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}}
\...
12
votes
1answer
404 views
Can I have a “dependent coproduct type”?
I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one.
The chapter introduces the function type
$$ f:A\to B $$
and then generalizes it by ...
7
votes
1answer
613 views
What were the research outcomes of the Univalent Foundations Program year (Homotopy Type Theory)
The Institute for Advanced Study has had a year-long special program devoted to the Univalent Foundations Program.
At the end of this they have produced a book and a code repository.
At the end of ...
10
votes
2answers
1k views
Universes in dependent type theory
I am reading about dependent types theory in the Homotopy Type Theory online book.
In section 1.3 of the Type Theory chapter, it introduces the notion of hierarchy of Universes: $\mathcal{U}_0 : \...
