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

[1337777.OOO]

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