Exercise 7.3. Show that if A is an n-type and B : A → n-Type is a family of n-types, where n ≥ −1,
then the W-type W(a:A) B(a) (see §5.3) is also an n-type.
This is true regardless of whether B is a family of n-types: https://homotopytypetheory.org/2012/09/21/positive-h-levels-are-closed-under-w/.
This is true regardless of whether B is a family of n-types: https://homotopytypetheory.org/2012/09/21/positive-h-levels-are-closed-under-w/.