Created complete small category, and moved the proof of Freyd’s theorem to there from adjoint functor theorem.

]]>Added the statement of the Isbell-Freyd characterization of concrete categories, in the special case of finitely complete categories for which it looks more familiar, along with the proof of necessity.

]]>you can define $\Cat$ to be the 2-category of all $U'$-small categories, where $U'$ is some Grothendieck universe containing $U$. That way, you have $\Set \in \Cat$ without contradiction.

Do you agree with changing this to

” you can define $\Cat$ to be the 2-category of all $U'$-small categories, where $U'$ is some Grothendieck universe containing $U$. That way, for every small category $J$, you have the category $\Set^J$ an object of $\Cat$ without contradiction. This way, e.g. the diagram in Cat used in this definition of comma categories is defined. “

?

Reason: motivation is to have the pullback-definition of a comma category in (For others, it’s about the diagram here) defined, or rather, having Cat provide a way to make it precise. Currently, the diagrammatic definition can either be read formally, as a device to encode the usual definition of comma categories, or a reader can try to consult Cat in order to make it precise. Then they will first find only the usual definition of Cat having small objects only, which does not take care of the large category

$Set^I$

used in the pullback-definition. Then perhaps they will read all the way up to Grothendieck universes, but find that option not quite sufficient either since it only mentions Set, but not $Set^{Interval}$ . It seems to me that large small-presheaf-categories such as $Set^{Interval}$ can be accomodated, too, though.

(Incidentally, tried to find a “canonical” thread for the article “Cat”, by using the search, but to no avail. Therefore started this one.)

]]>There are similar notions in the boundary fields already:

* Instituion in the logics and computer science (https://en.wikipedia.org/wiki/Institution_(computer_science))

* category of First order theories and subcategory of geometrical theories as defined by Olivia Caramell (in her book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en&, while I wonder that she mentions that there is some controversy around it http://www.oliviacaramello.com/Unification/Controversy.html)

So - are there some results or maybe it is not possible or it is not interesting to pursue building such category. I have my goals of using such category in the formalization of deep learning and I wonder what is the status of its research? ]]>

Created descent morphism.

In adding links, I discovered that Euclidean-topological infinity-groupoid and separated (infinity,1)-presheaf use the phrase “descent morphism” to refer to the *comparison functor* mapping into the category of descent data. If no one has any objections, I would like to change this to avoid confusion, but I’m not sure what to change it to: would “comparison functor” be good enough?

Created General Theory of Natural Equivalences, partly on the model of the (to me) useful-seeming Elephant. One reason was that I think it can be instructive for people learning more category theory to see this classic transparently commented on in a modern reference work like the nLab.

Another reason was that this is a historical important paper, which I needed an nLab reference for when writing a historical, context-adding section of directed graph, embedding Lawvere’s interesting Como comments into a relevant context, drawing historical parallels.

]]>I added a characterization, reference, and some more examples to absolute colimit.

]]>I have created Locally Presentable and Accessible Categories, with redirect LPAC, since we seem to refer to it a lot. I also added it as a reference to compact object, where it was surprisingly absent.

]]>Current tex file (surely with some mistakes): (output: https://imgur.com/a/BxcuqGE )

% !TeX engine = lualatex

\documentclass[tikz]{standalone}

\usetikzlibrary{cd, arrows, graphs, graphdrawing}

\usegdlibrary{layered}

\newcommand{\cat}[1]{\ensuremath{\mathbf{#1}}}

\begin{document}

\begin{tikzpicture}[>={Stealth}, rounded corners]

\graph [layered layout, nodes={font=\bfseries}]{

Vect -> Mod -> Ab -> {Grp, CMon -> Mon -> Cat};

Grp -> {Loop, ISGrp, Mon};

SGrp -> SGrpd;

Grp -> Grpd -> {SGrpd, pSet, Cat -> SGrpd -> Set};

{UMag, Loop} -> pSet -> Set;

{{ISGrp, Mon} -> SGrp, {Loop, ISGrp} -> QGrp, {Loop, Mon} -> UMag} -> Mag -> Set;

Field -> CRing -> Ring -> Grp;

CRing -> Ab;

Poset -> Set;

Hilb -> IPS -> Norm -> TVect -> Top -> Set;

Hilb -> Ban -> CMet -> Met -> "Top\textsubscript{Haus}" -> Top;

Ban -> Norm -> Met;

TVect -> Vect;

Set -> Rel;

};

\end{tikzpicture}

\end{document} ]]>

The classic way to encounter the theory of categories is via Set Theory via the typical definition we see for categories. We see all kinds of categories that are equivalent to the category of small categories. I wonder about presentations of the theory of categories. To facilitate a discussion, we may need to define what a presentation of a theory is. It may consist of a logical language or even the standard presentations of algebraic structures. For instance, a presentation of the theory of partial monoids would count as a presentation of Categories. The presentation should come with enough structure to analyze all small Categories.

I saw Marsden put together a presentation of categories in terms of string diagrams.

I like to think that string diagrams can be seen as containers. This is a paper about containers. So the idea is that you have a (co)monad that encodes the container for the theory of categories. Could this work?

]]>In the discussion at the bottom of monoidal category, we read:

