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.

Filter by
Sorted by
Tagged with
0 votes
0 answers
27 views

Is the existence of multiple algorithms for one problem the example of application of homotopy type theory?

There are problems which can be solved by multiple different algorithms, like shortest-path in graph: https://en.wikipedia.org/wiki/Shortest_path_problem. By Curry-Howard isomorphishm, each problem is ...
TomR's user avatar
  • 1,381
2 votes
1 answer
372 views

Which would be better for programming using Homotopy type theory Agda or Idris

I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
Ali S's user avatar
  • 21
2 votes
1 answer
79 views

Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda

An observation when defining List in agda with --without-K enabled: The following parameterized inductive definition is accepted:...
Kaa1el's user avatar
  • 191
8 votes
2 answers
576 views

What are the implications of Homotopy Type Theory?

I've recently come across the topic of homotopy type theory and I'm interested to learn more. I have a very limited background in type theory. Can anyone tell me, in functional programming terms or ...
thoughtpolice's user avatar
4 votes
0 answers
160 views

What are the applications of homotopy type theory to everyday programming?

What are the applications of homotopy type theory to everyday programming? I know of only two applications, neither of which I understand: "Homotopical Patch Theory" "HoTTSQL: Proving ...
Max Heiber's user avatar
2 votes
1 answer
108 views

Can Homotopy Type Theory be used to derive more efficient algorithms on more efficient data representations from less efficient ones?

I've read here that in HoTT, compilers could swap out less efficient representations of data for more efficient ones and I'm wondering whether my interpretation of that statement is correct. Say we ...
malte-v's user avatar
  • 155
5 votes
2 answers
275 views

Unordered pairs in Homotopy Type Theory

It's conceptually simple to state what an "unordered pair" is supposed to be in set theory. Yet, in homotopy type theory I have trouble formalizing this. A first naive try in agda syntax: ...
WorldSEnder's user avatar
2 votes
1 answer
323 views

Is cubical type theory still consistent with univalent excluded middle and univalent choice?

I want to formalize some undergraduate maths in cubical agda, and learning cubical type theory in the proccess. The problem is that I will need univalent excluded middle and univalent choice (and ...
Borja Sierra's user avatar
3 votes
1 answer
122 views

Derivation of product type eliminator in type theory

In HoTT book, section 1.5 (Product Types) in order to define the eliminators for the product type it assumes a function of type $g:A \rightarrow B \rightarrow C$ and then goes on to define the ...
al pal's user avatar
  • 621
2 votes
1 answer
109 views

Elementary proof that Bool is a Set

The type Bool, as in the datatype with just two point constructors true false : Bool and no higher-dimensional constructors, has ...
Cactus's user avatar
  • 205
8 votes
1 answer
820 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 ...
al pal's user avatar
  • 621
5 votes
1 answer
304 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 ...
V. Semeria's user avatar
2 votes
2 answers
152 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 ...
MJG's user avatar
  • 125
2 votes
3 answers
96 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. ...
al pal's user avatar
  • 621
6 votes
1 answer
95 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 ...
sryscad's user avatar
  • 191
2 votes
1 answer
189 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\...
al pal's user avatar
  • 621
7 votes
1 answer
453 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 ...
MJG's user avatar
  • 125
5 votes
2 answers
126 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=_{\...
Ilya Vlasov's user avatar
7 votes
1 answer
482 views

What should we return when pattern matching on a Path constructor?

Context: Cubical Type Theory Consider a simple HIT, say, an HitInt: ...
ice1000's user avatar
  • 928
2 votes
1 answer
80 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 ...
Cactus's user avatar
  • 205
5 votes
1 answer
103 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 ...
Cactus's user avatar
  • 205
7 votes
1 answer
168 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: ...
WorldSEnder's user avatar
0 votes
1 answer
72 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?
Daniel Donnelly's user avatar
2 votes
1 answer
126 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 ...
while1fork's user avatar
4 votes
1 answer
78 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 ...
L. Garde's user avatar
  • 236
5 votes
1 answer
191 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 ...
phischu's user avatar
  • 153
12 votes
2 answers
309 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 ...
Jake's user avatar
  • 3,790
8 votes
1 answer
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 ...
盛安安's user avatar
  • 934
2 votes
1 answer
83 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 ...
Dennis's user avatar
  • 143
3 votes
1 answer
305 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 ...
盛安安's user avatar
  • 934
8 votes
1 answer
231 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 ...
Filip Haglund's user avatar
0 votes
0 answers
113 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: ...
Stefan's user avatar
  • 368
5 votes
1 answer
104 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 ...
Jake's user avatar
  • 3,790
5 votes
1 answer
138 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$ ...
heisenbug's user avatar
  • 153
20 votes
3 answers
2k 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}} \...
Kostya's user avatar
  • 473
16 votes
2 answers
884 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 ...
Kostya's user avatar
  • 473
7 votes
1 answer
704 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 ...
hawkeye's user avatar
  • 1,199
12 votes
2 answers
2k 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 : \...
huynhjl's user avatar
  • 223