What is Nostr?
Martin Escardo /
npub1t3n…g3z4
2023-09-02 16:19:56
in reply to nevent1q…79fy

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.
Author Public Key
npub1t3n4le6kr3f09s823keer5kr53j4d0kf50q2fd83pu35lcpltr9q0fg3z4