When printing the signatures of the interface, I see
Inner.hcomp-T. Why is that generated without--cubical-compatible?
Test case:
module Inner where data T : Set where t : T
Running
agda-quicker Inner.agda -v 5 | grep hcomp
shows that cubical-related code is executed:
Generated name: [...] "hcomp-T" [...]
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4