Another possible target for the HoTT machine: Independence Friendly Logic.

Starting out with an untyped logic, it looks to express independence of quantifiers, e.g., branched quantifiers

$(\forall x)(\exists y)(\forall z)(\exists w/\forall x) R(x, y, z, w).$where $(\exists w/\forall x)$ means that $w$ is independent of $x$. Typing and functions should see to that.

]]>