containers.v

Set Implicit Arguments.
Set Contextual Implicit.

Record container : Type := {
  shape : Type;
  pos : shape -> Type;
}.

Inductive ext (c : container) (a : Type) : Type := {
  this_shape : shape c;
  this_rec : pos c this_shape -> a;
}.

Inductive list_shape a :=
  | NilF : list_shape a
  | ConsF : a -> list_shape a.

Definition list_pos a (s : list_shape a) : Type :=
  match s with
  | NilF    => False (* no holes *)
  | ConsF _ => True  (* one hole x *)
  end.

Definition list_container a : container := {|
  shape := list_shape a;
  pos := fun s => list_pos s;
|}.

Inductive Fix (c : container) : Type := MkFix (ext c (Fix c)).