Timeline for The groupoid of algebraic expressions and proofs
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20, 2015 at 13:45 | comment | added | Urs Schreiber | @goblin, that seems rather close in spirit to type theory ncatlab.org/nlab/show/type theory . In its flavors as homotopy type theory ncatlab.org/nlab/show/homotopy+type+theory this is precisely about groupoids whose morphisms are proofs of equivalences... and higher groupoids whose higher morphisms are proofs of equivalences of proofs of equivalences, and so on. | |
| Feb 13, 2015 at 15:49 | history | edited | Joel David Hamkins | CC BY-SA 3.0 |
added 408 characters in body
|
| Feb 13, 2015 at 15:45 | comment | added | goblin GONE | Interesting. There's definitely a strong connection there. | |
| Feb 13, 2015 at 15:33 | history | answered | Joel David Hamkins | CC BY-SA 3.0 |