Understanding the definition of Positivity Constraints in Coq In Interactive Theorem Proving and Program Development the authors explain constraints on constructors of inductive types in Coq.

For inductive type $T$, a constructor must have the form $t_1 \rightarrow t_2 \rightarrow ... \rightarrow t_l \rightarrow T a_1 ... a_k$ where $k$ is the number of arguments of the inductive type $T$.

There are some restrictions placed on the $t_i$s, which I cannot understand.


  If $t_i$ is the type of a constant, then $t_i$ can have the form "$g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k}),$" provided the expressions $b_{i,j}$ also satisfy the typing rules, and $T$ does not occur in these expressions or in $g$.


and 


  If $t_i$ is the type of a function, this type can have the form $t_1'\rightarrow ... \rightarrow t'_m \rightarrow g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$ but the type $T$ cannot occur in the expressions $t'_1, ... t'_m$ or in the expressions $b_{i,j}$


I am confused on what it means for a type $t_i$ "to have the form of $g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$". 

For instance, does nat (the type of natural numbers) have the form of $g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$"?

If so, how does nat obtain such a elaborate form? What is $g$ and what are the terms in the $(l,k)$ matrix $b_{i,j}$?

If not, am I prohibited from using nat in type constructors of inductive types? (That would seem absurd...)

Below I have uploaded a screenshot of the page in question.



Update: I was able to construct a counterexample to the textbook:

Definition g := fun x y z : Type =&gt; nat.

Inductive T : Set :=
  t : (g T T T) -&gt; T.


Here $l = 1, k = 0$, and $t_1$ can only have the form $g(T)$ but I was able to use $T$ 3 times inside an actual Coq environment.

Edit 2:
I think what you guys are saying about the reduced form makes sense so I tried to make another "counterexample"  

Inductive g (x y z: Type) : Set.

Inductive T : Set :=
  t : (g T T T) -&gt; T.
Take $l = k = 0$, the matrix of $b_{ij}$'s has size $0 \times 0$, hence we do not have to defined any $b_{ij}$, and take $g = \mathbf{nat}$.