Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] 5MoF 2018 (January/February)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] 5MoF 2018 (January/February)


Chronological Thread 
  • From: "1337777.OOO" <1337777.ooo AT gmail.com>
  • To: "thex AT yahoo.com" <thex AT yahoo.com>, "noisebridge-discuss AT lists.noisebridge.net" <noisebridge-discuss AT lists.noisebridge.net>, "algtop-l AT lists.lehigh.edu" <algtop-l AT lists.lehigh.edu>, "isabelle-users AT cl.cam.ac.uk" <isabelle-users AT cl.cam.ac.uk>, "coq-club AT inria.fr" <coq-club AT inria.fr>, "categories AT mta.ca" <categories AT mta.ca>
  • Subject: Re: [Coq-Club] 5MoF 2018 (January/February)
  • Date: Thu, 21 Jun 2018 19:37:07 -0700
  • Authentication-results: mail3-smtp-sop.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-f67.google.com
  • Ironport-phdr: 9a23:SCIyRhECeuHdTbh/WjRAAJ1GYnF86YWxBRYc798ds5kLTJ76psy+bnLW6fgltlLVR4KTs6sC17KL9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa9bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE7/mHZisJ+gqFGrhy/uxNy2JTbbJ2POfdkYq/RYdEXSGxcVchRTSxBBYa8YpMBA+YcM+tVoYvwqlkMoBa8HwWiHfrhxCZGinTr2qA2zuosHA/E0QEiHd8Dsm7YrNLyNKcVSu21w6zIwi/Cb/NSwzvy9I/IchU4rPyKQLl+f83RyUw1GAPEiFWdsZTlMCmV1+QVqWeb6/BsVeexhGI/sQ5xpyKgx8YrionPnI4a1lfE9SBhzIY6JN24VE57YcO/H5dKqy6aMI52TtstQ2FppCY11KMJtYSncygNzZQqwQPUZf+fc4WQ/B7vSOKcLS17iX9lYr6zmQu+/Eu6xuD9VMS51ktBoDBfndnWrH8N0gTe6siZRft5+UeswTOP2BrS6uFAOEw0kqvbJ4I4zr4+l5ces17PHiDxmEXxg6+Wclsr9vK05OTgZ7Xqvp6cN4lqhQHiKqkihNCzDOAiPgUNX2WX4/qw2KDg8EHjQbhHjOU6kqzDv5DbIcQbqLS5AwhQ0os79hqyATmr3dYakHQFLl9JYhWHj4/uO1zVL/D4CO2wg1WokDtx2//GObjhDo3XLnffiLfhYap960lExQUvytBf/otYBa0FIPLuQUD8r8fYDx88Mwys2enrEtR91oUEWWKOGKCVKq3SsUXbrt4odqOQZIIFkCf0K/8iofXpiDVxzUMdcLmBzJIXb3f+FfNjdQHRK3zrg8wMG30LsgUzCeDrk1afSiV7Y3epQ7l64DY6E4+sF4bPSY3rhrGdlm/vGJpXfW1MEFGAHnqte4SfUOoXcwqWI9R9iXoCUrm6RoU71B2huUn8xqYxaqKe8ykXqZX7kdxd4+zIiQp08TF0DsudlWyBUis8ymoMSCMxxOV7iUh80UuYl6x1g/1XFZpe6+4fFk9wNIXVxeF+D923RxnMZMyhQ1LgSdyjRzg6CM8yiZdaYl10Edimih2GwjGnGaQ9nLjND5UxtKvXmWXycYI1gX3Bzewqi0QsaspJL2yvwKBlvUCHDInQ1k6diqyCdKIG3SeL+n3ViSLEt0hEXQF3S6TIRlgaekKQpt2zrhfJRqOjBrM9MwZa4cueI+1BY4u6o09BQaKpYY+FPD3uxCGXIjHCjufVN9G1JDpCmiLaD2ALlgkS+TCNMg1oVXTpmH7XEDE7TQGnWEjr6+Qr8CrqHH9x9BmDagha75Tw/xcUgfKGTPZKh+ALvS4gr3N/G1PvhouKWerFnBJoeeBnWf14+E1OjDuLuAl0P5jmJKdn1AZHLlZH+nj23hAyMb1u1MgnqHRwkVh3IKOclVRAL3aWg8+2NbrQJW3/uhuobvyO1w==

Proph

https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution7.v
https://github.com/1337777/cartier/blob/master/cartierSolution7.v.pdf

solves half of some question of Cartier which is how to program grammatical polymorph generated-functor-along-reindexing ( "Kan extension" ) ...

