The Coq mailing list

["1337777.OOO" <1337777.ooo AT gmail.com>]

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