-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path1337777Programme.text
67 lines (34 loc) · 10.7 KB
/
1337777Programme.text
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
MORE :: https://github.com/1337777/cartier/blob/master/1337777Programme.text
SHORT ::
Mathematicians , logic , and topology are interdependent , but how ?
For the past half-century , mathematicians have failed to see the real computational logic which moves topology : some mysterious categorical-algebra reformulation indeed moves geometry ( "coverings over parameterizations" ) and homotopy ( "relaxations under relativizations" ) !
Firstly , in computational logic until now , mathematicians have stop short from generalizing the known techniques ( "cut-elimination" , "confluence" , "dependent-typed functional programming" ) from the computer machines towards any alternative formulations of categorical-algebra . For example , all these categorical-algebras : "adjunctions" , "comonads" , "products" , "extensions along functor" , "enriched categories" , "internal categories" , "2-fold categories" ( with sense in "model category" ) , "coherent presheaves" ( with sense in "topos" ) and "localizations" , "fibred category with local internal products" ... now have alternative reformulations as computational logics ( "polymorph mathematics" ) .
Secondly , in geometry ( with sense in "topos" ) and homotopy ( with sense in "model category" ) until now , mathematicians have not moved past the old computational support ( coefficients ) , which occurs inside "additive categories" ( "sheaves of modules" , "modules over some group-ring" , "parametrized linear algebra" , "iterative relative cohomological algebra of derived functors" ) . Even the latest "stacks" or "derivators" , which attempt to generalize from such "additive categories" as computational coefficients , have failed to notice this new computational logic formulation of categorical-algebra .
But it is now learned-and-discovered that : geometry ( "coverings over parameterizations" ) and homotopy ( "relaxations under relativizations" ) is moved by this alternative formulation of categorical-algebra as computational logic ! And the engineering-and-teaching of these is being attempted via the COQ-computer and the GAP-computer .
-----
MEMO :: OOO1337777 ends to learn-discover-engineer-and-teach 鸡算计-COQ polymorph mathematics to billions of secondary-school persons ( [[https://www.bilibili.com/video/av49126093]] ) ; « MODOS » (modified-colimitS) is the alpha-omega of polymorph mathematics contra « NOISEA » (forced-fool-and-theft/lie/falsification) ...
-----
SHORT ::
OOO1337777 SOLUTION PROGRAMME [[https://gitlab.com/1337777]] originates from some random-moment dia-para-computalogical learning-discovering-engineering-and-teaching of some convergence of the DOSEN PROGRAMME [[http://www.mi.sanu.ac.rs/~kosta]] along the COQ PROGRAMME [[https://coq.inria.fr]] .
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//maclaneSolution.svg]] [[1337777.OOO//coherence2.v]] [[1337777.OOO//maclaneSolution2.thy]] [[google.com/#q=1337777.OOO/coherence2.v]] [[https://sympa.inria.fr/sympa/arc/coq-club/2016-01/msg00090.html]] [[https://web.archive.org/web/20160627011042/https://raw.githubusercontent.com/1337777/dosen/master/coherence2.v]] that the attempt to deduce associative coherence by Maclane is not the reality , because this famous pentagon is in fact some recursive square (reflective-functorial associativity-elimination cut-elimination resolution) . This associative coherence is the meta-terminology for the completeness-lemma of the (oriented-)semiassociative coherence [[1337777.OOO//coherence.v]] and this semiassociative coherence does lack some more-common Newman-style local confluence lemma .
And OOO1337777 did learn-discover-engineer-and-teach [[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 (sameness-of-morphisms) , in comparison from the ssreflect-style .
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//ocic03-what-is-normal.djvu]] [[1337777.OOO//laoziSolution2.v]] how to program the grammatical polymorph coparametrism functors ( "comonad" ) .
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//chuSolution.v]] how to program the grammatical contextual singleton-or-multiple-or-total limits of polymorph functors ( "Kan extension" ) .
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution.v]] how to program the metafunctors-grammar ( "presheaves" , "colimit completion" ) , and did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution2.v]] how to program the grammatical pairing-commutant retractive reflection ( "localization" , "calculus of fractions" , "special factorization system" , "universal closure operator" , "Galois-topology" ) , and did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution3.v]] the lacking new elimination-scheme for expressing the dependence of limit-objects over grammatical morphisms via their sense-decoding ( "Yoneda" ) as metatransformations functions ; this technique is used to program grammatical polymorph metafunctors-full-subcategory containing-equalizers generated by some views ( "completion" ) ... These earlier attempts are 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" ) , and confirm the presence of some MODOS grammar , which is some style of "substructural topos" where the dependence of limit objects upon morphisms need not be grammatical ( "Yoneda" ) ! ... and where oneself could present grammatical polymorph views-data ( "sheaves" ) , grammatical polymorph generating-views ( "presentable category" ) , grammatical polymorph internal functors ( "internal category" ) , grammatical polymorph images ( "regular category" ) , grammatical polymorph unions ( "coherent category" ) ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution4.v]] how to program grammatical polymorph internal ( "typed" , "small" ) pairing-projections ( "product" ) ... And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution5.v]] how to program grammatical polymorph contextual ( "weighted" ) multifold ( "enriched" ) pairing-projections ( "product" ) ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution6.v]] how to program grammatical polymorph non-contextual ( "1-weighted" ) 2-fold ( "2-higher" ) pairing-projections ( "product" ) ... ( this multi-folding is the foundation of homotopy "algebraic topology"/"fibre functor" ) ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution7.v]] how to program grammatical polymorph generated-functor-along-reindexing ( "Kan extension" ) ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution8.v]] how to program grammatical polymorph « modos » / modified-colimits-into-viewed-functors ( "sheafification" , "forcing" ) ... « MODOS » (modified-colimitS) is the alpha-omega of polymorph mathematics . It shows the interdependence of computational-logic along geometry : sensible "soundness" lemma , cut-elimination , confluence lemma , sense-completeness lemma ( in presheaves whose combinatorics mimick "links"/"proof-net" ) , maximality lemma , asymptotics of randomness , DOSEN book ... ; generated-functors ( "Diaconescu lemma" ) , equalizer completion , image ( "regular" ) completion , essential geometric-morphisms ( "Cauchy completion" ) , BORCEUX book 1-2-3 ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//cartierSolution9.v]] how to program « parametrization modos » ( "parametrized form" , "dependent type" , "fibration with internal products" ) ...
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//dosenSolution101.v]] how to program the logical/particular/rewriting/(one-step) polymorphism/cut-elimination and the confluence/commutation of this rewriting for the grammatical polymorph pairing-projections ( "product" ) , which shows that this logical resolution ( by non-linear arithmetic grade ) is indeed some alternative description of the computational/total/asymptotic/reduction/(multi-step) polymorphism/cut-elimination chosen-function ( by linear arithmetic grade ) .
And OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//aignerSolution.v]] [[1337777.OOO//ocic04-where-is-combinatorics.pdf]] that the Galois-action for the counting-modulo ( "symmetry groupoid action" ) , is in fact some instance of reversible polymorph metafunctors . Another further step shall be resolve whether these are also some instance of localization of metafunctors-grammar . Yet 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 asymptotic/convergence of infinite random groups ...
Necessarily , OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//1337777solution.txt]] random-moment dia-para-computalogic , « noisea » forced-fool-and-theft/lie/falsification ( "absence of reality" ) .
Necessarily , OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//ethereumSolution.sol]] information-technology to measure reviews/citations (¢entse currency) by using public programmatic proxy-authors « pprogxy » ( "ethereum blockchain cryptographic smart-contract" ) integrated along content-addressable personal-public replicated-storage ( "swarm dht" ) .
Necessarily , OOO1337777 did learn-discover-engineer-and-teach [[https://space.bilibili.com/403144043]] [[https://mixer.com/OOO1337777]] [[1337777.OOO//qoc_jisuanji.v]] information-technology for multiple-market/language textual 鸡算计-COQ math programming .
Necessarily , OOO1337777 did learn-discover-engineer-and-teach [[1337777.OOO//init.html]] [[1337777.OOO//init.pdf]] [[1337777.OOO//makegit.sh.org]] [[1337777.OOO//editableTree.urp]] information-technology based on the EMACS org-mode logiciel which enables the communication of timed-synchronized geolocated simultaneously-edited multi-authors format-able searchable textual COQ math programming .
Whatever OOO1337777 did learn-discover-engineer-and-teach is simultaneously : predictable-time (1337) computational-logical and random-moment (777) dia-para-computalogical ...
-----
KEYWORDS :: OOO1337777 ; COQ ; 鸡算计 ; MODOS
-----
PAY $13.37 FOR 37 DAYS - VIEW OUT AND POST IN SCHOOL TRANSCRIPTS : [email protected]
[[https://www.paypal.com/cgi-bin/webscr?cmd=_s-xclick&hosted_button_id=SKR2W3TSU87HA]]