Re: [TYPES/announce] Tenure-Track Research and Teaching Positions at University of British Columbia, Vancouver, Canada

Re: [TYPES/announce] Tenure-Track Research and Teaching Positions at University of British Columbia, Vancouver, Canada

[1337777.OOO]

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

Re: [TYPES/announce] Tenure-Track Research and Teaching Positions at University of British Columbia, Vancouver, Canada

[Devrim Ünal]

[-- Attachment #1: Type: text/plain, Size: 6433 bytes --]

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

2017-12-31 15:37 GMT+03:00 1337777.OOO <1337777.ooo@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@qq.com ;
> eth 0x54810dcb93b37DBE874694407f78959Fa222D920 ; amazon
> amazon.com/hz/wishlist/ls/28SN02HR4EB8W ; irc #OOO1337777
>

[-- Attachment #2: Type: text/html, Size: 7889 bytes --]