The Coq mailing list

[Devrim Ünal <devrimunal AT gmail.com>]

This recent post, looks like a phishing attack email, please beware.

2017-12-31 15:37 GMT+03:00 1337777.OOO <1337777.ooo AT gmail.com>:

Proph

https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution3.v

solves half of some question of Cartier which is how to program
grammatical polymorph metafunctors-full-subcategory
containing-equalizers generated by some views ( "complete" ) ...

The ends is to start from some generating/views data and then to add
equalizers of morphisms ; but where are those equalizers ? Oneself
could get them as metafunctors on this generating data, as long as
oneself grammatically distinguishes whatever-is-interesting .

In contrast from the earlier grammatical presentation of
pairing-projections (product), now the equalizer-objects do depend on
the morphisms . BUT THIS DEPENDENCE NEED-NOT BE GRAMMATICAL ! This
dependence could be expressed via the sense-decoding ( "Yoneda" ) of
the grammatical morphisms .

The grammatical objects/morphisms are simultaneously-mutually
presented with their sense-decoding ; this could be done via some
common inductive-recursive presentation or alternatively by inferring
the sense-decoding computation into extra indexes of the type-family
of the object/morphisms .

The conversion-relation shall convert across two morphisms whose
sense-decoding indexes are not syntactically/grammatically-the-same.
But oneself does show that, by logical-deduction, these two
sense-decoding 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 .

For instant first impression , the conversion-relation constructor
which says that the inclusion/restriction (projection) morphisms
cancels the corestriction (pairing) morphism , is written as :

#+BEGIN_EXAMPLE
| Pairing_Project1 :
    forall Yoneda00_L Yoneda01_L (L : @obCoMod Yoneda00_L Yoneda01_L)
      Yoneda00_F Yoneda01_F (F : @obCoMod Yoneda00_F Yoneda01_F)
      Yoneda00_G Yoneda01_G (G : @obCoMod Yoneda00_G Yoneda01_G),
    forall Yoneda10_transfL (transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0)
      Yoneda10_transfR (transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0),
    forall Yoneda10_ff (ff : 'CoMod(0 L ~> F @ Yoneda10_ff )0),
    forall (Yoneda10_ff_eq :
         forall A : obIndexer, proj1_sig Yoneda10_transfL A \o
proj1_sig Yoneda10_ff A
                          =1 proj1_sig Yoneda10_transfR A \o proj1_sig
Yoneda10_ff A),
    forall ( _transfL : 'CoMod(0 F ~> G @ Yoneda10_transfL )0 )
      ( _transfR : 'CoMod(0 F ~> G @ Yoneda10_transfR )0 )
      Yoneda00_Z Yoneda01_Z (Z : @obCoMod Yoneda00_Z Yoneda01_Z)
      Yoneda10_zz (zz : 'CoMod(0 F ~> Z @ Yoneda10_zz )0),

      ( ( ff o>CoMod zz )
        : 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod Yoneda10_ff Yoneda10_zz )0 )
        <~~ ( ( ( << ff ,CoMod Yoneda10_ff_eq @ transfL , transfR >> )
               o>CoMod ( ~_1 @ _transfL , _transfR o>CoMod zz ) )
        : 'CoMod(0 L ~> Z @ Yoneda10_PolyCoMod (Yoneda10_Pairing Yoneda10_ff_eq)
          (Yoneda10_Project1 Yoneda10_transfL Yoneda10_transfR Yoneda10_zz) )0 )
#+END_EXAMPLE

KEYWORDS : 1337777.OOO ; COQ ; cut-elimination ; equalizers ;
polymorph metafunctors-grammar ; modos

OUTLINE :

  * Generating-views data

  * Grammatical presentation of objects and morphisms , with
sense-decoding as metafunctors and metatransformations
  ** Grammatical presentation of objects
  ** Grammatical presentation of morphisms

  * 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

  * Solution
  ** Solution morphisms without polymorphism
  ** Destruction of morphisms with inner-instantiation of object-indexes

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

-----

EPILOGUE : Now there is enough data (for multiple masters-engineering)
to confirm the presence of some MODOS grammar, which is some style of
"substructural topos" ... 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" ) ...

-----

Memo ( "prealables d'un debat" ) ref the unavoidable question : what
is the ends / added-value / product in mathematics ? The ends are
commonly described as research , which is the engineering of some
computational logical computer program or physical prototype (
"correct" ) , and education , which is the knowing-and-teaching of
random-moment dia-para-computalogical discoveries ( "ideas" ) .

But where is the money/pay ? Surprisingly even persons capable of very
complex mathematics can "bug" (
forced-fool-and-theft/lie/falsification ) on such small questions ...
reacting with completely pre-formated one-liners .

- whether public review of mathematical-ends is some unlimited
creation of resource/money/pay ? ( for example ,
https://github.com/1337777/cartier/issues )

- whether public-university registered-students shall have public
choice of who is their paid-teachers and where is their paid
classroom/videostream/book ? ( for example ,
https://www.youtube.com/watch?v=BhWHxiqQzrI&t=26m11s )

- whether if 99% of transfer of value occurs via information-knowledge
then for sure 99% of theft occurs via information-knowledge ? ( for
example , promotion/publisher by some interdependent-tribalistic
hidden "reviewer" is qualifiable as misappropriation of public funds )

... or is ubc not public ?

-----

BUY RECURSIVE T-SQUARE paypal.me/1337777 ; 微信支付 2796386464 AT qq.com ;
eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon
amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777