Typed Category Theory?

145 Views Asked by At

This small book (or long paper) describes objects and morphisims in a cateogry as having types. He also talks about pre-categories as categories with typeless objects and morphisims.

While I am totally in favor of forcing types on objects, is this standard? Can objections arise from a certain field when taken this approach?

1

There are 1 best solutions below

0
On

Let's say that in category theory is standard to reguard the morphisms as having a specified source and a specified target, so morphisms should always be typed in your sense.

Beside that I would rather avoid to call those things pre-categories, mainly because in category theory that term is already used to denote other things.

Using of untyped morphisms is usually strongly discouraged because is could rise complexity in formal proof.