Conjecture on irrelevant pathhood of interpreted ParamDTT types

About 9 years old · traced to

Let TT be a type that can be constructed in ParamDTT. Say that TT has irrelevant pathhood when weakening paths to bridges is injective:

(W,i:P)⊳t:T[γ⟩↦(W,i:B)⊳t\anglesi/i:T[γ(i/i)⟩.(W,\mathbf{i}:\mathbb{P})\mathrel{\rhd}t:T\left[\gamma\right\rangle\mapsto(W,\mathbf{i}:\mathbb{B})\mathrel{\rhd}t\angles{\mathbf{i}/\mathbf{i}}:T\left[\gamma(\mathbf{i}/\mathbf{i})\right\rangle.

Pathhood-irrelevance conjecture. The interpretation of any type that can be constructed in ParamDTT has irrelevant pathhood. This property is introduced to ensure injectivity of the operation sending t:Tt:T to t[κ]:T[κ]t[\kappa]:T[\kappa]. The source gives no proof or resolution of the conjecture.

References

Primary source

Andreas Nuyts, “A Model of Parametric Dependent Type Theory in Bridge/Path Cubical Sets”, arXiv:1706.04383 (2017).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.