3 ms·

I currently need help with: - (you can make it your own project) type-safe library for Matroids (in cubical agda, so different representations can be handled a

by m_j_g 7y ago

I currently need help with: - (you can make it your own project) type-safe library for Matroids (in cubical agda, so different representations can be handled automatically) - If you have some Elm experience you can help me with online toy to play with cubical agda :) ( https://raw.githack.com/marcinjangrzybowski/cubeViz/master/main.html#assoc,assoc https://raw.githack.com/marcinjangrzybowski/cubeViz/master/m... 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.

TheAsprngHacker 7y 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 7y ago
  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.