Re: 5MoF 2018 (January/February)

Re: 5MoF 2018 (January/February)

[1337777.OOO]

[-- Attachment #1: Type: text/plain, Size: 4850 bytes --]

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@gmail.com ;
微信支付 2796386464@qq.com ; eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ;
amazon amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777

[-- Attachment #2: Type: text/html, Size: 5725 bytes --]