This is a thread to discuss the HoTT book [spoiler: https://hott.github.io/book/hott-online-1353-g16a4bfa.pdf]. It doesn't require any prerequisite materials as it aims to be an informal (yet informative, we just abstract away context dependency and a few details) introduction to homotopy type theory :D I suggest we start with chapter 1 which is about MLTT (martin löf's dependent type theory).

P23717
>I suggest we start with chapter 1 which is about MLTT (martin löf's dependent type theory).
Sounds like a reasonable place to start. This chapter is mostly stuff I'm already familiar with from working with Coq, but I'll look through it. From the last time I was looking at this book, I recall the stuff about equality types being a bit tricky and deserving some special attention.

P2371
>I recall the stuff about equality types being a bit tricky and deserving some special attention.
As far as I understand, the notion of equality is said to be « intensional » if it distinguishes objects based on their particular definitions, and « extensional » if it does not distinguish objects that have the same observable behaviour.
While [tex: x \equiv y] is an intentional equality, meaning that x and y essentially have the same semantical definition, the propositional equality [tex: x =_{A} y] is more of an extensional equality. Therefore, exntensional type theory is so named because it does not admit any purely intensional equality by assuming a reflection rule that enforces the judgement equality to coincide with the more extensional identity type
[tex: \frac{\Gamma \vdash p : Id_{A}(x, y)}{\Gamma \vdash x \equiv y}

Regarding MLTT, we can see that
* In its intensional form, it has sufficient computational content to function as a programming language.
* At the same time, it has identity types whose presence shows that one is really dealing with a form of HoTT.

Now what I found quite confusing is that we exploit the fact that every type is an [tex: \infty]-groupoid, with the structure of morphisms, 2-morphisms, 3-morphisms, ... given by the identity type propositional (therefore extensional) equality.

I think it may be important to develop the actual inductive construction of the identity (which is ver elegant, beautifully simple, but far from trivial !)
The situation where two elements can be identified in possibly more than one way is analogous to the situation in homotopy theory where two points of a space can be connected in more than path.
Indeed, for any two points x, y in a space, there is a space of paths from x to y. Moreover, between any two paths from x to y there is a space of homotopies between them, and so on.

Consider a type A and let a : A. Then we define the [bold: identity type] of A at a as an inductive family of types [tex: a =_{A} x] indexed by x : A, of which the constructor is given by the introduction rule

[tex: \frac{\Gamma \vdash a : A}{\Gamma, x : A \vdash a =_{A} x type}], [tex: \frac{\Gamma \vdash a : A}{\Gamma \vdash refl_a : a =_{A} a}].

The induction principle then asserts that in order to prove something about all identifications of a with some x : A, it suffices to prove this assertion about [tex: refl_a] only.

[tex: \frac{\Gamma \vdash a : A\hspace5ex \Gamma, x : A, p : a =_{A} x \vdash P(x, p) type}{\Gamma \vdash ind-eq_a : P(a, refl_a) \rightarrow \prod_{x : A} \prod_{p : a =_{A} x} P(x, p)}]

I forgot to mention computation rule ^^'

[tex: \frac{\Gamma \vdash a \Gamma, x : A, p : a =_{A} x \vdash P(x, p) type}{\Gamma, u : P(a, refl_a) \vdash ind-eq_a(u, a, refl_a) \equiv u : P(a, refl_a)}]


------------------------------------------------------------------------------------

We can then show that identifications can be [bold: conatenated] and [bold: inverted], which actually corresponds to the transitivity and symetry of the identity type.

Let A be a type. We define concatenation operation as the following
[tex: concat : \prod_{x, y, z : A} (x = y) \rightarrow (y = z) \rightarrow (x = z)].
and we will write [tex: p \cdot q] for concat(p, q).

[bold: Proof] : We first construct a function
[tex: f(x) : \prod_{y : A} (x = y) \rightarrow \prod_{z:A} (y = z) \rightarrow (x = z)]
for any x : A. By the induction principle for identity types, it suffices to construct
[tex: f(x, x, refl_x) : \prod_{z : A} (x = z) \rightarrow (x = z)]. Here we have the function [tex: \lambda z.id_{(x=z)}].

The function f(x) we obtain via identity elimination is explicitely thus defined as
[tex: f(x) :\equiv ind-eq_x(\lambda z.id) : \prod_{y : A} (x = y) \rightarrow \prod_{z : A} (y = z) \rightarrow (x = z)].

To finish the construction of concat, we swap the order of the third and fourth variable of f, i.e., we define
[tex: concat_{x, y, z}(p, q) :\equiv f(x, y, p, z, q)].

------------------------------------------------------------------------------------

Want another example ?
Ok, let A be a type. We define the [bold: inverse operation]
[tex: inv : \prod_{x, y : A} (x = y) \rightarrow (y = x)].
Most of the time, we will write [tex: p^{-1}] for inv(p).

[bold: Proof] : By the induction principle for identity types, it suffices to construct [tex: inv(refl_x) : x = x], for any x : A.
Here we take [tex: inv(refl_x) :\equiv refl_x].

P23926
I think the first time I was looking at this book I started by completely skipping the first chapter, and then only went back to look at the equality stuff because they were using it in a way that I wasn't familiar with.

In particular the identity type found in Coq's standard library is an inductive type with these constructors, and Coq automatically generates a theorem

eq_rect
: forall (A : Type) (x : A)
(P : A -> Type),
P x -> forall y : A, x = y -> P y

which is similar to the induction principle given in the book, but is missing the part where proofs about [tex: refl_a] turn into proofs about any witness of [tex: a =_A x], and is basically just the familiar substitution principle.

It is however possible to prove the book's version of the induction principle about Coq's identity type:

Definition path_induction
(A : Type)
(C : forall x y : A, x = y -> Type)
(c : forall x : A, C x x (eq_refl x))
(x y : A)
(p : x = y)
: C x y p
:=
match p with
| eq_refl => c x
end.

And the expected computation rule also works:

Variable A : Type.
Variable C : forall x y : A, x = y -> Type.
Variable c : forall x : A, C x x (eq_refl x).
Variable x : A.
Eval compute in path_induction A C c x x (eq_refl x).

Coq responds:
= c x
: C x x eq_refl

my prof cowrote that

P24112
Cool. What class did you have him for?

P24132 My guess is Cookery

>Note that from any function f : A → B, we can construct a lambda abstraction function λx. f(x). Since this is by definition “the function that applies f to its argument” we consider it to be definitionally equal to f:

>f ≡ (λx. f(x))

>This equality is the [bold: uniqueness principle for function types], because it shows that f is uniquely determined by its values.

The last remark confuses me a little, because it sounds like functional extensionality (if f(x) = g(x) for all x, then f = g), but I know Coq has the rule above (iota conversion) but if you want functional extensionality, you have to assume it as an axiom.

P23974
I think there is a similar situation with agda.
Agda's pattern matching machinery already implies the existence of a path-induction primitive

data Id {i : Level} {A : UU i} (x : A) : A → UU i where
refl : Id x x


ind-Id :
{i j : Level} {A : UU i} (x : A) (B : (y : A) (p : x ＝ y) → UU j) →
(B x refl) → (y : A) (p : x ＝ y) → B y p
ind-Id x B b y refl = b


P24164
Actually, while the rules of dependent type theory are sufficient to characterize the identity types, [tex: \sum]-types and of [tex: \mathbb{N}], there are still two important characterizations of identity types missing: those of [tex: \prod]-types and those of universes. For those two cases we need axioms:

>The function extensioanlity axiom just tells you that given a type A and type family [tex: B : A \rightarrow U], we expect the type f = g of paths from from f to g in [tex: \prod_{x:A} B(x)] to be equivalent to the type of pointwise paths:
>[tex: (f = g) \simeq (\prod_{x:A} (f(x) =_{B(x)} g(x)))].
and
>For any two types A and B in a universe U, the canonical map [tex: (A =_{U} B) \rightarrow (A \simeq B) that maps [tex: refl_A] to the identity equivalence, is an equivalence.
These two axioms are the basis in which univalent foundations are built on.
The function extensionality axiom is used to derive many important properties in type theory. One class of such properties are (dependent) universal properties.
Universal propertiesgive a characterization of the type of function into, or out of a type. For example, the universal property of the coproduct A + B characterizes the type of maps [tex: (A + B) \rightarrow X] as the type of pairs of maps (f, g) consisting of [tex: f : A \rightarrow X] and [tex: g : B \rightarrow X], i.e., the universal property of the coproduct A + B is an equivalence
[tex: ((A + B) \rightarrow X) \simeq (A \rightarrow X) \times (B \rightarrow X)].
Therefore, we will need function extensionality in order to construct the homotopies witnessing that the inverse map is both a left and right inverse.

At this point, it is important not to confuse the above function extensionality axiom with
[tex: \frac{\Gamma, f : A \rightarrow B,\quad g : A \rightarrow B,\quad x : a \vdash f(x) \equiv g(x)}{f \equiv g}]extensionality-rule
which is derived using [tex: \eta]-reduction.
[tex: \eta]-conversion converts between [tex: \lambda x.f(x)] and f whenever x does not appear free in f.
[tex: \frac{f : A \rightarrow B}{f \equiv (\lambda x:A.f(x)}].

I was wondering if there was any judgmental equality we can prove in the empty context with [tex: \eta]-conversion that we can't do with just [tex: \beta]-conversion, but think I answered my own question. An example, if I'm not wrong would be:

[tex: (\lambda (A : U) (f : A \to A) (x : A) . f x) \equiv (\lambda (A : U) (f : A \to A) . f)]

P24229
>At this point, it is important not to confuse the above function extensionality axiom with
>[tex: \frac{\Gamma, f : A \rightarrow B,\quad g : A \rightarrow B,\quad x : a \vdash f(x) \equiv g(x)}{f \equiv g}]extensionality-rule
>which is derived using [tex: \eta]-reduction.
That's a helpful way to put it. The [tex: \eta]-reduction version works with judgmental equality [tex: \equiv] while the funcional extensionality axiom works with propositional equality =.

I am trying to make my mind on whether decidability of type-checking is a desirable, important or essential property that a type theory may have or not.
I am thinking in particular about type theories implemented/implementable in computer systems for proof-checking and software verification. If I understand correctly, type-checking is decidable in Coq and Agda, and it is not in Nuprl and Lean.
From a programming point of view, it seems that having an algorithm that checks whether a given program has indeed the type that is has been assigned is pretty fundamental. From a logical point of view, similarly, if we think of elements of some types as proofs of propositions, checking whether a given proof lives in the desired type, seems also fundamental.
But in both cases there are also derivations of these judgements, and perhaps correctness of a derivation is decidable even when type-checking is undecidable.
If anyone has useful references or has clear thoughts about this issue, I'd be happy to know.

URL changed: https://hott.github.io/book/hott-online-1355-g95ed534.pdf

Still reading through this thing slowly. Most of the stuff in the first chapter isn't new to me, but sometimes I've been introduced to ideas I wasn't aware of, like uniqueness principles, so it's been worth looking through the material.

Pic related (p. 38), though it's not new to me, feels worth a post.

2 + 2
≡ succ(succ(0)) + succ(succ(0))
≡ succ(succ(0) + succ(succ(0)))
≡ succ(succ(0 + succ(succ(0))))
≡ succ(succ(succ(succ(0))))
≡ 4

And all without going through hundreds of pages of Whitehead and Russell! (For a comparison to ZFC instead, Enderton's Elements of set theory covers addition of natural numbers on page 79.)

P27283
I don't know about Principia Mathematica, but I think recent construction of [tex: \mathbb{N}] in modern set theory relies on the Von-neuman definition of ordinals (which can be considered as a generalization of natural numbers anyway).
In ZFC, the natural numbers are defined inductively by letting 0 = {} be the emptyset and [tex: n+1 = n \cap {n}] for each n. In this way n = {0,1,...,n-1} for each natural number n. The set [tex: \mathbb{N}] is then defined in this system as the smallest set containing 0 and closed under the successor function defined by [tex: S(n) = n \cap {n}] (you could also say that the structure [tex: (\mathbb{N}, 0, S)] is a model of PA in some sense).
It is also quite known that the axiom of infinity states that the proper class of natural numbers form a set.
Back to type theory (supposed to assume identification types, function types, and dependent sequence types), I think this definition works in a similar way : the natural numbers type is the inductive type generated by an element, a function and induction. In particular, addition is defined by double induction on the natural numbers.

----
Actually, we have a much more powerful result from this
>In the form of a natural numbers object, the axiom of infinity generalizes to the existence of inductive types or W-types.

!P27283
You could check out the Church-encoding chapter in any Lambda Calculus book for this as well btw