The Coq mailing list

["1337777.OOO" <1337777.ooo AT gmail.com>]

I QUIT MATHEMATICS ... I am the most mathematician-by-definition of
the 21st century until now .

-----

Proph

https://gitee.com/OOO1337777/cartier/blob/master/cartierSolution8.v
https://gitlab.com/1337777/cartier/blob/master/cartierSolution8.v.pdf

solves half of some question of CARTIER which is how to program
grammatical polymorph « modos » /
modified-colimits-into-viewed-functors ( "sheafification" , "forcing"
) ...

ERRATA :: this also solves cartierSolution7.v where the
default-colimiting was "confused" .

SHORT ::

  The ends is to start with some given viewing-data on some
generator-morphology and then to modify the default-colimiting which
says that « each functor is the sum/colimit of its elements ; which is
that the (outer) indexings/cocones of the elements of some target
functor over all the elements of some source functor correspond with
the (inner) transformations from this source functor into this target
functor » . In other words : any outer indexing ( X ; (s : S X) |- T X
) corresponds with some inner transformation (   |- (S ~> T) ) . But
where are those modified-colimits ? Oneself could get them as
metafunctors over this generator-morphology , as long as oneself
grammatically-distinguishes whatever-is-interesting .

  The modified-colimiting presents this « copairing » even when any
such indexing ( « real polymorph-cocones » ) is over only some
viewing-elements of this source « viewing-functor » ( "local
epimorphism" ) , as long as the corresponding transformation is into
the (tautologically extended) « viewed-functor » ( "sheafification")
of this target functor . Memo that when the target functor is already
viewed-functor ( "sheaf" ) then this modified-colimiting becomes the
default-colimiting ; in other words it is valid to move from-to :

#+BEGIN_EXAMPLE
(f : F) ; (v : viewing at f) |- (w : viewing indexing the
                                       inner cocone (e_ f v)) -> (e_ f v w : 
E)
#+END_EXAMPLE

#+BEGIN_EXAMPLE
(f : F) ; ((v : viewing at f) , (w : viewing indexing the
                                       inner cocone (e_ f v))) |- (e_ f v w : 
E)
#+END_EXAMPLE

  « 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 ...

  For instant first impression , the conversion-relation constructor
which says that the polyelement (injection) morphism laxly-cancels the
polytransf (copairing) morphism , is written as :

#+BEGIN_EXAMPLE
| PolyTransf_PolyElement : (* ... *)
 forall G f H (v : 'Generator( H ~> G | (V_ G f) )),
 ( (ee_(G)(f)(H)(v)) o>CoMod 'UnitViewedFunctor )
   <~~ ( ( 'PolyElement F v
           : 'CoMod( View H ~> ViewingFunctor F V_ @ _ ) )
         o>CoMod ( [[ ee_ @ F, V_data , V_transp, Yoneda10_ee_natural,
                            Yoneda10_ee_morphism, Yoneda10_ee_real ]]
                   : 'CoMod( _ ~> ViewedFunctor (ViewingFunctor E U_) @ _ ) ) 
)
#+END_EXAMPLE

KEYWORDS :: 1337777.OOO ; COQ ; MODOS

OUTLINE ::

  * Indexer metalogic , viewing data
    + Indexer metalogic
    + Viewing data
    + Unit (total) viewing
    + Intersection (point) viewing
    + Inner (dependent sum) viewing

  * Grammatical presentation of objects
    + Sense-decodings of the objects
    + Grammar of the objects , which carry the sense-decodings

  * Grammatical presentation of morphisms
    + Sense-decodings of the morphisms
    + Modified colimiting is default (common) colimiting when into
viewed-functors
    + Grammar of the morphisms , which carry the sense-decodings

  * Grammatical conversions of morphisms , which infer the same sense-decoding
    + Grammatical conversions of morphisms
    + Same sense-decoding for convertible morphisms
    + Cardinality of the viewing-elements of some viewing-functor
    + Linear total/asymptotic grade and the degradation lemma

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

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

-----

HINT :: secondary-school engineering : redo the
generated-functor-along-reindexing cartierSolution7.v as some
modified-colimitS ( "Diaconescu lemma" ) :
#+BEGIN_EXAMPLE
| PolyTransfGenerated_ : ( forall (I : obIndexer), forall (G : obGenerator)
 (R : obReIndexer) (gr : 'Generator( G ~> Generating0 R ))
 (R_viewing : obViewingReIndexer R)
 (ri : 'Indexer( ReIndexing0 R |- ViewedIndex I )),
 forall R' (v : 'ReIndexer( R' |- R | R_viewing )),
  'CoMod( View_Generating0 R' ~> E_ (ViewedIndex I) @ Yoneda10_ee_ gr
ri v ) ) ->
'CoMod_indexed( Generated_ ~> ViewedFunctor_indexed E_ @ _ )
#+END_EXAMPLE

-----

MEMO :: 1337777.OOO ends to discover-engineer-and-teach 计算鸡-COQ
polymorph mathematics to billions of secondary-school persons (
https://v.youku.com/v_show/id_XMzgwNzY2MTYxNg ) ; « MODOS »
(modified-colimitS) is the alpha-omega of polymorph mathematics contra
« NOISEA » (forced-fool-and-theft/lie/falsification) ...

-----

BUY MOM RECURSIVE T-SQUARE :: paypal.me/1337777 
1337777.OOO AT gmail.com
; 微信支付 
2796386464 AT qq.com
 ; irc #OOO1337777