Positive inductive-recursive definitions

Update June 2017 for Agda development: Added introduction rules (bypassing Agda's checks for convenience), and worked out the details for the nested type Lam. Prompted by a question from Larry Diehl.

     author    = {Ghani, Neil and Malatesta, Lorenzo and Nordvall Forsberg, Fredrik},
     title     = {Positive Inductive-Recursive Definitions},
     journal   = {Logical Methods in Computer Science},
     volume    = {11},
     number    = {1},
     year      = {2015},
     doi       = {10.2168/LMCS-11(1:13)2015},
Last modified: Sun 25 Jun 19:34:02 UTC 2017.