Modos
In mathematics, specifically in category theory, modos is the modification of the default-colimiting which says that « each functor is the sum/colimit of its elements » . Modos shows the interdependence of computational logic ( soundness lemma , cut-elimination , confluence lemma , completeness lemma ... ) along with geometry ( completion , topos ... ) . Any secondary-school student is able to understand such mathematics, which has been programmed onto the Coq computer.[1][2]
Default (common) colimiting
Remember that given two functions xA : X → A and xB : X → B , one may form the pairing ( xA , xB ) : X → A * B into the product A * B such that the two projections of this product a_ : A * B → A and b_ : A * B → B cancel this pairing : a_ ∘ ( xA , xB ) = xA : X → A and b_ ∘ ( xA , xB ) = xB : X → B .
Also remember that in presheaves , the default-colimiting 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) ) .
Modos modifies such common things, but by holding some more-motivated, more-grammatical, more-complete context.
Modified colimiting
The aim is to start with some given viewing-data ( "coverings" ) on some generator-morphology ( "category" ) and then to modify the above default-colimiting .
The modified-colimiting presents this above summing/copairing correspondence 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 . Note that when the target functor is already a viewed-functor ( "sheaf" ) then this modified-colimiting becomes the default-colimiting .
But where are those modified-colimits ? One could get them as metafunctors over this generator-morphology, as long as one grammatically-distinguishes whatever is interesting . Note that in contrast to the more-common mutually-inductive types, this above grammatical presentation of limit objects shall somehow depend on the morphisms, but this dependence need not be grammatical because this dependence is via the sense-decoding ( Yoneda lemma ) of the morphisms .
See also
- Topos
- Video tutorials for the Coq proof assistant by Andrej Bauer.
References
- ↑ 1337777.OOO : Maclane associativity pentagon is some recursive square (functorial-reflection associativity-elimination cut-elimination confluence programmed in COQ) , https://github.com/1337777/maclane/blob/master/maclaneSolution.svg
- ↑ 1337777.OOO : MODOS , https://github.com/1337777/cartier/blob/master/cartierSolution8.v
- Dosen, Kosta (2013). Cut Elimination in Categories. Springer. ISBN 9789401712071. Search this book on
- Borceux, Francis (1994). Handbook of Categorical Algebra. Cambridge University Press. ISBN 9780521441803. Search this book on
|  | |||||||||||||||||
| ||||||||||||||||||
This article "Modos" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Modos. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
![[1]](#cite_note-maclaneSolution.svg-1){kind=link}