In fact a strict monoidal category is just a monoid internal to the category Cat. Unfortunately this definition is circular, since to define a monoid internal to Cat, we need to use the fact that Cat is a monoidal category!

And then later

For example, you can define a monoidal category to be a pseudomonoid internal to the 2-category Cat — but nobody knew how to define these concepts until they knew what a monoidal category is!

Doesn’t the same circularity afflict the definition of monoidal category that’s on the page? For example, the associator is given as

$a \;\colon\; ((-)\otimes (-)) \otimes (-) \overset{\simeq}{\longrightarrow} (-) \otimes ((-)\otimes(-))$But this doesn’t make sense if taken literally. You cannot have a natural transformation between functors on different domains, and the domain of these functors are not the same. The domain of the left functor is $(\mathcal{C}\times \mathcal{C})\times\mathcal{C}$ whereas the domain of the right functor is $\mathcal{C}\times (\mathcal{C}\times\mathcal{C})$. Of course those two categories are isomorphic, and using that isomorphism, we can make sense of the definition. But that’s using the monoidal structure of $\text{Cat}$! We’re being circular in exactly the same way as we would if we defined a monoidal category as a (pseudo)monoid in the monoidal (2-)category $\text{Cat}$!

I guess it’s not circular in any formal sense, since we can just observe that any cartesian category has canonical isomorphisms $(\mathcal{C}\times \mathcal{C})\times\mathcal{C}\cong \mathcal{C}\times (\mathcal{C}\times\mathcal{C})$ and we can just insert that into the definition as needed, without commenting that it is part of a monoidal structure on the ambient category. The same applies to any monoid in any cartesian category. In particular, I think it’s not formally circular to define a (weak/strict) monoidal category as a (pseudo) monoid in $\text{Cat}$.

Shouldn’t that equivalent definition be mentioned higher in the article, since it’s valid and not really circular?

And shouldn’t the article be more explicit about this, about using the cartesian associator and unitors of $\text{Cat}$, given that it’s basically an article about the need to be careful and rigorous about the axioms of associators and monoidal structures?

Also, is there some more coherent, higher categorical way out of this circularity, other than than just capping it with a cartesian structure at some level of the higher categorical ladder?

]]>I´m Software Architect experienced in Optimization Algorithms and Distributed Expert Systems. I have recently developed a technique which breaks limitations on Neural Persistence, on which I want to release my research article. However, I think that it is recomendable firstly to introduce appart the philosophical proceeding using fibred categories as a powerfull innovation in research level. I want to review and discuss this publicly for a better acceptance before resarch article comes out.

Please find out below and give me your feedback:

