functors.v

Require Vector.

Module Type NAT.
  Parameter n : nat.
End NAT.

Module A (N : NAT).
  Definition t : Type := Vector.t unit N.n.
End A.

Module B (N : NAT).
  Module Import AN := A N.

  Definition x : AN.t := Vector.const tt N.n.
End B.

Module C (N : NAT).
  Module Import AN := A N.

  Definition f : AN.t -> AN.t := Vector.map (fun x => x).
End C.

Module D (N : NAT).
  Module Import AN := A N.
  Module Import BN := B N.
  Module Import CN := C N.

  Check f x.
End D.