VV in Scientific American
27 views
Skip to first unread message
Steve Awodey
Oct 3, 2013, 5:25:08 PM10/3/13
to homotopyt...@googlegroups.com, univalent-foundations@googlegroups.com Foundations
Michael Shulman
Oct 3, 2013, 5:56:31 PM10/3/13
to Harley D. Eades III, Steve Awodey, homotopyt...@googlegroups.com, univalent-foundations@googlegroups.com Foundations
I would think the difference between MLTT and CIC is so technical as
to be irrelevant for an article at this level. I'm more bothered by
the misleading juxtaposition
"Georges Gonthier, for example, spent a decade checking the four-color
theorem. But this approach circumvents all that labor."
On Thu, Oct 3, 2013 at 2:42 PM, Harley D. Eades III
<harley...@gmail.com> wrote:
> Very cool!
>
> I like seeing words like "type theory" in a mainstream blog.
>
> There is one funny sentence though:
>
> "And that last one — Coq — he couldn’t understand.
> It was based on something called Martin-Löf type theory, and he just
> couldn’t get his head around it."
>
> All this time I was thinking it was CIC. :-P
>
> .\ Harley
>
> On Oct 3, 2013, at 4:25 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
>
> http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
to be irrelevant for an article at this level. I'm more bothered by
the misleading juxtaposition
"Georges Gonthier, for example, spent a decade checking the four-color
theorem. But this approach circumvents all that labor."
On Thu, Oct 3, 2013 at 2:42 PM, Harley D. Eades III
<harley...@gmail.com> wrote:
> Very cool!
>
> I like seeing words like "type theory" in a mainstream blog.
>
> There is one funny sentence though:
>
> "And that last one — Coq — he couldn’t understand.
> It was based on something called Martin-Löf type theory, and he just
> couldn’t get his head around it."
>
> All this time I was thinking it was CIC. :-P
>
> .\ Harley
>
> On Oct 3, 2013, at 4:25 PM, Steve Awodey <awo...@cmu.edu> wrote:
>
>
> http://blogs.scientificamerican.com/guest-blog/2013/10/01/voevodskys-mathematical-revolution/
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
Steve Awodey
Oct 3, 2013, 6:17:23 PM10/3/13
to Michael Shulman, Harley D. Eades III, homotopyt...@googlegroups.com, univalent-foundations@googlegroups.com Foundations
On Oct 3, 2013, at 10:56 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> I would think the difference between MLTT and CIC is so technical as
> to be irrelevant for an article at this level. I'm more bothered by
> the misleading juxtaposition
>
> "Georges Gonthier, for example, spent a decade checking the four-color
> theorem. But this approach circumvents all that labor."
>
S
Reply all
Reply to author
Forward
0 new messages