http://ixilka.net/publications/innovations_in_maths.pdf

]]>A bit of a long shot, but since there is a Hegel page on ncatlab, I thought it would be interesting to see if there are any thoughts on the very interesting way Ruth Garett Millikan uses the word Category in her 1984 Book Language, Thought and Other Biological Categories. Btw, this can be thought of as a biological extension of Game Theoretical work by David Lewis on Language, such in his Languages and Language. There are categories of games, and even as coalgebras, so why not categories that would allow one to think of the biological, understood as that which reproduces.

Her departure point is that what seperates the physcial from the biological is the concept of reproduction. She starts with an example of a photocopier. Paper comes in, a copy comes out. There is clearly something that is the same from the input and the output, but that is not that the atoms are the same. This she argues can only be understood by taking the function of the photocopier into account. Its purpose is to make patterns of ink on a new paper that match those on the input, and other things can vary: eg. paper quality, color, etc… need to be the same.

With devices this function is (for us) easy to ascertain. For living things though as there is no manual for each species we need to work out what is the case by observing and theorizing. Here statistics by itself won’t do: she uses as example that most sperm never fertilise an egg. One has to look at the role the organ plays in the evolutionary survival of the organism, even the prehistory of that organism.

She then goes on to show how language fits then into that category, as words are reproduced from speaker to listener, and their function she argues is referential correctness. But not always: only at key points. So a single person could take a massive computer hard drive and fill it with “2+43=3” and that would not render arithmetic as we understand it nonsense, by overwhelming all existing literature on the subject with falsities. This is already very enlightening in so far as it I think correctly highlights the importance of etymology in the meaning of a word.

]]>Started pure subobject. I wish someone would tell me the intuitive reason for their importance though!

]]>Wiki has interesting chapter https://en.wikipedia.org/wiki/Adjoint_functors#Solutions_to_optimization_problems that adjoint functors can be used for optimization, I guess more in the sense of finding optimal objects, structures. Is this original idea whose first exposition is in the wiki article or maybe there are available some references and elaborations of this idea? It would be good to know them? References will suffice, I can study them further.

Also, I guess, such optimization can use for solving the “optimal, paradox free deontic logic” as sketched in my previous question https://nforum.ncatlab.org/discussion/9838/category-of-institutions

]]>As far as I understand - then each institution is designed for some logic. It has two categories - one for syntax (whose objects are signatures) and one for models, effectively - each pair of objects in those categories describe one theory for the logic of this institution.

My question is: are there efforts to construct category of institutions - whose objects would be some logic?

I am beginning to read https://academic.oup.com/logcom/article-abstract/27/6/1753/2687725 and the logical framework mentioned in this articles, seems to be the step in this direction, but this article is somehow detached from the other papers in institutional model theory, so, some comments would be welcome.

Applications sometimes require to construct logic with some peculiar properties, e.g. field of normative reasoning and deontic logics is in search of paradox-free (purely philosophical notion, axiomatic level) deontic logic. So - maybe one can construct category of institutions and then find some universal property, some distinct object which would be the sought after deontic logic with excellent properties?

]]>My question is - what can we deduce about objects and morphisms of this category from the properties of this catgory? Even more - maybe we can recover from the properties of the C the full structure of the objects and morphisms.

E.g. each logic can be assigned the tuple called institution (e.g. https://kwarc.info/people/frabe/Research/GMPRS_catlog_07.pdf and https://www.amazon.co.uk/Institution-independent-Model-Theory-Studies-Universal-ebook/dp/B00KTHC9AI) which is tuple of categories and functors. There are catalogized around 2.000 different logics, not all of them have their institutions invented but maybe all they can have institutions. There is urgent need to devise new logics and to quickly check the properties of newly minted logics, i.e. are they complete and sound. E.g. there are dynamic action logics from the one side and there are linear logics with temporal, spatial, epistemic and some other modalities, but there is no good example of the logic that combines both aspects - dynamic actions and substructural modalities.

So - maybe we can work at the institution level and devise in the first step the tuple of categories and functors with some properties that can go into the institution of the future logic and after then we can infere the exact objects and morphisms for the new minted categories. E.g. instutions have category of signature, so - maybe we can recover signature from the properties of the category.

That is one example. But maybe there are more example where such approach can be desirable.

I have asked the same question in math.stackexchange https://math.stackexchange.com/questions/2821628/algorithms-and-procedures-to-recover-objects-and-morphisms-from-the-properties-o but there is quite aggresive stance against it and it is being voted to be closed.

I have to hear some thoughts about this deduction process. Maybe there are some good literature on this? ]]>

