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 geometry ( completion , topos ... ) . Any secondary-school person is able to know such mathematics , which has been programmed onto the Coq computer.[1][2]
Default (common) colimiting[edit]
Remember that given two functions xA : X → A and xB : X → B , oneself 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[edit]
The ends 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 . Memo that when the target functor is already viewed-functor ( "sheaf" ) then this modified-colimiting becomes the default-colimiting .
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 . Memo 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[edit]
- Topos
- Video tutorials for the Coq proof assistant by Andrej Bauer.
References[edit]
- ↑ 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}