1
$\begingroup$

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?

Improve this question
$\endgroup$
7
  • 2
    $\begingroup$ Proofs have been first class mathematical objects since at least the early 20th century, so you don't need HOTT for that. $\endgroup$
    – provocateur
    Commented Mar 31 at 20:30
  • 2
    $\begingroup$ @provocateur: well, yes, but not really. They have and still are considered to be syntactic objects, which would be a bit like thinking that functions are expressions with "x" appearing in them. Such a syntactic approach prevents the sort of mathematical development that one can achieve by going the extra step and abstract away from concrete representation (in the case of functions it leads to spaces of functions and functional analysis). $\endgroup$
    – Andrej Bauer
    Commented Apr 1 at 22:12
  • 2
    $\begingroup$ @BenSprott: not all proofs are "paths", only proofs of (propositional) equalities. So your question seems misguided. And also, at least one kind of proof relevance/irrelevance distinction is already studied in terms of monads, namely propositional truncation. (The relevant part of the HoTT book is the chapter on truncations and modal operators.) $\endgroup$
    – Andrej Bauer
    Commented Apr 1 at 22:12
  • 1
    $\begingroup$ @Ben Mac Lane might claim that all concepts might be Kan extensions, but I doubt that all concepts are monads. ^_^ $\endgroup$
    – David Roberts ♦
    Commented Apr 2 at 1:28
  • 2
    $\begingroup$ I think you need to have a solid understanding of proof relevance before thinking about how to model this with a monad. Respectfully, watching an introductory lecture will not equip you to do this. Proof relevance is not about paths, but about the behaviour of the identity type. From this sentence "it sounds a little like monads, in the sense that at the core of a monad is the functor which is a directed object." I get the feeling you have a solution in search of a problem. If this guess had any weight, then you could say that any morphism in any category is relevant because it's directed. $\endgroup$
    – David Roberts ♦
    Commented Apr 11 at 0:55

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .