Meaning of the notation Typ := TVar | (Typ → Typ)

In the paper "introduction to type theory" by Herman Geuvers, it states the following definition for the type theory of propositional logic (I've added "convention 2" just for reference):



Given that this is an introduction, I'd assume that he would explain the meaning of a statement like $\mathrm {Typ}:=\mathrm {TVar}|(\mathrm {Typ}\to \mathrm {Typ})$, or what a "type variable" is.

My question is twofold:

-
What do these two things mean?

-
What background knowledge is this introduction assuming, that I would need to study before reading this "introductory" text?

Intuitively, a type variable is like a variable in an expression, except that it stands in for a type rather than standing in for a number/bitstring/etc.

Formally, we choose a countably infinite set $\mathsf{TVar}$, and then define a type variable to be a member of $\mathsf{TVar}$.

The notation $\mathsf{Typ}:=\mathsf{TVar}|(\mathsf{Typ}\to \mathsf{Typ})$ is an instance of Backus normal form. It is an inductive definition of $\mathsf{Typ}$. It says that if $\alpha$ is a type variable (i.e., if $\alpha \in \mathsf{TVar}$), then $\alpha$ is an element of $\mathsf{Typ}$; and if $\alpha,\beta$ are type variables (i.e., $\alpha,\beta \in \mathsf{TVar}$), then the term $\alpha \to \beta$ is an element of $\mathsf{Typ}$. $\mathsf{Typ}$ is the set of terms that can be constructed in this way. We call a term a type if it is an element of $\mathsf{Typ}$.

StackExchange Computer Science Q#91362, answer score: 7