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.

ct4scala

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

http://tinyurl.com/ct4scala

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;



vs



(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)
https://drive.google.com/file/d/0BwRrcixvqFQgcDNsSTFySGFYODQ/edit?usp=sharing

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

just wanted to dispel some misunderstandings
comments are wholeheartedly welcome
juan_gandhi: (VP)
https://docs.google.com/document/d/15UKcOKbvenFOgrmw51pAzzggGM1BmEM89OE74NqJxd0/edit?usp=sharing

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 лет Эмми - и думал, о, как здорово!).

Profile

juan_gandhi: (Default)
juan_gandhi

February 2017

S M T W T F S
    1 2 3 4
5 6 7 8 9 10 11
1213 14 15 16 17 18
19 20 21 22232425
262728    

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Feb. 22nd, 2017 10:05 pm
Powered by Dreamwidth Studios