I was going to upload some whiteboard images of the basic constructions for fixpoints of indexed containers, but it won’t let me. I’ll link to them instead.
- least fixpoint uses W-types for the basic shape, then recursively defined notions of index-matching and input indexing; I didn’t use inductive families because that’s what we’re constructing, right?
- greatest fixpoint uses M-types for the basic shape, then inductively defined notions of O-indexed and I-indexed places. The index-matching condition is the property that in every O-indexed place, the O you want is the O you’ve got.
Of course, there’s some work to do to show that these things really are what I say they are, but I think they look about right.
By the by, we really need to figure out some notational issues or we’re heading for a mess…