Desc@ICFP: motivate role of switchD
Desc@ICFP: motivate role of switchD

Reviewer 2 says:

"Also, in the implementation, I did not see anything resembling
"switchD", which makes me believe that the implementation does not
tell us anything about the soundness of the full system with "switchD"
in which levitation is possible."

To which we answered:

"Referee 23B asks how much is definable from a "vanilla" system and
advises us to bring our models into more light. As mentioned above,
Coq is problematic, but in Agda the news is rather better. We used
universe polymorphism to hardwire the Desc type at all levels, then
define the associated machinery as Agda programs. As referee #23A
observes, this is unsatisfactory because Agda's universe polymorphism
is underexplained (although it is distinctly conservative in
approach).  Moreover, the closest we get to levitation is to note that
an isomorphic copy of Desc(n) has a description in Desc(n+1). We have
effectively shown how, with care, to collapse that isomorphism."



mietek/epigram2,larrytheliquid/pigit,mietek/epigram2