17

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 ...


13

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 $$...


11

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 "...


11

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 \...


10

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 ...


8

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 ...


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

ℕ→ℕ-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.


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$. ...


7

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.


7

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\...


7

A year after and I'm writing one myself.


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.


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 ...


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

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 ...


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

The problem you are talking about is relevant not to HoTT itself, but rather to the construction of HoTT models. When we construct a model of HoTT in some category we have to choose a morphism for each functional constant that we defined, so that all stated relations hold. This choice is inherently non-unique, and this non-uniqueness of model (even within ...


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

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 ...


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

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

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

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 ...


2

I recommend that in addition to watching videos you also read some material which actually explains homotopy type theory. Some good sources are: The HoTT book, which is "the bible". If you are philosophically minded you might like this primer by James Ladyman & Stuart Presnell. It might not hurt to read on some basic notions in topology, where it is ...


2

In programming languages, we usually distinguish concrete syntax, where a program is represented as a linear list of symbols, from abstract syntax, where programs have a tree structure. The vast majority of PL theory, including most type systems, happens after parsing, working with abstract syntax. So, it's impossible to generate a parser simply from type ...


2

The induction principle for $=_{U_{i+1}}$ gives you a map $(A=_{U_{i+1}}B)\rightarrow (A=_{U_i}B)$. In HoTT without univalence, there is no map $(A=_{U_i}B)\rightarrow (A=_{U_{i+1}}B)$: indeed, you could assume the univalence axiom only for universe $U_i$. In that case, $A\simeq B$ gives you by univalence an inhabitant of $A=_{U_i}B$, but not of $A=_{U_{i+1}...


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