Timeline for Enriched cartesian closed categories
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 11, 2019 at 5:06 | comment | added | David Roberts♦ | @MikeShulman link to your Coq proof? | |
| Feb 3, 2019 at 23:47 | comment | added | Mike Shulman | @მამუკაჯიბლაძე Passing to the presheaf category $[D^{\rm op},V]$ introduces all cotensors and the subcategory $C$ is closed under them, just like all other $V$-limits. | |
| Feb 3, 2019 at 22:44 | comment | added | მამუკა ჯიბლაძე | Is it obvious that having powers (that is, cotensors) will not require additional restrictions that would damage the counterexample? | |
| Feb 1, 2019 at 0:04 | comment | added | Mike Shulman | @FoscoLoregian The exercise is to do the proof. I found it helpful to use a proof assistant to assist me in doing the proof, and others might likewise. In particular, a 5-line tactic script in Coq was able to prove all 625 associativity equations automatically without any thought on my part, saving me a lot of work. (Do that in Agda! (-: ) In fact, when I first defined composition I made a couple of mistakes, so the proof of associativity failed and showed me where the mistakes were. But, if you'd rather write them all out by hand, be my guest. (-: | |
| Jan 31, 2019 at 21:46 | comment | added | fosco | Is the exercise about doing the computation without Coq, or rather about coding the proof in Coq? | |
| Jan 31, 2019 at 21:09 | comment | added | David Roberts♦ | Tip of the hat for the formal proof check that your category is what you claim it is! | |
| Jan 31, 2019 at 20:10 | history | edited | Mike Shulman | CC BY-SA 4.0 |
typo fix
|
| Jan 31, 2019 at 9:38 | history | answered | Mike Shulman | CC BY-SA 4.0 |