Martin Escardo on Nostr: npub1jd874…vt4jc May I say, without trying to offend anybody, the cubical type ...
npub1jd874v63430gng67kpw5m597f34dr9vr0yhkp8dkmnma8208rayscvt4jc (npub1jd8…t4jc) May I say, without trying to offend anybody, the cubical type theory feels like assembly language for homotopy theory?
As I discussed earlier here, I am glad it exists because I can use it to compute if I want to. But I prefer to write high-level code in the style of HoTT/UF, in Agda, knowing that the assumptions I make (univalence, HIT's) are implemented in cubical Agda and so I can supply them as inputs to my high-level proofs.
Also, at the moment, cubical type theory is not "portable": it applies to particular models rather than all models.
As I discussed earlier here, I am glad it exists because I can use it to compute if I want to. But I prefer to write high-level code in the style of HoTT/UF, in Agda, knowing that the assumptions I make (univalence, HIT's) are implemented in cubical Agda and so I can supply them as inputs to my high-level proofs.
Also, at the moment, cubical type theory is not "portable": it applies to particular models rather than all models.