syzygies

On the other hand, it should be perfectly valid to make your functor application compository. You just take your proposition ∃x:τ.P(x), and your more different propositions B |- C and M : ∃a.B, and you cross-project their modularity functions in the opposite order. So then you get:

module AppTable(B |- C const M : ∃a.B) : TABLE =
  struct
    type t:τ
    type x:τ.τ, y:2τ
    val π1M:τ = unpack(B   C)
    τ.τ.τ ? ∃a.B : throw new ModularityException();;
    let M unpack x in y with implicit(z)
    return M:τ
  end