I could not understand the proof of the fact that if a vector space $V$ over a field $k$ is dualisable in the monoidal category $\mathbf{Vect}_k$ then it should be finite dimensional. I understand that the image of $k$ under the unit is a $1$-dimensional subspace, but why should this imply the finite dimensionality of $V$? I would be thankful if someone could provide me the complete proof or a pointer to it.

With my regards,

partha

]]>I want to record a certain lemma on the nlab that is rarely made explicit (slight variation here: https://arxiv.org/abs/1112.0094).

The theorem is that if you have a profunctor $R$ from $C$ to $D$ and it is representable as a functor $F : C \to D$ then the action of $F$ on morphisms is uniquely determined by $R$ and the representation isomorphism.

This explains the initially strange feature of type theoretic connectives, which have semantics as functors but we never actually define their action on morphisms because we can derive the action from the introduction and elimination rules.

My question is should this get a page on the nlab, called I guess “Representability determines Functoriality” or something like that? Or should I try to find some existing page?

And a meta-question is should I err on the side of just making a page with whatever name I feel like or come to discuss the name here on the nforum? Is it easy to change names of pages after the fact?

]]>I’ve just seen an interesting abstract construction in this paper by Mellies and Tabareau on page 19 and I’m curious if people have other examples.

They call it the “fingerprint”. Given 3 categories $A,B,C$ and adjunctions from $A$ to $B$ and $B$ to $C$ you get a monad and a comonad on $B$, and so for every object $b \in B$ a morphism $f_b : W b \to b \to M b$. If $B$ further has an orthogonal factorization system, then you can recover (up to iso) $b$ from this map and then it is called the “fingerprint” of $b$ (since it uniquely identifies $b$). By the adjunction this map can actually be represented as a morphism in $A$ or $C$ as well, so this means any object of $B$ can be represented by a morphism in $A$ or $C$.

In that paper the example they give is that $A$ is Cat, $B$ is MultiCat and $C$ is MonoidalCat with the (hopefully) obvious adjunctions. Then the fingerprint of a multicategory $M$ is a morphism $i : Unary(M) \to Contexts(M)$ in Cat from the category of unary morphisms to the monoidal category of “contexts” that has sequences of objects of $M$ as objects and “substitutions”/sequences of arrows of $M$ as arrows.

This seems very similar to the presentation of models of simple type theory taking as objects contexts and then having a subset of display objects to represent the actual types. In fact, I think you can make this presentation an instance of “fingerprint” if you take $A$ to be Set and compose with the discrete cat/set of objects adjunction to get an adjunction from Set to MultiCat.

The construction is obviously very general though, does anyone see any other natural examples (or perhaps a different name for fingerprint)? I would hope that a presentation of models of dependent type theories would have a similar formulation, but I’m not sure what the categories would be. $C$ is probably locally cartesian closed categories and maybe $A$ is Cat but then what is $B$?

]]>Created a short page for quasi-Borel spaces

]]>**Changes-note**. Changed the already existing page 201707071634 to now contain a different svg illustration, planned to be used in an integrated way in pasting schemes soon.

**Metadata.** Like here, except that in 201707071634 symbols (arrows) indicating what is to be interpreted to 2-cells are given, in the same direction as in Power’s paper.

Changed 201707051620.

**Metadata.** by-and-large, cf. this thread.
A difference to 201707051600 is that here what A 2-Categorical Pasting Theorem, Journal of Algebra 129 (1990) calls a “boundary of the face F” is indicated by bold arrows.

EDIT: (proof of necessity of hypothesis in [A 2-Categorical Pasting Theorem, Journal of Algebra 129 (1990] and relevance to 201707051600 temporarily removed, to make it more uniform)

]]>