3 ms·
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
by TheAsprngHacker 6y ago
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?).
- m_j_g 6y agoThere 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.