The projection-term conjecture for lax cones in CaTT

Let $K$ be a cone over a diagram $\Gamma$ with apex $c$, and let $\Gamma \vdash t: A$ be a term of dimension $d$. Writing

$$K \equiv \Gamma, c: \operatorname{Ob}, \Pi,$$

assume that $\sigma$, $\tau$, $\operatorname{FV}$, and the operation $\ast$ have the meanings given by the CaTT syntax and the cone construction. Define $T_t$ recursively by

$$T_t=c\to t$$

when $\dim(t)=0$, and by

$$T_t=p_{\tau(t)}\to p_{\sigma(t)}\mathop{\ast}_{d-1}^{d}\Big(1_{p_{\sigma^2(t)}}^{1}\mathop{\ast}_{d-2}^{d}\Big(1_{p_{\sigma^{3}(t)}}^{2}\mathop{\ast}_{d-3}^{d}\dots\Big(1_{p_{\sigma^{d}(t)}}^{d-1}\mathop{\ast}_{0}^{d}t\Big)\Big)\Big)$$

when $\dim(t)>0$. Then there exists a term $p_t$ such that $K\vdash p_t:T_t$, and

$$\operatorname{FV}(p_t:T_t)=\bigcup_{\substack{p_{x_i}\in\operatorname{FV}(\Pi)\\ y\in\operatorname{FV}(t:A)\\ y\propto\tau(p_{x_i})}}\operatorname{FV}(p_{x_i}:T_{x_i}).$$

Projection-term conjecture. Under these hypotheses, there exists a term $K\vdash p_t:T_t$ with the recursively specified type $T_t$, and its free variables satisfy the displayed union formula.

This conjecture predicts a uniform construction of projection terms for arbitrary terms, including coherence terms, in the weak higher-categorical setting. The supplied text reports only low-dimensional evidence and gives no resolution status.