we were lacking an entry *realizability* that points to all the related entries (and in fact some entries were asking for just “realizability”).

So I started one. Put in the following Idea-paragraph:

]]>The idea of

realizabilityis essentially that of constructivism, intuitionistic mathematics and the propositions as types paradigm: for instance constructively a proof of an existential quantification $\underset{x\in X}{\exists} \phi(x)$ consists of constructing a specific $x \in X$ and a proof of $\phi(x)$, which “realizes” the truth of the statement, whence the name (e.g. Vermeeren 09, section 1).

I have added the following paragraph to *calculus of constructions*, I’d be grateful if experts could briefly give me a sanity check that this is an accurate characterization:

]]>More in detail, the

Calculus of (co)Inductive Constructionsis

a system of natural deduction with dependent types;

with the natural-deduction rules for dependent product types specified;

and with a rule for how to introduce new such natural-deduction rules for arbitrary (co)inductive types.

and with a type of types (hierarchy).

I was involved in some discussion about where the word “intensional” as in “intensional equality” comes from and how it really differs from “intenTional” and what the point is of having such a trap of terms.

Somebody dug out Martin-Löf’s lecture notes “Intuitionistic type theory” from 1980 to check. Having it in front of me and so before I forget, I have now briefly made a note on some aspects at *equality* in the section *Different kinds of equalits* (below the first paragraph which was there before I arrived.)

Anyway, on p. 31 Martin-Löf has

intensional (sameness of meaning)

I have to say that the difference between “sameness of meaning” and “sameness of intenTion”, if that really is the difference one wants to make, is at best subtle.

]]>I found the organization at *Zorn’s lemma* a bit rough, so I have tried to smoothen it out a bit

For instance

at one point it had suddenly said “proof of the converse” without a clear statement of the other direction having appeared before. I have created two Theorem-environments and tried to make the statements clearer.

the Idea-section had started out saying that “Zorn’s lemma is a trick”. I think that’s misleading or at least misses the important nature of the thing, so I rewrote that and expanded a bit.

But the foundationalists among you please check!

]]>Am trying to get some historical citations straight at *linear type theory*, maybe somebody can help me:

what are the original sources of the idea that linear logic/type theory should generally be that of symmetric monoidal categories (“multiplicative intuitionistic LL”)?

In order of appearance, I am aware of

de Paiva 89 gives one particular example of a non-star-autonomous SMC that deserves to be said to interpret “linear logic” and clearly identifies the general perspective.

Bierman 95 discusses semantics in general SMCs more generally

Barber 97 reviews this and explores a bit more.

What (other) articles would be central to cite for this idea/perspective?

I am aware of more recent reviews such as

but I am looking for the correct “original sources”.

]]>Hello there, am an independent researcher interested in foundations of mathematics though without comprehensive mathematical background. Last year, it caught my attention that physics is formalized in richer kinds of homotopy theory in Science_Of_Logic. There is mention of universal algebra but they choose to work in a kind of synthetic homotopy theory but in my view continuing in universal algebra is more generic and could actually lead to a foundation of math. My math is bad but there could be some truth :

- A unity of opposites is between EM category on a monad and EM category on a comonad. It is subsumed by the ambient category via bireflection
- The bireflection has kleisli lifting as left adjoint inclusion and eilenberg-moore lifting as right adjoint inclusion(a crucial step yet am not so sure)
- The tower of adjoint modalities extends(by monadic decomposition) to any arbitrary ordinal as compared to the one on nlab which I believe is of length 12.
- A foremost assumption of mine is that any tower is equivalent to a fully faithful functor from kleisli category to eilenbergmoore category and that it is an equivalence( at least it is without overly-restrictive conditions). Also, dont forget it is still a tower of unity of opposites
- This now forms a 2-category with adjunctions as 0-cells, a square of adjunctions as 1-cell and transformations as 2-cells. The adjunctions in it are all tripple adjoints.
In my view, this should be formalized in enriched category theory so that every category turns out to be such a tower. The truth of this may be predicted using the idea that enriched categories are just free (co)completions and as such they are equivalent to eilenbergmoore categories, leading to my final step. 7.The 2-category above can be viewed as the category of all categories. The importance of this approach is that universal algebra is equivalent to inductive/recursive types and we can take advantage of this to inductively/recursively define the whole of mathematics and prove all its theorems in a big-bang kind of manner.

As a remark, I observe how bireflection seems to be equivalent to the physical notion of time, as defined in the nlab page, causal locality. This gives me the impression that math is inherently dynamic, that math actually exists objectively. Either way, what prevents a mathemetical theory from being real except causality ? I posted a related question on MathOverflow has there been any serious attempt at a circular foundation of mathematics. I at-least expect that the Hegelian pseudo-code can be formalized on such lines. I would appreciate it if some more advanced mathematician embarks on this or

