This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the

This is standard notation. The `x : A` supposes a value, `x`, inhabiting a type `A` (like in Rust, or ML, or maybe `A x` in C). On the right hand side of the turnstile, we have `B(x) : Type`, which is roughly what it looks like: `B` is a type parameterised by `x` (note - it is not parameterised by `A`, but by `x`! It is allowed to know about the value `x`). The central turnstile is a contextual relation. The left hand side is an ambient known value, and the right hand side is something that be defined in that context. You can read it informally as "given", so this phrase is "given x: A, we can construct a type B(x)".