Re: 计算鸡在 [ALGTOP-L] International Workshop on Algebraic Topology, June 6-9, 2018

Re: 计算鸡在 [ALGTOP-L] International Workshop on Algebraic Topology, June 6-9, 2018

[1337777.OOO]

Proph

https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution6.v
https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution6.v.pdf

solves half of some question of Cartier which is 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" )

SHORT ::

  The ends is to do polymorph mathematics which is 2-folded/enriched
ref some indexer which is made of all the graphs as indexes and all
the graph-morphisms as arrows . Such indexer admits the
generating-views ( "generators" ) subindexer ( 4.5.17.h ) made of :
the singleton-object {0} graph ( for « morphisms » , possibly
interdependent with « transformations of morphisms » via
non-grammatical "Yoneda" ... ) , and the
singleton-morphism-between-two-distinct-objects {0 ~> 1} graph ( for «
transformations of morphisms » , for « left-whisk » composition , for
« right-whisk » composition , for « inner » composition along some
tight/strict or lax « cut-adherence » ) , and the two
structural-dividing ( "boundary" ) {0} |- {0 ~> 1} graph-morphims (
for « domain-codomain-morphisms-of-each-transformation » type-indexes
) , and the structural-multiplying ( "degeneracy" ) {0 ~> 1} |- {0}
graph-morphism ( for « unit-transformation-on-each-morphism »
type-constructor ) .

  The 2-conversion-for-transformations relation shall convert across
two transformations whose domain-codomain-morphisms-computation
arguments are not syntactically/grammatically-the-same . But oneself
does show that , by logical-deduction
[convTransfCoMod_convMorCoMod_dom] [convTransfCoMod_convMorCoMod_cod]
, these two domain-codomain-morphisms are indeed 1-convertible (
"soundness lemma" ) .

  Finally, some linear total/asymptotic grade is defined on the
morphisms/transformations and the tactics-automated degradation lemma
shows that each of the conversion indeed degrades the redex
morphism/transformation .

  For instant first impression , the
