Type theory friends: is there any work out there looking into the relationship between indexed inductive types and inductive recursive types?
Conversation
For the specific use case I’m interested in, it seems like I can translate one into the other with wrapper types, but I’m curious if there’s anything more concrete. Both styles are convenient for different purposes.