I am reading a nlab article about Matt Oliveri's computational logical framework. It introduces new type constructors such as $\textsf{Relax}$. I tried to read the author's justification for the introduction of $\textsf{Relax}$, but I can't understand it. The basic question is that the author didn't explain what amounts to a relax type $\textsf{Relax}(A)$ (for $A:\textsf{type}$). But the author does offer the inference rules:
Since the author Matt Oliveri says that it is based on his unpublished work, I cannot find any publication to consult. Can anyone take a look at this article and tell me what amounts to $\textsf{Relax}$?