群论笔记 09

that's depends very much on the structure of the category.In some categories there are lots of morphisms between objects like set — morphism rich category.

If we draw these 4 ojbects( set, type constructor ): Fa, Fb, Ga, Gb

In mathematics, we often say that: from Cat C, we can find the object a can be mapping to a morphism of Cat D; and similarly, morphism of Cat C can be mapping to a Naturality Squre in Cat D.

natural transformation can be something like higher-level thant the commutative graph. So you just can say "there is a Natural trans between 2 functors", then this means that "there are some commutative graphs,these Naturality squares"

and we will have a second semaster lectures, introducing "limit, colimit" — defined on the basis of Natural trans, of course they also can be defined by the commutative graphs. But Natural Trans is a higher-level 'language' to describe. And we can find that product and coproduct are just special cases of limit and colimit.

components of a Natural Trans are morphisms, and you know that morphisms are functions, function can shrunk information — can lose information. If you map one functor into another functor using a natural trans, there maybe lot of information will lost.

Natural Trans acts like sampling from a high resolutin picture, and get a low resolution picture.

seriously :| then you find that: you have some mapping, and you have a invertible mapping:

• function and invertible function will lead to a definition of isomorphism, and a isomorphic objects.
• Natural Trans and invertible Natural Trans must will lead to something — isomorphic functors.

so natural transfomation, is also natural isomorphism.

Natural transformation is just a bunch of morphisms, that means there will be bunch of isomorphism.

Move further, means that all of components are invertible morphism, means every component is isomorphism.

Natural isomorphism are really important.

Functor is mapping between categories, and in Haskell it's endofunctor mapping from ONE category to itself.

Natural transformation is a family of morphisms between two endofunctors.

Family of morphisms, morphism is functin, family of functions that parameterize by a type — which is called polymorphic function.

seriously :|

So,

naturally transformation is a polymorphic function

alpha:: forall a. Fa -> Ga

Notice the difference between polymorphic function and ad-hoc polymorphism. * polymorphic function : apply one function for all type.

define a safeHead

safeHead :: [a]->Maybe a //this is a F[a]->G[a] a NaturalTransformation
safeHead [] = Nothing
safeHead (x:xs) = Just x

and it'll automatically find the different implemention of fmap by different invocator, this scenario List and Maybe. So the whole naturality condition will automatically satisfied.

This will give you a intuition that category theory can be used in programming in a very practical way. You see that from picture above, apply fmap to a List is very expensive. But if compiler knows natural transformation, then convert fmap of List, to fmap of a Maybe, this will save a lot of computing resource

So we know that why call a functor a container, because fmap apply to a container will ONLY modify content inside of the container, it will NEVER change the shape of container.

On the opposite side, the natural trans NEVER modify the contents of the container, what it ONLY dose is change the shape of the container, repackages the container.

fmap :: (a->b) -> (Fa->Fb)

alpha:: forall a. Fa -> Ga

we use polymorphic function a lot, is it a natural transformation?

function from a to List[a], yes it's a natural transformation:

• type a to type a: is just a identity functor on a

so fn:: a->[a] is truely a natural transformation

Like computing the length of a List, it's also a natural transformation, because the a is constant functor, it will ignore its type argument.

So, in general if you have a polymorphic function from an ADT to another ADT, it's a natural transformation.

because ADT as showed before, are functors.

before that we must check the Naturality condition:

Hf * (β * α_a) ? (β * α_b) * Ff=

Diagram chasing, you must make sure all the Naturality condition satisfied.

of course, NT is bunch of morphism, morphism of course is composable, so dose the NT.

But, hold on, what are we talking about? Mappings of Functors, and Functor is mapping of 2 category.

*when refer to a mapping of some thing, you must ask yourself, can I take this "something" back to the basic concept of "object" of category.*

In this scenario, yes we can:

• NT -> morphism
• functor -> object
• ??? -> category

??? = [C, D]

So this scenario: * NT is morphism; * functor is object;

remeber "Category of Category" is a "Cat". remeber that, * functor is the morphism of Cat. * category is the object of Cat.

https://postimg.cc/image/xbly6vrrv/

2-category : has move further one step than "Cat"—category of category, which is the pair category as object.

Hom-set of Cat is set of Functors; Cat often think as a Category of small Category.

Hom-set are trully a set. And then set can be seen as a Category, then we get [C,D] — 2-category.

but wait a minite, in the Category of Category, we have 2 objects: C and D, then [C,D] must also be in the same category with C and D. So:

something like the set: * set = {a,b,c,d} * a ∈ set * c ∈ set * {a,c} ∈ set

but functor of category, is a exponential ADT,

?????? why [C,D] = D\^C

by the partial function, we can see some glue of [C,D] = D\^C, this should be marked as TODO, I ignore the details of this, when this taught at previous lectures, need reviewing.

categorical products as pairs of elements and categorical products with universal construction and projections, they will give you the same result.

the category of functor category[C,D] is same as the D\^C, we start with a product category CXD,and then do the universal construction and we get the exponential objects.

Can we build something instead hom-sets of hom-objects

vertical composition

Is there the natural trans between G * F and G'*F'

and the answer is "Yes"

and it's called β * α.

horizon composition and vertical compoisition

skipped, too long to draw

but definition of 2-category involves both vertical composition and horizon composition of two cells ,and the interchanging law.

we can get isomorphism from the vertical composition ??? They are called left and right unitor.

So, if we start defining the stuff up to isomorphsim, then suddenly from a 2-category we are getting into something called bicategory.

the diff between 2-category and bicategory: * in a bicategory categorical laws are up to isomorphism. * 2-category is more strict than bicategory, becasue categorical laws is equale * bicategory is relaxed version of 2-category.

can not understand, so skipped!!

Lets just talk about bicategory

what if we have a category in which all morphism are inverted.If morphism in a category are all inverted, this category is called groupoid.

So if you start doing the same thing with groupoid,instead of categories, turn out that you can have like n-groupoids and coherence laws are simple for groupoids.

so the groupoid people say to catgory people,you're wrong direction. The correct thing to do is work with groupoid, and in particular if you go with high enough, you know at some point you say well, what's wrong with infinity. infinity groupoid.

infinity groupoid would be something has zero cells – objects . one cells morphism between them, two cells morphism between morphims, three cells between morphisms of morphisms and … so on to inifinity.

It turns out this is exactly the structure of the famous homotopy type theory.

homotopy type theory said that groupoid are the way to go, not categories.