I am just getting started with homotopy type theory. After watching an introductory lecture, I was attracted to the concept of proof relevance. In my understanding, the core idea here is to elevate proofs to first class mathematical objects. In standard HOTT, the proof relevance is achieved by viewing proofs as paths. This then gets a bit complicated when you start to consider the case where the proof is going between different types and then you have to bring in the idea of dependent types.
It turns out that I have a whole research program that is trying to do something similar to HOTT in science where experiments are given a first class mathematical object. No one cares about this program, but it is my pet project. It sounds a little similar to the HOTT situation if you consider experiments to be the “proofs” of conjectures in science. In any case, the first class objects I consider for my experiments seem to be monads.
From there, I started to wonder if there was a way to expand HOTT so that proof relevance is supported by mathematical objects other than paths. Of course, I had to make life difficult and wanted to jump straight to monads. To this end, I just did a little research on the standard ways that HOTT is being expanded with different types of proof relevance. I found some literature about directed paths. Then I found a paper where proof relevance was handled by spans. That is as far as I got. In the case of going to directed paths for proof relevance, it sounds a little like monads, in the sense that at the core of a monad is the functor which is a directed object. Beyond that, I have nothing.
Edit: I guess I am looking for a foundation with proof relevance in the style of HOTT except proof relevance is supported by monads.
Is there any literature that might lead in my direction?
