1337777.OOO
2018-09-03 22:37:06 UTC
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 ***@gmail.com
; 微信支付 ***@qq.com ; irc #OOO1337777
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 ***@gmail.com
; 微信支付 ***@qq.com ; irc #OOO1337777