I enjoyed the CPP talk yesterday about "Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda" (https://dl.acm.org/doi/10.1145/3779031.3779090) by @ltchen@mathstodon.xyz, @fnf@mathstodon.xyz and Tzu-Chun Tsai.
One of the problems mentioned was that Agda did not accept their definition of the eliminator as terminating. In my hubris, I thought I would have a go at trying to fix it, and got down to one remaining case (for set-truncation):
https://github.com/L-TChen/TTasQIIRT/blob/494d02ac2f28fa2575a611a45d5182c5e55885cc/src/Theory/SC/QIIRT-tyOf/Elim.agda#L216
(PR with all the changes: https://github.com/L-TChen/TTasQIIRT/pull/1)
The conceptual argument is simple: "Ty∙ is a set, so all Ty∙ paths are equal". Unfortunately, when constructing the type of the square, it seems that you need to recurse on elimTy with e.g. (λ j → elimTy (tyOf (p j)))
elimTy (tyOf t) can be justified by adding Ford (tyOf t) to the Tm-is-set path constructor where
data Ford {A : Set ℓ} : A → Set ℓ where
ford : {x : A} → Ford x
(i.e. taking advantage of how Agda considers dot patterns during structural termination checking).
I don't know how to replicate the same trick with tyOf (p j) though - especially as this j is not even bound in the original pattern. Ford (cong tyOf p) unfortunately does not work.
I guess one solution here could be to globally assume UIP (in --cubical=no-glue) and then get rid of the set truncation path constructors, but this feels somewhat unsatisfying. I would hope that there exists some way to make this work in ordinary --cubical (it is especially frustrating that this case is the only remaining problem, given it is "just" set truncation). If anyone has ideas how to fix it I would be very interested.