Computational Higher Type Theory IV: Inductive Types