19 votes
Accepted

Can I have a "dependent coproduct type"?

The dependent sum is a common generalization of both the cartesian product $A \times B$ and the coproduct $A + B$. It just so happens that the HoTT book introduces dependent sum by generalizing $A \...
  • 28.4k
16 votes
Accepted

Is path induction constructive?

It is an illusion that the computation rules "define" or "construct" the objects they speak about. You correctly observed that the equation for $\mathrm{ind}_{=_A}$ does not "...
  • 28.4k
11 votes
Accepted

Why is `map insertionsort` not to equal to`map mergesort`?

It has to do with the axiom of extensionality, i.e. whether you accept it for functions or not. The statement of this axiom with regard to functions is $$\forall f,g:A \to B,\ ((\forall x:A ,\ f\ x = ...
  • 3,419
10 votes
Accepted

Proof that type does not have decidable equality in Agda

ℕ→ℕ-undecidable is not provable in Agda. If we postulate the law of excluded middle (LEM), it follows that equality on every set is decidable, contradicting ...
10 votes
Accepted

What does canonicity property mean in Type Theory?

There are potentially multiple ways of presenting canonicity (and I think complications depending on the theory). However, I think the simplest way to think about it is from the perspective of a ...
  • 2,155
9 votes
Accepted

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

it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer My understanding is ...
9 votes
Accepted

Cubical type theory for dummies?

A year after and I'm writing one myself.
  • 914
8 votes

Reducing products in HoTT to church/scott encodings

To get your idea working you need something extra, as was pointed out in @cody's answer. Sam Speight worked under the supervision of Steve Awodey to see what can be achieved in HoTT using an ...
  • 28.4k
8 votes
Accepted

Reducing products in HoTT to church/scott encodings

The standard reference I often give is Induction is not derivable in second order dependent type theory by Herman Geuvers, which says that there is no type $$N : \mathrm{Type}$$ with functions $$Z:N\...
  • 7,754
8 votes
Accepted

Show how lack of universe levels would create contradiction in homotopy type theory (in Agda)

The problem is not specific to homotopy type theory. In type theory in general, if there is a type of all types, then every type is inhabited. This was shown first by Girard who encoded the Burali-...
  • 28.4k
7 votes
Accepted

Flawed argument in the proof of function extensionality in cubical type theory?

The expression: \(a : A) -> (p a) @ 0 parses as: \(a : A) -> ((p a) @ 0) So this is applying ...
  • 2,155
7 votes

Is path induction constructive?

I'm no HoTT person, but I'll throw in my two-cents. Suppose we are wanting to make a function $$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$$ How would we do this? Well, suppose we're given any ...
6 votes
Accepted

Constructing a sphere ($S^2$) in HoTT directly?

This was asked once on the HoTT-cafe list. The answer is "yes" and I composed a short video which explains exactly how this happens.
  • 28.4k
6 votes
Accepted

What types are propositions?

The original conception of propositions-as-types did not distinguish propositions and types at all: all types are propositions. Under this view, we may indeed speak of different proofs of a ...
  • 28.4k
5 votes
Accepted

How is functional property guaranteed in type theory when function type is defined?

Type theory shows that every element of a function type has the "function property". Let $A$ be a type and $B(x)$ a dependent type with $x : A$. We can construct an element of $$\Pi (x : A) (y , z : B(...
  • 28.4k
5 votes
Accepted

Continuing the example of why it's hard to compute with univalence?

You are correct, in the sense that the elusive computational nature of Univalence is not so elusive for "ordinary" type constructors. In fact, you might want to glance at Tabareau, Tanter and Sozeau'...
  • 7,754
4 votes
Accepted

How to understand equivalence of indexes of a family of types that are not definitionally equal

We can prove (x : Nat) (y : Nat) -> x + y = y + x (they are propositionally equal). I'm using Agda-ish notation here rather than the notation in the HoTT book ...
4 votes
Accepted

Why is reflexivity enough in this HoTT formulation of quotient types?

Your Quot construction is a set-truncated quotient by an arbitrary relation $R$ since you never use the reflexivity assumption in the construction. That is, you don'...
  • 28.4k
4 votes
Accepted

Unordered pairs in Homotopy Type Theory

The type of unordered pairs in a type $A$ is defined to be $$\sum_{(X:\mathcal{U})}\sum_{(H:\|X\simeq \mathsf{bool}\|)}A^X.$$ In other words, an undordered pair in $A$ is simply a map $X\to A$ from a ...
  • 171
3 votes
Accepted

Propositional truncation of excluded middle

The only way to prove ∥ X ∥ is to prove X (unless you admit some other axiom). So, assuming P is a proposition, there is no way to prove ∥ ((A) ⊎ (¬ A)) ∥ if you cannot prove ((A) ⊎ (¬ A)). It is not ...
  • 236
3 votes
Accepted

Identity types and universes

In general cummulative universes are a bit nasty. To see what is really going on, at the very least it makes sense to have explicit lifting maps $\mathsf{lift}_{i,j} : \mathcal{U}_i \to \mathcal{U}_j$ ...
  • 28.4k
3 votes

How is functional property guaranteed in type theory when function type is defined?

Set theory does not have functions. Instead, we can model functions via special relations (i.e. sets of pairs). When we write $f(x)=y$ in a set-theoretic context, what this actually means is $(x,y)\in ...
3 votes

Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory

The original statement in my question sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso)) is a valid statement in Homotopy Type Theory but because (...
  • 91
3 votes

Is path induction constructive?

I'm an amateur HoTT guy, so I'll try to complement Moses' already great answer. Let me take the type $A\times B$ as an example. The basic principle of constructive type theory, as outlined by Martin-...
  • 7,754
3 votes

Can I have a "dependent coproduct type"?

I'll talk about this more software-engineering-ly. Are you talking about a coproduct type whose latter constructors can refer to prior ones (which, looks pretty similar to a product whose latter ...
  • 888
3 votes

When do we need U(n+2) to solve a problem that can be formulated in U(n)?

This question on the theoretical CS stack exchange asks if pentation is implementable on Church numerals in a predicative variant of System F. In the normal, impredicative system, this is quite easy, ...
  • 2,155
3 votes
Accepted

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

You ask if we could derive a more efficent way to compute even? Yes, we could of course. The point however is that compilers could not. Having a compiler ...
  • 28.4k
3 votes

What are the implications of Homotopy Type Theory?

I won't lie: I don't understand the homotopy part of homotopy type theory. But I have a decent grasp of Univalence, which is the axiom at the heart of Homotopy Type Theory (HoTT). The main idea of ...
  • 29.2k
3 votes

What are the implications of Homotopy Type Theory?

I think the best way to understand why homotopy type theory related stuff is interesting from a computer science perspective is that is a more satisfying account of extensional equality than any prior ...
  • 2,155
3 votes

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

Agda is definitely the better choice if you're doing Homotopy Type Theory. Idris has several features that are specifically incompatible with HoTT. Specifically, you can use dependent pattern ...
  • 29.2k

Only top scored, non community-wiki answers of a minimum length are eligible