Timeline for Monads for proof relevance in type theory
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 11 at 14:48 | comment | added | Ben Sprott | @DavidRoberts Your comment is well taken David. I am in no position to start some big project. I am just learning. I have the HOTT book and am looking at the identity types section. | |
| Apr 11 at 0:55 | comment | added | David Roberts♦ | 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. | |
| Apr 10 at 14:39 | comment | added | Ben Sprott | @DavidRoberts Hi David, very good to see you commenting. My thought about your comment was this: science has a restricted form of reasoning and a restricted form of natural language (which encapsulates in a "tight" way the reasoning). So, maybe not all concepts are what I am after, just the ones that are relavant to science. Sorry about the hand wavey-ness, but a smaller fragment is fine for me and I might be able to show how that is expected. | |
| Apr 2 at 1:28 | comment | added | David Roberts♦ | @Ben Mac Lane might claim that all concepts might be Kan extensions, but I doubt that all concepts are monads. ^_^ | |
| Apr 1 at 22:12 | comment | added | Andrej Bauer | @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.) | |
| Apr 1 at 22:12 | comment | added | Andrej Bauer | @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). | |
| Apr 1 at 21:45 | history | edited | Ben Sprott | CC BY-SA 4.0 |
added 137 characters in body
|
| Mar 31 at 20:30 | comment | added | provocateur | Proofs have been first class mathematical objects since at least the early 20th century, so you don't need HOTT for that. | |
| Mar 29 at 15:11 | history | edited | YCor | CC BY-SA 4.0 |
formatting, added tag
|
| Mar 29 at 14:55 | history | asked | Ben Sprott | CC BY-SA 4.0 |