**corrects me**. Thank you

I noticed that all the paradox-related articles were happily pointing to *paradox*, which however was less than a stub. So I tried to promote it at least to stub-status.

created *Bishop set* to go with the discussion in another thread here

(I have tried to cross-link this to the relant entries, but maybe Toby should look over this. I suppose some further existing nLab discussion of Bishop’s work could be cross linked here)

]]>created a stub (in category: reference) for *Principia Mathematica*, in order to mention its idea of “ramified types”. Added a pointer to this to the lists of references at *type theory* (also at *foundations of mathematics*).

I’d like some kind of comment like “This is the earliest proposal of a type theory.” Or “This is the earliest substantial/formal/sensible/substantive/influential proposal…” or the like. What’s the right thing to say?

Thanks to David Roberts for highlighting this in discussion. Ultimately I’d find it fun to get a historical impression of Russell’s road from the “revolt against idealism” to type theory.

]]>We have several entries that used to mention *Lawvere’s fixed point theorem* without linking to it. I have now created a brief entry with citations and linked to it from relevant entries.

I do not quite understand the discussion under the axiom of extensionality. It says that one can do two variants (of course), one is that equality is taken as a primitive (predicate) and another that the axiom is taken as a definition of equality. Of course, this is in the idea so, but then the second version of the axiom is written unclear (and it is not quite a definition) and the discussion is also unclear. I see it this way: there is a propositional calculus and there is a propositional calculus with equality. “The same” is probably here just an informal way to refer to *the* equality of the propositional calculus with equality, that means a distinguished binary predicate which satisfies substitution axiom, transitivity, reflexivity and symmetry. In that calculus we just state the axiom (not a definition) that the equality can be rephrased via belongness relation. If we work in just a propositional calculus then we can define a relation which we may call equality but we can also call it blablabla. Then we have to state explicitly which properties, possibly weaker than required in the propositional calculus with equality hold for that relation (I am not quite sure how entry extensional relation solves this, in particular, should we now prove the substitution axiom for equality). Now, one should do that version precisely. In calculus with equality there is no space for two versions as far as I see: equality is given (distinguished) by the propositional calculus with equality, we can only characterize it.

New entry categoricity and a slight extension of the stub abstract elementary class.

]]>The page fully formal ETCS is convincing regarding the foundation of the **Category of Sets** as a first order theory. Good !

What about the formal defintion of **FUNCTOR** that implies the connection between two categories ?

Usual textbooks are defining a **FUNCTOR** as two **MAPS** with some additonnal properties. The first **MAP** is between two **COLLECTIONS** of objects. The second **MAP** is between two **COLLECTIONS** of arrows. But these usual textbooks never define **MAP**, neither **COLLECTION**.

What are the formal systems capable to express the concept of **FUNCTOR** ?
Do those systems rely on set theory ? On some type theory ?

It is possible (may be not handy) to setup a first order theory that formalizes in complete autonomy both the concepts of **CATEGORY** and **FUNCTOR** ?

1) Is there a formalization of SEAR anywhere, like for example as a Coq/Agda/Lean library or the like? Just being able to see a fully formalized version & proving the basic theorems would help a lot. As I understand it, full SEAR requires some kind of dependent types in order to express indexed families of sets, and "property" as expressed in the nLab needs some kind of definition?

2) If you remove replacement to get the ETCS-like fragment, can the axioms be expressed purely in first order logic? Or does it still need some form of type theory? What gets lost, other than not being able to formulate products of an arbitrary number of non-isomorphic sets?

3) (possibly trivial but not immediately obvious since I have a hazy understanding of what is allowed by the axioms) In that first order fragment, is it provable that the lattice of relations from A to B is complete, since infinite conjunctions and disjunctions are generally not allowed? ]]>

Am not sure if this page exists on the nlab, but I think a nice presentation of this proof technique, would be useful in the development of **“new ways of doing mathematics”**. I would also like to know of other proof techniques in category theory that are useful but happen to be unpopular, maybe a page can be created to handle such? I would appreciate an example that illustrates transformation of a proof in theory A to a proof in theory B(a concept we may have taken for granted? I don’t know). You can view Olivia Caramello’s general idea

I had given it an $n$Lab page already a while back, so that I could stably link to it without it being already there:

Now it’s even “there” in the sense of being incarnated as a pdf.

]]>Started literature section with several references at forcing.

]]>Naturalness in Category Theory is a difficult notion to pin down. Here is some discussion about naturalness.