2-conversion-relation-for-transformations constructor which says that
the first projection morphism/transformation is natural/polyarrowing (
commutativity along these structure-arrow-actions : the
structural-multiplying-arrow ( "degeneracy" ) action which is the
unit-transformation-on-each-morphism [ 'UnitTransfCoMod ]
type-constructor , and the two structural-dividing-arrow ( "boundary"
) actions which are the
domain-codomain-morphisms-of-each-transformation [ 'transfCoMod ]
type-indexes ) , is written as :

#+BEGIN_EXAMPLE
| Project1_UnitTransfCoMod :
    forall (F1 F2 Z1 : obCoMod) (z1 : 'morCoMod(0 F1 ~> Z1 )0),
      ( ~_1 @ F2 _o>CoMod^ ( @'UnitTransfCoMod z1 : 'transfCoMod(0 z1 ~> z1 )0 )
        : 'transfCoMod(0 ~_1 @ F2 o>CoMod z1 ~>
                ( ~_1 @ F2 o>CoMod z1 : 'morCoMod(0 Pair F1 F2 ~> Z1 )0 ) )0 )
        <~~2 ( @'UnitTransfCoMod ( ~_1 @ F2 o>CoMod z1 ) )
#+END_EXAMPLE

KEYWORDS :: 1337777.OOO ; COQ ; cut-elimination ; 2-fold functors ;
non-contextual 2-fold pairing-projections ; polymorph
metafunctors-grammar ; modos

OUTLINE ::

  * Indexer metalogic for 2-fold-enrichment
    + Generating data 2-folded-enriched ref the generating-views subindexer

  * Grammatical presentation of objects and touched-morphisms
2-folded/enriched ref the generating-views subindexer

  * Solution morphisms
    + Solution morphisms without polymorphism
    + Inversion of morphisms with same domain-codomain objects
    + Destruction of morphisms with inner-instantiation of object-indexes

  * Grammatical 2-conversion of transformations , which infer the
1-conversions of their domain-codomain morphisms
    + Grammatical 1-conversions of morphisms
    + Linear total/asymptotic morphism-grade and the degradation lemma

  * Polymorphism/cut-elimination by
computational/total/asymptotic/reduction/(multi-step) resolution

  * Grammatical presentation of transformations
    + Inversion of the cut-adherence ( here propositional-equality )
    + Outer ( "horizontal" ) left-whisk cut , outer ( "horizontal" )
right-whisk cut , and inner ( "vertical" ) composition cut with
cut-adhesive

  * Solution transformations
    + Solution transformations without polymorphism
    + Destruction of transformations with inner-instantiation of
morphism-indexes or object-indexes

  * Grammatical 2-conversion of transformations , which infer the
1-conversions of their domain-codomain morphisms
    + Grammatical 2-conversions of transformations
    + 1-convertibility of the domain/codomain morphisms for
2-convertible transformations
    + Linear total/asymptotic transformation-grade and the degradation lemma

  * Polymorphism/cut-elimination by
computational/total/asymptotic/reduction/(multi-step) resolution

-----

HINT :: free master-engineering-thesis ; program this grammatical
polymorph generated-functor-along-reindexing ( "Kan extension" ) :

generatedFunc ( I : IndexerCat ) ( G : GeneratorsCat ) :=
 { R : ReIndexerCat & { f : G ~> generatingFunc R | p : reIndexingFunc
R |- I } }

-----

老子

https://github.com/1337777/dosen/blob/master/1337777solution.txt

1。 [力了-疯-与-[偷窃/谎言/伪造]]（ “缺乏[真相/现实/现实/是]” ， “吵恶” ， “noisea” ， “f-f-a-t” ）是
2。 [
2.1。 做
2.2。 尝试/[编造[可能性/时机/机会]]做 ]
3。 转换 或 采取
4。 自己的自我（ 由转移 ， 或 由比例=打印自己的钱=燃烧其他的钱 ）[获得/赢/非损失]
4.1。 （ 如[同步/勾结/纵容] /
4.2。 [ 作为[相互依存的/非自主的]（ “部落主义” ， “tribalistic” ），当时盗用公共资金由相互依赖的绕道 （
“detournement-interdependant de fonds publics” ） ] /
4.3。 [ 作为货币主义者（ “现金-货币-只”作为[附加价值/产品/本末] ） ] /
4.4。 [ 作为[收款人/木偶/代理人]（ “宠物” ） ] /
4.5。 [ 作为[付款人/木偶匠/指挥官]（ 由付款 ， 由建议 ，由[预测损失如果别] ） ] /
4.6。 [ 作为[法官/裁判员/仲裁人]（ “巫师” ）谁[撰写/编辑/编造/猜测]过分地以外其管辖权=权限=[个人知识证词在只之见证人] ]
4.7。 在[追溯-时间]（ “retrocommission” ）或在[现在-时间]或在[未来-时间]（ “贷款” ， “信用卡” ，
“a-credit” ）
4.8。在一些货币主义的或[相互依存的/部落主义的]和[有效地-匿名的][人群/暴民/帮派/社团主义] ，
4.9。 这样为防止[累积和继承]于[力了-疯-与-[偷窃/谎言/伪造]] ）
5。 对于其他[某些人或公众]的损失 （ “detournement-interdependant de fonds publics” ） （
5.1。 损失于：[可预测-时间][计算地-逻辑的]工程 ， 或
5.2。 损失于：[随机-时刻][横-准-计算-逻辑的]发现（ “dia-para-computalogical”
），包括过之损失于[评论/输入/反馈]从公众或公共学生 ， 或
5.3。 损失于：[时机/动量/“kairos”/机会/可能性们] ， 或
5.4。 损失于：可交易性， 包括过这损失于[公众或公共学生们][付款人们/购买们/客户们] ， 或
5.5。损失于：健康 ， 或
5.6。纯属 恶意（ “嫉妒” ））
6。由媒介这么如
7。谎言 ，
7.1。谎言隐藏了因为自己的疯 ，
7.2。谎言经由：隐藏的谎言，以便[防止/挫败]公众的自己审查 ，
7.3。谎言经由：伪造 ，
7.4。（ “mispell” ）。 谎言经由：[模拟/模仿/玩][混乱/随机/非意图/非动机/非知识] ，
7.5。 谎言经由：缺席如同否定（ 略去，抹去，不要[确定化/决定] ） ，
7.6。（ “[墨水-和-纸]” ）。 谎言经由：没费用地谎言 ，
7.7。 谎言经由：[[模仿者/冒名顶替者/篡位者]-叛徒] ，
7.8。（ “[首都的-双重-谎言们]” ）。
谎言经由：做多一个的新的[力了-疯-与-[偷窃/谎言/伪造]]，以便隐藏一些早期的[力了-疯-与-[偷窃/谎言/伪造]]，或以便于[愚弄/误导]一些“[公平-和-平衡的]”[法官/裁判/仲裁员]直到它让出[双重-谎言们]的一半
，
8。 和同时
9。 疯 ，
9.1。 疯隐藏了因为自己的谎言 ，
9.2。 疯经由：隐藏的疯，以便[防止/挫败]之公众的自己审查 ，
9.3。疯经由：吵恶的或吵的 ，
9.4。（ “进出” ， “flip-flop” ）。 疯经由：混乱或由矛盾于自我， 或由进出“可能性”（ “酌情” ， “风险”
）对着“[抄我]-分级”（ “简历” ， “客观” ， [它拒绝是在教学下主观] ） ，
9.5。疯经由：分心，
9.6。疯经由：鲁莽的跑步（不知道后果），
9.7。（“mythomane”）。 疯经由：不完整的年表 ，
9.8。（“呜呜”）。 疯经由：[不成比例/过度的]比较在[损害/损失] ，
9.9。（“玩” ， “[倒装的-指控]”）。 疯经由：[模拟/模仿/玩][损害/损失/受害者]当自我是之原因或受益人 ，
9.10。（ “宠物任务” ）。 疯经由：[模仿/[冒名顶替]/[篡位]]-[背叛/交易]其他人的实际的[损害/损失]
，当自我是之原因或受益人，或 当自我是“[之效果是一样的]-[之感是更坏的]”（ “不是全但是每” ， “[消防者-纵火者]” ）比之原因
，
9.11。（ “你懂的” ）。 疯经由：转移自己的[傻瓜/精神病/幻想/[神经运动]]到另一个人身 ，
9.12。（ “现状” ， “特权” ）。 疯经由：转换常见的重复的[力了-疯-与-[偷窃/谎言/伪造]]至真相，或
由转换“[不在[逮捕/捕获/抓住]]”至真相 ，
9.13。 （ ”单一者-类“ ）。 疯经由：[编造/伪造]一些[法律/规则/分级/类]，哪或它的补集包含只某些[有效地-单一]目标个人 ，
以便 最大化这个人或相应地阻碍这个人 ， 或 当 只“身份们的交叉口”是有效的和这样是更坏的 ，
9.14。（ “疯-垄断” ）。 疯经由：在支持疯从自我，却 [需求量/要]理由从另一个人 ，
9.15。（ “最大化-垄断” ）。 疯经由：[只单向-最大化]（ “支持”，“鼓励” ，“拥护”，“额外-程序”
），当时[“自大的”-感]于之[另一方向-围绕] ，
9.16。（ “指控-垄断” ）。 疯经由：[只单向-[损害/受害者]]（ “恐吓”，“骚扰” ，“威胁的”，“阻碍”
），当时只承认[直接-物理的-[外伤/伤口]]为之[另一方向-围绕] ，
9.17。（ “玩-垄断” ）。 疯经由：可能性于[[模拟/模仿/玩/玩笑]-借口]从自我，当时这么总是[现实/严肃]从另一个人 ，
或经由[诽谤/指控]（ 没有自我[个人-知识] ）以[问问题-借口]的形式 ( “ ... ? ” ) ，
9.18。（ “假勇气” ）。 疯经由：反对[任何人/自主地]除外自己的[付款人/相互依存] ，
9.19。（ “va-t-en-guerre”，“将在战争” ）。 疯经由：指挥力, 却不想[自己的-做]力 ，
10。 和同时
11。 力，
11.1。 力，而在[疯-与-[偷窃/谎言/伪造]] ，
11.2。 力经由：[指挥/暗示/[子-领导]]一些[官员的-强制者] ，
11.3。（ “突击” ）。 力经由：突然的力 ，
11.4。 力经由：缓慢的力 。

-----

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