Do you have any project ideas for Agda? I used it to formalize the simply typed lambda calculus; what else should I do? After all, I can't really do "traditional" programming projects in Agda as its ecosystem is more geared towards proving. Are there any interesting projects with proofs as a focus?
In fact I would be very happy to find a collaborator for those projects. There is lot of people from academia focused on the fundamental projects, but I am more focused in programming something practical.
Wow, cool! I'm still wrapping my head around Cubical Type Theory, so I'm not sure if I can help. I don't have the mathematical background to know what Matroids are (skimming the Wikipedia page, I see some set-theory-centric definitions that talk about subsets and powersets, to what extent would they translate to type theory?).
There is nothing special about them.
I am talking about simple formalisation, there is already some code about finite types in cubical-agda library, so it would be good place to start.
I think that usefull definitions and properties can be formalised in ~100h.
Matroids are known to be good example of cryptomorphic structures, so cubical agda can be used so that those cryptohmorphism can work "under the hood". I know how to do this, but I am currently working on something different.
If You are interested pm me.
