coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: 1337 777 <1337777.net AT gmail.com>
- To: "Prof. Vladimir Voevodsky" <vladimir AT ias.edu>, coq-club AT inria.fr
- Cc: kosta AT mi.sanu.ac.rs, zpetric AT mi.sanu.ac.rs, categories AT mta.ca
- Subject: Re: [Coq-Club] 2016-2017 at the IAS
- Date: Wed, 20 Jan 2016 12:37:02 -0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=1337777.net AT gmail.com; spf=Pass smtp.mailfrom=1337777.net AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f181.google.com
- Ironport-phdr: 9a23:IdvZlRb/sb1FHn41mNkr1Bv/LSx+4OfEezUN459isYplN5qZpMy+bnLW6fgltlLVR4KTs6sC0LqI9fm4ACdbvN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDsvcSLOk4T2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIszEkSGIY1FJ2BwHJ7RT7RN/PtSbkseZm2zjQdZnoSbk4WDGj9Y9qQQSuhSsaYXpx+2bOz8d0kahzoRS7phU5zZSHTpuSMa8nJfiCNYxFGiIVB50KCHMeXcW6YpcnAO8IPOIepI748Qhd5SCiDBWhUbu8ggRDgWX7iOhji7ws
Proph Voevodsky
https://github.com/1337777/dosen/blob/master/dosenSolution.v
propose some alternative alongside the Univalent Foundations : the Solution Programme.
___
Short : some Coq program of the termination technique of the oriented equations of adjunction as presented by Dosen [1]. For example, (counit f <o reflection (unit g)) ~> (f <o reflection g), which is the polymorphic (Yoneda) terminology of the common equations. And the confluence technique and links-model resolution technique for semiassociativity and associativity was already programmed and simultaneously-edited and timed-tutored in [2] and [3]. These Coq programs use dependent types to encode source-target functions and use inductives to encode grammatical (free) generations of adjunctions.
The Solution Programme lacks to extend and mix these automation programming techniques into the enriched-lax monoidal topology (Tholen's TV) or the n-fold-lax categorial homotopy (Riehl's Kan-obsession) or the dissociativity technique (Dosen's boolean categories and linear logic) or the compositional automation technique (Chlipala's ?functorial? MirrorShard)... ultimately this may converge to the descent technique of Galois. The Solution Programme initiated by Gentzen lacks to comprehend things in different « terminologies » or « formulations » or « coordinates ». This angle of view was continued by Lambek into categories, then by Kelly, then by Dosen-Petric. Einstein's single deepest angle of view was about « coordinates », even before the « spin » or the « entropy » ...
[1] Dosen, «Cut Elimination in Categories» In: https://books.google.com/books?isbn=9401712077
[2] 1337777.net, «MACLANE PENTAGON COHERENCE IS SOME RECURSIVE COMONADIC DESCENT» In: Studies in Logic, SYSU
[3] 1337777.net, «1337777.info»
____
We at 1337777.net Solution Programme Seminar will be present alongside the Univalent Foundations seminar this May 16-20 summer in the grass fields alongside the fields institute, may you visit us to present some of your questions ? « mais sans plus guère aller chercher la rime, si elle ne vient d’elle-même »
https://github.com/1337777/dosen/blob/master/dosenSolution.v
propose some alternative alongside the Univalent Foundations : the Solution Programme.
___
Short : some Coq program of the termination technique of the oriented equations of adjunction as presented by Dosen [1]. For example, (counit f <o reflection (unit g)) ~> (f <o reflection g), which is the polymorphic (Yoneda) terminology of the common equations. And the confluence technique and links-model resolution technique for semiassociativity and associativity was already programmed and simultaneously-edited and timed-tutored in [2] and [3]. These Coq programs use dependent types to encode source-target functions and use inductives to encode grammatical (free) generations of adjunctions.
The Solution Programme lacks to extend and mix these automation programming techniques into the enriched-lax monoidal topology (Tholen's TV) or the n-fold-lax categorial homotopy (Riehl's Kan-obsession) or the dissociativity technique (Dosen's boolean categories and linear logic) or the compositional automation technique (Chlipala's ?functorial? MirrorShard)... ultimately this may converge to the descent technique of Galois. The Solution Programme initiated by Gentzen lacks to comprehend things in different « terminologies » or « formulations » or « coordinates ». This angle of view was continued by Lambek into categories, then by Kelly, then by Dosen-Petric. Einstein's single deepest angle of view was about « coordinates », even before the « spin » or the « entropy » ...
[1] Dosen, «Cut Elimination in Categories» In: https://books.google.com/books?isbn=9401712077
[2] 1337777.net, «MACLANE PENTAGON COHERENCE IS SOME RECURSIVE COMONADIC DESCENT» In: Studies in Logic, SYSU
[3] 1337777.net, «1337777.info»
____
We at 1337777.net Solution Programme Seminar will be present alongside the Univalent Foundations seminar this May 16-20 summer in the grass fields alongside the fields institute, may you visit us to present some of your questions ? « mais sans plus guère aller chercher la rime, si elle ne vient d’elle-même »
- Re: [Coq-Club] 2016-2017 at the IAS, 1337 777, 01/20/2016
Archive powered by MHonArc 2.6.18.