![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Theory of Objects
Nov. 3rd, 2016 11:42 amon one page
1. Idea
The theory of objects is the logical theory whose models in a category 𝒞 are precisely the objects of 𝒞.
2. Definition
The theory of objects 𝕆 is the theory with no axioms over the signature with a single type and no primitive symbols except equality.
===================
The classifying topos 𝒮[𝕆] for the theory of objects 𝕆, or the object classifier, as it is also called, is the presheaf topos [FinSet,Set] on the opposite category of FinSet.
What motivates the terminology, is that for any topos E, geometric morphisms E→𝒮[𝕆] correspond to objects of E.
1. Idea
The theory of objects is the logical theory whose models in a category 𝒞 are precisely the objects of 𝒞.
2. Definition
The theory of objects 𝕆 is the theory with no axioms over the signature with a single type and no primitive symbols except equality.
===================
The classifying topos 𝒮[𝕆] for the theory of objects 𝕆, or the object classifier, as it is also called, is the presheaf topos [FinSet,Set] on the opposite category of FinSet.
What motivates the terminology, is that for any topos E, geometric morphisms E→𝒮[𝕆] correspond to objects of E.
Came to a conclusion that it may be easier to use the idea of "evidences"; e.g. a truth table is an evidence; a proof is an evidence; but then we basically have a topos below (an evidence of a conjunction is a tuple, and an evidence of an implication is a function).
So, it's a type theory.
So, it's a type theory.
i got it, got it
Apr. 29th, 2015 04:26 amIn short, there are small types and big types. Small types, you can call them data types, but that term is kind of taken.
Small types are what the OOP people draw in their class diagrams. Large types are whatever is available in your language.
Embedding (modeling) a small type in a large type is just Yoneda embedding.
So e.g. the diamond problem turns into the problem of building a limit or a colimit. Or rather a Kan extension of appropriate variance.
So-called inheritance is just about Kan extensions, which turn, when the base category ("large types" of a language) is a topos (has logic), into geometric morphisms... rather, into essential geometric morphisms.
That's it; that's why I just woke up and went down to write it down.
Maybe it's all pretty trivial, maybe not.
Upd:
http://arxiv.org/pdf/1206.0357.pdf
http://comonad.com/reader/2015/domains-sets-traversals-and-applicatives/
Small types are what the OOP people draw in their class diagrams. Large types are whatever is available in your language.
Embedding (modeling) a small type in a large type is just Yoneda embedding.
So e.g. the diamond problem turns into the problem of building a limit or a colimit. Or rather a Kan extension of appropriate variance.
So-called inheritance is just about Kan extensions, which turn, when the base category ("large types" of a language) is a topos (has logic), into geometric morphisms... rather, into essential geometric morphisms.
That's it; that's why I just woke up and went down to write it down.
Maybe it's all pretty trivial, maybe not.
Upd:
http://arxiv.org/pdf/1206.0357.pdf
http://comonad.com/reader/2015/domains-sets-traversals-and-applicatives/
I'm in Dallas, TX
Sep. 17th, 2014 02:31 pmIn DFW, the airport.
While on the plane, managed to build the correct empty type (and false);
https://docs.google.com/presentation/d/1HVrs-uhe2N9jQopA5eE41PIFMOzGry69b2CrUArOnsg/edit?usp=sharing
Thank you![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif)
migmit; it was not exactly the way you said, but pretty close.
So there.
Will give a talk about it next week.
While on the plane, managed to build the correct empty type (and false);
https://docs.google.com/presentation/d/1HVrs-uhe2N9jQopA5eE41PIFMOzGry69b2CrUArOnsg/edit?usp=sharing
Thank you
migmit; it was not exactly the way you said, but pretty close.So there.
Will give a talk about it next week.
slides for logic of toposes (part 2)
Jun. 11th, 2014 05:41 amI started talking about topos logic at BACAT, so here are slides, which are, mostly, just a plan of my next talk. References: Johnstone, TT.
https://docs.google.com/presentation/d/1ifVHKj7Nrr_moL1HlGN4c6NzyWNaJjljxbf57AthUOg/edit?usp=sharing
(sorry, sharing was not set properly; fixed)
https://docs.google.com/presentation/d/1ifVHKj7Nrr_moL1HlGN4c6NzyWNaJjljxbf57AthUOg/edit?usp=sharing
(sorry, sharing was not set properly; fixed)