SHORT ::

  The ends is to do start with some given generating-functor from some given reindexer-graph into some given generator-graph and then to generate some other extended functor from some given extended indexer-graph into some extension of the given generator-graph ; but where are those outputs of the generated-functor at the indexes ? Oneself could get them as metafunctors over this generator-graph , as long as oneself grammatically-distinguishes whatever-is-interesting .

  Memo that the sense of this generated-functor ( « colimits » ) really-is the colimit(-simultaneously) of multiple diagrams , instead of the multiple colimits of each diagram ( "pointwise" ) (I.3.7.2) ... Moreover memo that here the generator-graph is some non-quantified outer/global parameter , instead of some innerly-quantified local argument which is carried around by all the grammatical constructors , in some « polygeneration » (functorial) form , as for some presentation of grammatical right-adjunction  (I.3.7.6) ...  Elsewhere memo that the generated-functor is similar as some existential-quantification functor ( left adjoint to some preimage functor of the generating-functor ) , therefore oneself may now think of adding logical-connectives to form some external-logic of modos and to attempt polymorph (relative-)quantifier-elimination ...

  Now the conversion-relation shall convert across two morphisms whose sense-decoding datatype-indexes/arguments are not syntactically/grammatically-the-same . But oneself does show that , by logical-deduction , these two sense-decodings are indeed propositionally equal ( "soundness lemma" ) .

  Finally , some linear total/asymptotic grade is defined on the morphisms and the tactics-automated degradation lemma shows that each of the conversion indeed degrades the redex morphism . But to facilitate the COQ automatic-arithmetic during the degradation lemma , here oneself assumes some finiteness-property on the graph of reindexer elements of each index along the reindexing-functor and also assumes some other finiteness-property on the indexer-graph . Clearly this ongoing COQ program and deduction will still-proceed when those things are confined less than any regular cardinal .

  For instant first impression , the sense-decoding ( "Yoneda" ) of the generated-functor-along-reindexing , is written as :

#+BEGIN_EXAMPLE
Definition Yoneda00_Generated (I : obIndexer) (G : obGenerator) :=
  { R : { R : obReIndexer & 'Indexer( ReIndexing0 R |- I ) }
        & 'Generator( G ~> Generating0 (projT1 R) ) }.
Axiom Yoneda00_Generated_quotient :
  forall (I : obIndexer) (G : obGenerator),
  forall (R S : obReIndexer) (rs : 'ReIndexer( R |- S ))
    (si : 'Indexer( ReIndexing0 S |- I ))
    (gr : 'Generator( G ~> Generating0 R )),
    ( existT _ (existT _ S si) (gr o>Generator Generating1 rs) )
    = ( existT _ (existT _ R (ReIndexing1 rs o>Indexer si)) gr
        : Yoneda00_Generated I G ).
#+END_EXAMPLE

KEYWORDS :: 1337777.OOO ; COQ ; cut-elimination ; polymorph generated-functor-along-reindexing ; polymorph metafunctors-grammar ; modos

OUTLINE ::

  * Indexer metalogic , generating-views data

  * Grammatical presentation of objects
    + Sense-decodings of the objects
    + Grammar of the objects , which carry the sense-decodings

  * Grammatical presentation of morphisms
    + Sense-decodings of the morphisms
    + Grammar of the morphisms , which carry the sense-decodings

  * Solution morphisms
    + Solution morphisms without polymorphism
    + Destruction of morphisms with inner-instantiation of object-indexes

  * Grammatical conversions of morphisms , which infer the same sense-decoding
    + Grammatical conversions of morphisms
    + Same sense-decoding for convertible morphisms
    + Linear total/asymptotic grade and the degradation lemma

  * Polymorphism/cut-elimination by computational/total/asymptotic/reduction/(multi-step) resolution

-----

HINT :: free master-engineering ; program this grammatical polymorph viewed-metafunctor-along-views-data ( "sheafification" ) :
#+BEGIN_EXAMPLE
| PolyElement :
  Transformations( ( S : SubViewOfGeneratingView G ) ~> F )
  -> Transformations( G ~> ViewedMetaFunctor F )
#+END_EXAMPLE

-----

BUY MOM RECURSIVE T-SQUARE :: paypal.me/1337777 1337777.OOO AT gmail.com ; 微信支付 2796386464 AT qq.com ; eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777


  • Re: [Coq-Club] 5MoF 2018 (January/February), 1337777.OOO, 06/22/2018

Archive powered by MHonArc 2.6.18.

Top of Page