coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: 1337 777 <1337777.ooo AT gmail.com>
- To: awodey AT cmu.edu, francis.borceux AT uclouvain.be, categories AT mta.ca
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] 1-year teaching / research position
- Date: Sat, 28 May 2016 00:37:32 -0700
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=1337777.ooo AT gmail.com; spf=Pass smtp.mailfrom=1337777.ooo AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f65.google.com
- Ironport-phdr: 9a23:Lpqy5B9iubCZdf9uRHKM819IXTAuvvDOBiVQ1KB92+scTK2v8tzYMVDF4r011RmSDdSdt6MP0rCL+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U05X8jrrvs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtJTqL2crUQRrlFSjkqLiR96tfisxLCVk2F4WEXX3gGugdDBw/Y8hj7WNH7v2+yveNh1SadJ8z7VpgxRT3k5K44ZgXvjXJebGVmuD6I1YQk1fkA/03++Fp4xIn8b4ScNf44daTYK4BJDVFdV9pcAnQSSri3aJECWrIM
Proph
https://github.com/1337777/borceux/blob/master/borceuxSolution.v
1. Short: This [1] solves some question of Ahrens [2] and Kan-Riehl [3], which is how to program Kelly's <<enriched categories>> and how the inter-dependence of <<naturality>> with <<category>> is cyclic. Also This [4] attempts to clarify the contrast <<categorical algebra>> (ring/locale-presentation and its "internal logic"), from <<categorial logic>> in the style of the <<enriched/encoded/programmed/recursion>> categories of Kelly-Dosen or Lawvere-Lambek and as attempted in [5], for example : the yoneda lemma and most categorial lemmas are no-more-than Gentzen's constructive logic of re-arranging the input-output positions <<modulo naturality>>. Now homotopy/knots/proof-nets may be held as (faithfull or almost-faithfull) semantical techniques (<<descent>>) to do this <<categorial logic>>, and the homotopy itself may be programmed in specialized grammars (for example [6] or HOTT).
2. The common assumption that catC( - , X ) is dual to catC( Y , - ) is FALSIFIED. This falsification originates from the description of the composition as some binary form instead of as some functional form which is programmed/encoded/enriched onto the computer. Then get some new thing which is named <<polymorphism>> from which to define <<polymorph category>>. This is the only-ever real description and deduction of the yoneda lemma, which says that the image of polyF (which is injective and contained in natural transformations) also contains all natural transformations.
3. Some polymorph category is given by polyF, which is commonly ( _1 o> _2 ), polymorph in V and polymorph in A :
Variable obF : Type.
Variable polyF00 : obF -> obF -> obV.
Notation "F[0 A1 ~> A2 ]0" := (polyF00 A1 A2) (at level 25).
Parameter polyF : forall (B : obF), forall (V : obV) (A : obF),
V(0 V |- F[0 B ~> A ]0 )0 ->
forall X : obF, V(0 F[0 A ~> X ]0 |- [0 V ~> F[0 B ~> X ]0 ]0 )0.
4. And to get polymorph functor, instead of describing F : catA --> catB then (contrast yoneda structures) describe catV[ V , catB[ B , F - ] ] : catA --> catV
And to get polymorph transformation, instead of describing phi A : G A -> H A then a-la-dosen (contrast weighted colimiting Kan extension) describe phi _f : catV( V , catB[ B , G A ] ) -> catV( V , catB[ B , H A ] )
5. Stake for nondependent Solution Programme Seminary at FMCS2016 and ICMS2016 :
paypal 1337777.OOO AT gmail.com , wechatpay 2796386464 , irc #OOO1337777
[1] 1337777.OOO, https://github.com/1337777/borceux/blob/master/borceuxSolution.v
[2] Ahrens, https://github.com/benediktahrens/monads/blob/trunk/CAT/enriched_cat.v
[3] Riehl, http://www.math.jhu.edu/~eriehl/context.pdf
[4] 1337777.OOO, https://github.com/1337777/borceux/blob/master/chic05.pdf
[5] 1337777.OOO, https://github.com/1337777/dosen/blob/master/itp.pdf
[6] Ye, http://katherineye.com/post/129960474471/strange-loops-capturing-knots-with-powerful
* use this authorizing-geolocated-timed-tutoring tool to play these links as TV !
http://1337777.link/ooo/guJAHkwRZYYyuhrh4GyYWv7BPOwNEF-jSeQcYN9WxLk!Zw1GYSFfr6cheRhkPhTPCnsog7DFPZQUCcv7ZEKh22s
https://github.com/1337777/borceux/blob/master/borceuxSolution.v
1. Short: This [1] solves some question of Ahrens [2] and Kan-Riehl [3], which is how to program Kelly's <<enriched categories>> and how the inter-dependence of <<naturality>> with <<category>> is cyclic. Also This [4] attempts to clarify the contrast <<categorical algebra>> (ring/locale-presentation and its "internal logic"), from <<categorial logic>> in the style of the <<enriched/encoded/programmed/recursion>> categories of Kelly-Dosen or Lawvere-Lambek and as attempted in [5], for example : the yoneda lemma and most categorial lemmas are no-more-than Gentzen's constructive logic of re-arranging the input-output positions <<modulo naturality>>. Now homotopy/knots/proof-nets may be held as (faithfull or almost-faithfull) semantical techniques (<<descent>>) to do this <<categorial logic>>, and the homotopy itself may be programmed in specialized grammars (for example [6] or HOTT).
2. The common assumption that catC( - , X ) is dual to catC( Y , - ) is FALSIFIED. This falsification originates from the description of the composition as some binary form instead of as some functional form which is programmed/encoded/enriched onto the computer. Then get some new thing which is named <<polymorphism>> from which to define <<polymorph category>>. This is the only-ever real description and deduction of the yoneda lemma, which says that the image of polyF (which is injective and contained in natural transformations) also contains all natural transformations.
3. Some polymorph category is given by polyF, which is commonly ( _1 o> _2 ), polymorph in V and polymorph in A :
Variable obF : Type.
Variable polyF00 : obF -> obF -> obV.
Notation "F[0 A1 ~> A2 ]0" := (polyF00 A1 A2) (at level 25).
Parameter polyF : forall (B : obF), forall (V : obV) (A : obF),
V(0 V |- F[0 B ~> A ]0 )0 ->
forall X : obF, V(0 F[0 A ~> X ]0 |- [0 V ~> F[0 B ~> X ]0 ]0 )0.
4. And to get polymorph functor, instead of describing F : catA --> catB then (contrast yoneda structures) describe catV[ V , catB[ B , F - ] ] : catA --> catV
And to get polymorph transformation, instead of describing phi A : G A -> H A then a-la-dosen (contrast weighted colimiting Kan extension) describe phi _f : catV( V , catB[ B , G A ] ) -> catV( V , catB[ B , H A ] )
5. Stake for nondependent Solution Programme Seminary at FMCS2016 and ICMS2016 :
paypal 1337777.OOO AT gmail.com , wechatpay 2796386464 , irc #OOO1337777
[1] 1337777.OOO, https://github.com/1337777/borceux/blob/master/borceuxSolution.v
[2] Ahrens, https://github.com/benediktahrens/monads/blob/trunk/CAT/enriched_cat.v
[3] Riehl, http://www.math.jhu.edu/~eriehl/context.pdf
[4] 1337777.OOO, https://github.com/1337777/borceux/blob/master/chic05.pdf
[5] 1337777.OOO, https://github.com/1337777/dosen/blob/master/itp.pdf
[6] Ye, http://katherineye.com/post/129960474471/strange-loops-capturing-knots-with-powerful
* use this authorizing-geolocated-timed-tutoring tool to play these links as TV !
http://1337777.link/ooo/guJAHkwRZYYyuhrh4GyYWv7BPOwNEF-jSeQcYN9WxLk!Zw1GYSFfr6cheRhkPhTPCnsog7DFPZQUCcv7ZEKh22s
- Re: [Coq-Club] 1-year teaching / research position, 1337 777, 05/28/2016
Archive powered by MHonArc 2.6.18.