What you're describing here (and this again is my interpretation) sounds more similar to 'Homotopy Type Theory'. https://en.wikipedia.org/wiki/Homotopy_type_the

What you're describing here (and this again is my interpretation) sounds more similar to 'Homotopy Type Theory'. https://en.wikipedia.org/wiki/Homotopy_type_theory https://en.wikipedia.org/wiki/Homotopy_type_theory Homotopy Type theory also shows some deep connections between mathematics and programs, as the progress of the theory has bee characterised by building programmatic proofs _first_, to generate new mathematics. That's an inversion of the usual process.