juan_gandhi: (VP)
on 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.


Oct. 15th, 2016 04:23 pm
juan_gandhi: (VP)
Just slapped together a deck of slides, category theory for scala programmers


Comments wholeheartedly welcome
juan_gandhi: (VP)
scala> val s = Set("a", "b", "c")
s: scala.collection.immutable.Set[String] = Set(a, b, c)

scala> val t = s.map(_ + ":)")
t: scala.collection.immutable.Set[String] = Set(a:), b:), c:))

scala> val s = Set("a1", "a2", "a3")
s: scala.collection.immutable.Set[String] = Set(a1, a2, a3)

scala> val t = s.map(_ take 1)
t: scala.collection.immutable.Set[String] = Set(a)

scala> val u:Set[Any] = s map identity
u: Set[Any] = Set(a1, a2, a3)

scala> val v:Set[Any] = s
<console>:8: error: type mismatch;
 found   : scala.collection.immutable.Set[String]
 required: Set[Any]
Note: String <: Any, but trait Set is invariant in type A.
You may wish to investigate a wildcard type such as `_ <: Any`. (SLS 3.2.10)
       val v:Set[Any] = s

From a categorist's p.o.v, wtf, if we have map, we have a covariant functor. But wow, it's "type theory", covariance here means only covariance w.r.t. subtyping. So, big deal, map with identity, no? I mean, not being a typist, I don't even understand the problem. Do you?
juan_gandhi: (VP)
an example of a Set-endofunctor that does not preserve monomorphisms... any ideas?
juan_gandhi: (VP)
Ok, so product type is ok, we have them in languages.

Any solution for a pullback "type"?

Or an equalizer type?
juan_gandhi: (VP)
Say, we have Set<T> objects;


(Yes, it's Java)

What happens here. If you declare a function as injective, it can map a set to a set; otherwise, "elements can be repeated"; and map won't be "efficient enough", so an abstract collection is returned. It does not happen if you map a list.
juan_gandhi: (VP)
products and sums in categories

I wonder if you find something new for you there. Comments wholeheartedly welcome.
juan_gandhi: (VP)

кто про что, а озабоченный про категории

just wanted to dispel some misunderstandings
comments are wholeheartedly welcome
juan_gandhi: (VP)

This is a VERY gentle/simple introduction to categories. If you know what an adjoint functor is, you won't be interested in opening this.

Comments, bugs, suggestions, ideas, questions, queries are extremely welcome.
juan_gandhi: (VP)
тут репост, но неважно

Что интересно - выдумают (а точнее, откроют для себя, после ознакомления с HoTT или элементами теории категорий) какую-нибудь хрень в Хаскеле, тут же где-нибудь в Скале или в С# подхватят; потом Бьярне, который не знает, почему функциональное программирование провалилось и не оправдало надежд, прочитает, ну или ему прочитают, и вот в С++ уже появляется новая революционная фича - хотя, казалось бы, С++ был уже само совершенство до того, и вся эта функциональщина ваша не приносит никакой пользы и только ухудшает эффективность.

До тех пор, пока Бьярне не скажет, что вот эта именно фича, это своевременно и давно пора. Конечно, настанет момент, когда они и от первичности материи откажутся, но он ещё за горами.

И все счастливы; и всем даже кажется почему-то, что С++, будучи совершенством, стал ещё бoльшим совершенством, и развиваться дальше некуда, но нет предела совершенствованию.

Тут можно было бы привлечь индукцию Нётер и её связь с аксиомой фундирования (я на днях обнаружил, что эту связь я когда-то давно переоткрыл, типа лет через 50 лет Эмми - и думал, о, как здорово!).


juan_gandhi: (Default)

March 2017

    1 2 3 4
5 6 7 8 9 1011
12 13 14 15 16 17 18
19 20 21 22 23 24 25
26 27 28 293031 


RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Mar. 29th, 2017 09:09 pm
Powered by Dreamwidth Studios