Follow

What if I took your — I mean, what if I took *my* — perfectly good Cubical Agda, and... made it suck? Just, make it the worst type theory ever? Coming soon (by which I mean probably never), agda --xtt

@amy I mean, I would unironically use this. I'm in the middle of a major development that makes extensive use of guardedness and quotients and dependent paths not a drop of glue. But there are a *ton* of places where things would be so much easier if I could just pattern match on refl or at least assume UIP.

I suspect I'm not alone. Guardedness is super helpful for doing logical relations in PL theory and modelling non-terminating things. Dependent paths are a really nice way to handle equalities between dependent pairs. Quotients are handy for reasoning about things modulo a normal form without having to actually compute that normal form. And there are lots of uses that don't need groupoids or paths between paths.

Like I don't think XTT is a replacement for ZFC but it could certainly be *useful* :)

@joey like you're not going to be able to match on paths in this any more than you would in ordinary cubical agda. also, did I mention XTT sucks? go use --cubical --with-K with Cubical.Data.Identity or whatever, this is never seeing the light of day

@amy You can't match on paths but you at least get that transport is the identity for loops. There's a bunch of times where, for withK, you'd match on refl to get rid of transport in your goal, where here it would be gone once you used J.

Is --cubical --with-K a thing? I didn't realize, I thought it implied --without-K.

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.