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