Hacker News Reader

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?).

View on HN

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.

Reply on news.ycombinator.com