[GAP Forum] [MCA2017] Computations in Groups and Applications in Montréal

[1337777.OOO]

Proph

https://gitlab.com/1337777/cartier/blob/master/cartierSolution.v

solves some question of Cartier which is how to program grammatical
meta (metafunctors) ...

This starting lemma of polymorph mathematics ( "categories" ) :

Coreflections( Set , Funtors( op C , Prop ) ) <=> Funtors( C , Set )

says that the senses ( "metafunctors models" ) onfrom some given
primitive-syntax graph may be instead dually viewed as senses (
"coreflective-metafunctors models" ) into some more-complete
metafunctors-grammar ( "classifying topos" ). And this starting lemma
may be upgraded such to perceive flat metafunctors via geometric
morphisms into this metafunctors-grammar. Also this starting lemma may
be upgraded such to perceive continuous flat metafunctors via
geometric morphisms into some sheaf metafunctors-grammar ...

The question is whether these new more-complete metafunctors-grammars
are relatively computational/decidable ? This COQ text solves half of
this question, the resting half is promised only ...

Outline: Primo, the things shall be confined to some meta regular
cardinal, and this COQ text assumes-as-axiom some maximum operation
inside this regular cardinal and this COQ text assumes-as-axiom some
functional extensionality of families of morphisms which are confined
to this regular cardinal. Secondo, as was done in the earlier COQ text
for colimits, one shall erase/extract some logical cocone-conditions
by assuming some erasure/extraction scheme as axiom instead of some
very-complicated-induction scheme (beyond induction-induction) ...
Tertio, the degradation lemma is more technical than in the earlier
COQ texts, because for the congruent-reduction from the copairing
operation applied onto some cocone of morphisms, one shall require
simultaneous full-reduction of every reductible morphism in the
cocone. Most of this COQ program and deduction is automated.

Keywords: 1337777.OOO//cartierSolution.v ; metafunctors-grammar ;
duality ; classifying topos

-----

Memo :

The 1337777.OOO SOLUTION PROGRAMME originates from some random-moment
discovery of some convergence of the DOSEN PROGRAMME
[[http://www.mi.sanu.ac.rs/~kosta]] along the COQ PROGRAMME
[[https://coq.inria.fr]].

The 1337777.OOO has discovered [[1337777.OOO//coherence2.v]]
[[google.com/#q=1337777.OOO/coherence2.v]]
[[https://web.archive.org/web/20170516011054/https://github.com/1337777/dosen/blob/master/coherence2.v]]
[fn:4] [fn:5] that the attempt to deduce associative coherence by
Maclane is not the reality, because this famous pentagone is in fact
some recursive square. This associative coherence is the meta of the
semiassociative coherence [[1337777.OOO//coherence.v]] which does lack
some more-common Newman-style confluence lemma.

Moreover the 1337777.OOO has discovered
[[1337777.OOO//borceuxSolution2.v]] [[1337777.OOO//chic05.pdf]] that
the "categories" ( "enriched categories" ) only-named by the
homologist Maclane are in reality interdependent-cyclic with the
natural polymorphism of the logic of Gentzen, this enables some
programming of congruent resolution by cut-elimination
[[1337777.OOO//dosenSolution3.v]] which will serve as specification
(reflection) technique to semi-decide the questions of coherence, in
comparasion from the ssreflect-style.

Furthermore the 1337777.OOO has discovered
[[1337777.OOO//aignerSolution.v]]
[[1337777.OOO//ocic04-where-is-combinatorics.pdf]] that the
Galois-action for the resolution-modulo ( "symmetry groupoid action"
), is in fact some instance of polymorph functors.

And the 1337777.OOO has discovered
[[1337777.OOO//ocic03-what-is-normal.djvu]]
[[1337777.OOO//laoziSolution2.v]] how to program polymorph
coparametrism functors ( "comonad" ).

And the 1337777.OOO has discovered [[1337777.OOO//chuSolution.v]] how
to program contextual limits of polymorph functors ( "Kan extension"
).

And the 1337777.OOO has discovered [[1337777.OOO//cartierSolution.v]]
how to program the metafunctors-grammar ( "topos" ), as the primo step
towards the programming of the ( "classifying-topos" )
sheaf-metafunctors-grammar which is held as augmented-syntax in the
Diaconescu duality lemma ( "coreflective-metafunctors models" ).
Another further step shall be to GAP-and-COQ program
[[https://www.gap-system.org]] the computational logic for Tarski's
decidability in free groups and for convergence in infinite groups ...

Additionnally, the 1337777.OOO has discovered random dia-para-logic
discoveries [[1337777.OOO//1337777solution.txt]] and
information-technology [[1337777.OOO//init.html]]
[[1337777.OOO//init.pdf]] [[1337777.OOO//makegit.sh.org]]
[[1337777.OOO//editableTree.urp]] [[1337777.OOO//gongji.ml4]] based on
the _EMACS org-mode_ logiciel which enables communication of
_timed-synchronized_ _geolocated_ _simultaneously-edited_
_multi-authors_ _format-able_ _searchable_ text, and therefore
_personal email_ and _public communication_ of
_multiple-market/language_ (中文话）textual COQ math programming, and
which enables _personal archiving_ and _public archiving_ and
therefore _public reviews / webcitations_ .

Whatever is discovered, its format, its communication is
simultaneously some predictable-time (1337) computational-logical
discovery and some random-moment (777) dia-para-computalogical
discovery.

-----

Memo ( "prealables d'un debat" ) ref the unavoidable question : what
is the "ends" / "added-value" / "product" in mathematics ? The "ends"
in mathematics are commonly described as "education" and "research".
In reality the only "research" ( predictable-time
computational-logical discovery, "correct" ) is the engineering of
some computational logical computer program or the engineering of some
physical prototype, and the rest is "education" ( random-moment
dia-para-computalogical discovery, teaching "ideas" ) which is
amplified by the question of "audience"/"market" or universality of
the communication-language medium [[1337777.OOO//gongji.ml4]].

Unfortunately sometimes forced-fool-and-theft/lie/falsification (
"absence of reality" ) [[1337777.OOO//1337777solution.txt]] defeats
both "research" by preventing anything other than " .PDF binary files
with pretty greek-letters and large-vertical-symbols ", and defeats
"education" by preventing public-review (including public-students
review). The medium of this forced-fool-and-theft/lie/falsification
may be monetarist or "tribalistic" (interdependent) ... such that it
is common ( "maybe half" ) question whether one "tribalistic"
(interdependent) teacher's purely predictable-time
computational-logical discovery, steals/hides/injects some other
original-teacher's "idea" (random-moment dia-para-computalogical
discovery) ... and such that it is common ( "maybe half" ) question
whether the fabrication/falsification of some non-necessary
grade/bounty/reward is precisely to permit "tribalistic"
(interdependent) determinism ... or am I the 7ok3r ?

-----

paypal 1337777.OOO at gmail.com , wechatpay 2796386464 at qq.com , irc #OOO1337777