I try to study and generate applications of Category Theory to the natural world. I believe that naturalness has been a guiding principle in my work over the years. Another principle that has guided me is Occams’s razor. I get the feeling they may be related, but I have never seen this written about. Does anyone have any thoughts on this?

I have been developing ideas about science couched in the language of monads. They seemed rather natural to me. I am now discovering sketches, but have a very limited understanding of both of these. They both seem like a way to have natural presentations of theories or analysis of ideas. Is one more natural than the other? I feel that monads are more natural, but that might just be because I don’t understand sketches very well. I think monads are more natural because there is this effect that, when you are looking for a given monad, it may only exist on a particular category. It forces you to accept the particular site where everything that ought to be true, is true. Cleverness, or brittle constructions are not as useful.

I suppose the counter argument could be made that sketches work by choosing the kinds of limits you are going to use and then you can achieve various presentations of theories given that kind of limits you chose. So, you work in the universe or logic of particular limits and all things that ought to be true with those limits are true.

It has been put forth that monads and sketches are not related, in that they don’t present the same kinds of things (or theories). Taking a look at Barr and Well’s CT for computing science text, the first example they give is the “free monoid construction”. How is that any different from the list monad, who’s category of algebras is the category of monoids? Also, we know that you can generate monads from sketches. They are clearly related, and I would argue, presentations of the same things.

Here we see a publication where the authors assert the following

“Lawvere theories and monads have been the two main category theoretic formulations of universal algebra”

I believe Lawvere Theories are just sketches restricted to finite products.

The fact that sketches tend to be more like complicated constructions, would suggest to me that they are less natural than monads.

Why is this all important? Look at this quote in Spivak’s latest paper

“Previous work has shown how to allow collections of machines to reconfig- ure their wiring diagram dynamically, based on their collective state. This notion was called “mode dependence”, and while the framework was compositional (forming an operad of re-wiring diagrams and algebra of mode-dependent dynamical systems on it), the formulation itself was more “creative” than it was natural.”

Naturalness mattered to the tool he choses in his paper, namely the category of polynomial endofunctors on set and their monads

If you read this book by Hosseenfelder, you see that what physics may be in need of now is a new guiding principle, other than the standard understanding of beauty. I am proposing that the new principle which we should be looking for is the categorical notion of naturalness.

]]>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?

]]>I gave *Sets for Mathematics* a category:reference entry and linked to it from *ETCS* and from *set theory*, to start with.

David Corfield kindly alerts me, which I had missed before, that appendix C.1 there has a clear statement of Lawvere’s proposal from 94 of how to think of categorical logic as formalizing objective and subjective logic (to which enty I have now added the relevant quotes).

]]>Created ZFA, about ZF with atoms. I’ve added it to the foundations side bar under material set theories and a stack of links.

]]>I was contacted by somebody involved in *The QED Project*. I have given that an $n$Lab page now, linked to from *proof assistant*, cross-linked with *ForMath*. (Maybe we should have a page *formal mathematics* or the like?)

added to *pure type system* in the Idea-section the statement

In other words a

pure type systemis

a system of natural deduction

with dependent types

and with the dependent product type formation rule.

and to the *Related concepts*-Section the paragraph

Adding to a pure type sytstem

rules for introduing inductive types

possibly a type of types hierarchy

makes it a

calculus of inductive constructions.

Finally I added to the References-section a pointer to these slides

]]>Late last night I was reading in *Science of Logic* vol 1, “The objective logic”.

I see that the idea of cohesion is pretty explicit there, not in the first section of the first book (*Determinateness*, which has the discussion of “being and becoming” that Lawvere is alluding to in the Como preface) but in the second section of the first book, “The magnitude”.

There the discussion is all about how the continuous is made up from discrete points with “repulsion” to prevent them from collapsing to a single and with “attraction” that keeps them together nevertheless.

This “attraction” is clearly just the same idea as “cohesion”. One can play this a bit further and match Hegel’s *Raunen* to formal expressions involving the flat modality and the shape modality pretty well. I made some quick notes in the above entry.

On the other hand, that section 1 about being and becoming seems to be more about the underlying type system itself. Notably about the empty type and the unit type, I think

]]>Recently in an edit of mine Frank Waaldijk found it necessary (here) to replace “intuitionistic” by “constructive”. This alerted me that it would be nice if the distinction were made a bit more transparent in the respective $n$Lab entries. Presently our “constructive logic” simply redirects to “intuitionistic logic”. And while we do have separate entries for “constructive mathematics” and “intuitionistic mathematics”, I find it hard to extract from them their distinction.

I am not going to edit on these matters. This is an alert and a request to the logic experts around here. Maybe if you have some spare energy, it would be worthwhile to improve on this situation of $n$Lab entries a little.

]]>