Timeline for Global elements in categories with no terminal object?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 7, 2016 at 21:43 | history | edited | Musa Al-hassy | CC BY-SA 3.0 |
as a night labourer i do Math for fun, at night and using similar exclaimation notation has led to a type error, which i have now fixed.
|
| Jul 7, 2016 at 21:06 | comment | added | Musa Al-hassy | please take another gander | |
| Jul 7, 2016 at 21:06 | history | edited | Musa Al-hassy | CC BY-SA 3.0 |
added requested explantions
|
| Jul 7, 2016 at 7:54 | comment | added | Philippe Gaucher | Could you say please what proof assistant you are using ? | |
| Jul 5, 2016 at 12:16 | comment | added | Marcus Pivato | Thank you very much for you response, Musa. However, I must admit that I do not understand most of your notation. I guess it comes from theoretical computer science? Perhaps it would help to answer the following question: once we unpack your notation, is your construction basically the same as Quiaochu's construction via the Yoneda embedding? | |
| Jul 5, 2016 at 9:44 | comment | added | Peter LeFanu Lumsdaine | Nice answer, but it would be quite helpful to add (a) a note explaining what formal language you are writing in, and (b) a translation into ordinary mathematical prose, so that mathematicians not familiar with computer formalisation can read it more easily. | |
| Jul 4, 2016 at 23:19 | comment | added | Qfwfq | What is $\mathbb{B}$? I guess it's some category of "truth values"? | |
| Jul 4, 2016 at 19:30 | history | answered | Musa Al-hassy | CC BY-SA 3.0 |