Archive for January, 2006

Fixpoints of Indexed Containers

Sunday, January 22nd, 2006

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…