# Tag Info

19

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 \times B$, because that does not require the boolean type to be defined first. The coproduct is a special case of dependent sum. Given types $A$ and $B$, consider ...

16

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 "define" it, but failed to observe that the same is true in other cases as well. Let us consider the induction principle for the unit type $1$, which seems particularly obviously "...

15

The question under what circumstances we need to jump from a universe to one higher in the hierarchy is a good one. Having the hierarchy and the ability to climb it is important. You need to jump levels when you want to treat a universe as a type or as part of a type. For example to define functions of (non-dependent) type $$A \rightarrow \mathcal{U}_i$$...

14

I will slightly amend Martin's answer to explain where cumulativity comes in (the rule which says that $X : \mathcal{U}_i$ and $i \leq j$ entail $X : \mathcal{U}_j$). Suppose we have $A : \mathcal{U}_{42}$ and we would like to give a type to $A \to \mathcal{U}_{99}$. The formation rule for $\to$ is this: $$\frac{\Gamma \vdash X : \mathcal{U}_i \qquad \Gamma \... 11 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 = g\ x) \Leftrightarrow f = g).$$Informally it means that if two functions are equal point-wise, then we consider them equal. Syntactically merge-sort and ... 10 ℕ→ℕ-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 ℕ→ℕ-undecidable. Since Agda is consistent with LEM, it follows that ℕ→ℕ-undecidable is not provable in base Agda. This holds the same for cubical and vanilla Agda. 9 it matches the Path pos 0 == neg 0 and returns pos 1 -- say, matches a Path, but returns a normal integer My understanding is that it matches points of path rather than path itself. This is why the matching is on posneg x (where x : I) rather than posneg itself. Since paths can be seen as (special) maps from I, we can think of HIT constructors as just a ... 9 A year after and I'm writing one myself. 9 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 programmer wanting to use the type theory to compute something. For instance, we might want to compute some natural number satisfying some specification we've come ... 8 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 impredicative universe, see Impredicative Encodings of Inductive Types in HoTT blog post. 8 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\qquad S:N\rightarrow N $$such that$$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\...

8

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-Forti paradox in type theory. A simplification of the paradox was found by Hurkens. Here is Agda code for it, and here is Coq code.

7

The expression: \(a : A) -> (p a) @ 0 parses as: \(a : A) -> ((p a) @ 0) So this is applying p a : Path B (f a) (g a) to the 0 point. This reduces to f a, because it is the beginning point of the path. It's essentially doing the same thing as the earlier step, which beta reduced the (<i> ...) @ 0 to (...)[i := 0], except p a looks abstract to ...

7

The book is itself representative of the research product of the program. The code that they wrote actually is mostly in Coq, to my knowledge, and certainly the development that accompanies the book was written in Coq. Homotopy Type Theory itself essentially constitutes Martin-Löf, together with the univalence axiom, which essentially states that equivalent ...

7

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 $x,y : A$ and a proof of their equality $p : x =_A y$. Since I know nothing about the arbitrary type $A$, I know nothing about the `structure' of $x,y$. ...

6

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.

6

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 proposition. One way to understand the differences between different conceptions of propositions-as-types is to view them as capturing different notions of provability ...

5

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(x)) \,.\, f x =_{B(x)} y \to f x =_{B(x)} z \to y =_{B(x)} z$$ quite easily, because we just use symmetry and transitivity of equality. For instance in Coq: ...

5

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's paper Equivalences for Free!, which outlines what you have just written, along with many more types of, well, types. Trouble starts (as usual!) with ...

4

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 because type setting is hard. Note that we can prove this in standard intensional type theory. This gives a function from Nat to Nat to a proof of equality. In intensional type theory we don't ...

4

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't even need the reflexivity of $R$ to perform the quotient and derive its basic properties. As the HoTT book explains in Section 6.10, it is perfectly possible to make set-truncated quotients by ...

4

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 type $X$ that merely has two elements. Note that in general, this is not a set, because the type of 2-element types is not a set but a 1-type. The way to think ...

3

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 f$. If $f$ was an arbitrary binary relation, there would be absolutely nothing stopping $(x,y)\in f$ and $(x,y')\in f$ with $y\neq y'$. By definition of set-...

3

The original statement in my question sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso)) is a valid statement in Homotopy Type Theory but because (homotopy-) isomorphisms are a special case of equivalences, the statement can be generalized to sym (ua fEquiv) ≡ (ua (invEquiv fEquiv)) (*) It is one of the properties of ua that are informally proven ...

3

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, because we have: ℕ : Type ℕ = forall (R : Type). (R -> R) -> (R -> R) 1 : ℕ 1 R s z = s z hyper : (ℕ -> ℕ -> ℕ) -> (ℕ -> ℕ -> ℕ) ...

3

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$ for $i \leq j$. With these in place, your question is: how do the types $$\mathsf{lift}_{i,i+1}(A =_{\mathcal{U}_i} B)$$ and $$(\mathsf{lift}_{i,i+1} A) =_{\... 3 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-Löf, is that *every element of A\times B is described as being in the image of the constructor:$$ \mathrm{pair}\ :\ A\rightarrow B\rightarrow A\times B This ...

3

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 fields can refer to prior ones)? This is possible in Agda after HIT is introduced (in version 2.6.0): -- Auxiliary definition: Nat data Nat : Set where zero : ...

3

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 a correct intuition that undecidable propositions are either true or false, just we do not know about it. A formal system S with an undecidable proposition P ...

3

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 automatically perform very fancy optimization techniques is a hard problem. In fact, if you ask for too much the problem may become undecidable, and for almost all interesting cases at least extremely hard....

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