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

August 2017

S M T W T F S
   1 23 4 5
6 7 8 9 10 11 12
13 14 15 16 1718 19
20212223242526
2728293031  

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Aug. 21st, 2017 02:50 am
Powered by Dreamwidth Studios