Anders Mörtberg

It's some benchmarks for a paper that we don't want to ever break. How about having the general make target not build anything in Experiments but have the CI do?...

Are you aware of https://git.sr.ht/~jorge-jbs/theory-of-computation? I haven't really looked at the code yet, but it seems very much related to your suggestion

Btw, the place to discuss this is over on the Agda Zulip: https://agda.zulipchat.com/#narrow/stream/260790-cubical/topic/Theory.20of.20computation

Yeah, I totally agree that we need more CS applications of univalence and HITs. I only meant to refer the discussion about the particular formalization that I linked in my...

I fixed the conflicts. Will merge once the CI is finished

@MatthiasHu Can you please take a look at this :-)

> ```shell > cat test.agda > {-# OPTIONS --cubical #-} > open import Cubical.Foundations.Prelude > EOF > > nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/52dfed7b703e6294b7acd11244cd838480839367#agdaWithCubical > > agda -l cubical -i...

Is this ready to be merged now? @MatthiasHu Is there be anything us developers will have to do in the future for example when releasing a new version of the...

> > Is there be anything us developers will have to do in the future for example when releasing a new version of the library when there is a new...

> Also, whatever steps need to be taken could just be documented in [RELEASE.md](https://github.com/agda/cubical/blob/master/RELEASE.md) :) That would be great!