Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nforum nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022

    starting something, to go alongside necessity and possibility

    (will adjust page name in a second)

    not much here yet, though, under construction

    v1, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022


    v1, current

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022

    added the quote by Heisenberg

    v1, current

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 1st 2022

    Added reference

    diff, v2, current

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2022

    Concerning the nonlinear case, why not take a case from everyday life and see how we’d speak about it. So letting the type of variation, DayDay, be days of the week, we might take the type of hours in the day, HourHour, numbered from 1 to 24. Base change takes HourHour to a copy of HourHour over each day.

    In TypeType the (co)unit maps pass from the type, HourWeekHourWeek, of hours in the week to HourHour and from HourHour to HourPerDayHourPerDay, the type of assignments of an hour to each day.

    (15:00, Thursday) is sent to 15:00, which in turn is sent to 15:00 any day.

    HourWeekHourWeek provides definite times to meet.

    Perhaps we might say of HourHour that it is as yet only potential. “What time shall we meet? 15:00. Yes, but which day?”

    How would we speak of HourPerDayHourPerDay, an element of which would be ((13:00, Monday), (09:00, Tuesday), (22:00, Wednesday),…)? All of the information is there, but we don’t have the time fixed yet as we don’t know the day.

    HourWeekHourWeek seems the most natural one, worthy of a simple term, such as ’definite’ or ’determined’.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    Okay, let’s get to the bottom of this linguistic riddle.

    On the one hand, it is true that once we have a term t: BP=b:BPt \;\colon\; \star_B P \;=\; \underset{b \colon B}{\coprod} \; P in the coreader comonad, it is “definitely any” of the types P bP_b, b:Bb \colon B, where here P b=BP_b = B for all b:Bb \colon B.

    This is what i used to be building my linguistic intuition on, too.

    But putting the emphasis on the collection of all such terms, it reads more like being “definitely any” of these types.

    Namely, the coproduct produced by the coreader comonad inevitably behaves much like that produced by a maybe monad or exception monad, and their interpretation is decidedly as non-definite.

    So I come to think that t: BPt \colon \star_B P is not really to be addressed as a “definite typing” unless regarded after the fact as in “we now have a definite term tt”, which however is not the meaning we are after.

    It might indeed be better if we try to stick to speaking as functional programmers, in order to figure out the right linguistic value of the coreader.

    For instance, in a case like the maybe-monad, the functional-programming terminology is linguistically rather straightforward: To say that t:Maybe(Bool)t \colon Maybe(Bool) is almost literally to say in ordinary language that “the term tt may be of type BoolBool”.

    We should ask from this perspective how to pronounce the “coreader” B\star_B. Then it seems to be more something like this:

    • t: BPt \;\colon\; \star_B P means something like: “tt is given for any index b:Bb \colon B:

    So maybe – thinking out aloud here – the correct modal adjective is – “anyways” – which is really close to what we need if we read it as: “in any event” or “in one way or another”(!)

    Then our modal transform would be:

    • anywayspotentiallyindefinitelyanyways \Rightarrow potentially \Rightarrow indefinitely

    What do you think?

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2022

    Ok, good. So the operator acts on the type. But then why the difference with MaybeMaybe where the paraphrase of Maybe(Bool)Maybe(Bool) speaks of BoolBool, and yet the paraphrase of t: BPt \;\colon\; \star_B P doesn’t speak of PP? And is it really any? That sounds to me more like a functional assignment.

    Instead of

    • t: BPt \;\colon\; \star_B P means something like: “tt is given for any index b:Bb \colon B

    isn’t it more

    • t: BPt \;\colon\; \star_B P means something like: “tt is a value in PP for some (or other) index b:Bb \colon B?

    BP\star_B P is ’some (copy of) PP’.


    • t: BPt \;\colon\; \circ_B P means something like: “tt is a value in PP for each index b:Bb \colon B

    I’m reminded of that intricate treatment of each, every, any, all and some by Vendler:

    • Zeno Vendler, Each and Every, Any and All, Mind New Series, Vol. 71, No. 282 (Apr., 1962), pp. 145-160. (JSTOR)

    They line up in somewhat surprising ways. Sometimes it has a linear logic feel of available resources:

    • I can afford a/some dish.
    • I can afford each/any/every dish.
    • I can afford all dishes.

    Sometimes it refers to whose choice it is, again linear logic-like:

    • I’ll give you an/some apple.
    • I’ll give you any apple.

    These in turn aren’t

    • I’ll give you each/every apple.

    And here ’each’ sounds odd, unless one adds something like ’…in turn for you to inspect’.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022
    • (edited Nov 2nd 2022)

    and yet the paraphrase of t: BPt \;\colon\; \star_B P doesn’t speak of PP?

    Oh, it does: If we agree, we would write t:Anyway(P)t \;\colon\; Anyway(P) and read it (following the thesaurus) as:

    “The term is of type PPin one way or anotheranywaysomehow or other.

    Seems to make good sense to me.

    Also, it’s not really different from your suggestion: “some (or other)”, is it? But we need a shorter version of that as a name for a modality.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2022

    Ok. I prefer ’some’ featuring in the expression than ’any’. Not in the truncated existential quantifier sense - some, I don’t know which. But in the specifying sense.

    BP\star_B P has the feel of SomeB(P)Some B (P). Then maybe ’how’ stands in for BB, and we have Somehow(P)Somehow(P). Or Someway(P)Someway(P).

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    All right, I like that!

    So then our sentence reads

    somehowpotentiallyindefinitely somehow \Rightarrow potentially \Rightarrow indefinitely ”.

    This looks good. Now the weakest spot seems to actually be “indefinitely”. It feels more clunky than the other two now and also it tends to be read with a temporal connotation that we don’t want here.

    I am undecided, but maybe “randomly” wasn’t that bad, after all?

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    If we pronounce the reader \bigcirc as “randomly”, then “random access memory” would formally be the modality of ” randomly somehow “.

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2022

    Anyhow(P)Anyhow(P) or Everyhow(P)Everyhow(P)?

    ’Everyhow’ is archaic: in all ways; in every manner; however; by whatever means.

    ’Anyhow’: in any way whatever; in any case; at all events; in a careless manner; haphazardly

    Perhaps, Anyhow(P)Anyhow(P) then.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022
    • (edited Nov 2nd 2022)

    I see. That’s good.

    But then “potentially” in

    somehowpotentiallyanyhowsomehow \Rightarrow potentially \Rightarrow anyhow

    does not sound right, after all, does it: One wouldn’t want to say that something holds “anyways” as soon as it holds “potentially”.

    The adjective in the middle should express truth without reference to the “how” in “somehow”, “anyhow”.

    Indeed, the composite implication “somehowanyhowsomehow \Rightarrow anyhow” sounds wrong.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    The problem is that on in-dependent type we can’t really say “how”, at all, because that would involve referring to the context.

    So instead of “somehow” it is more like “alternatively”: We pick some alternative, but without really saying how.

    This leads me to suggest something like:

    alternativelypotentiallyrandomlyalternatively \Rightarrow potentially \Rightarrow randomly

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2022

    These middle terms in a sense should be doing nothing, no? After all the necessarilyactuallypossiblynecessarily \Rightarrow actually \Rightarrow possibly is WP(w)P(w) WP(w)\Box_W P(w) \Rightarrow P(w) \Rightarrow \lozenge_W P(w), so that Actually(P)(w)Actually(P)(w) is P(w)P(w).

    Unless we imitate modal logic and see actualisation as an operator which takes a modal proposition to a plain proposition, which we might take to be pullback along the map which singles out the actual world, a:*Wa: \ast \to W. After this pullback we have (for all worlds PP \Rightarrow this world PP \Rightarrow some world PP).

    But then in the in-dependent setting there isn’t anything like this actualisation to be done. Whatever we have as the middle term can’t do anything to the type.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    Yes, the middle adjective is not for an operator, it indicates the context that we are in.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022
    • (edited Nov 2nd 2022)

    It’s becoming a bit of a goose chase, but let’s just keep going while we have the momentum:

    One observation is that B\star_B and B\bigcirc_B ought to be about the same kind of randomness, just that the first is about specific random inputs (namely to coKleisli morphisms of the coreader comonad) while the latter is about unspecific random outputs (produced by Kleisli morphisms for the reader monad):

    If we think of both reader and co-reader as dependent on a potentially unspecified global parameter b:Bb \colon B, then

    • a coreader coKleisli program BD 1D 2\star_B D_1 \to D_2 reads in random but fixed data d:b:BD 1d \;\colon\; \underset{b \colon B}{\coprod} D_1 and it proceeds with that fixed data,

    • a reader Kleisli program D 1 BD 2D_1 \to \bigcirc_B D_2 outputs random and unspecified output data d:b:BD 2d \,\colon\, \underset{b \colon B}{\prod} D_2, preemptively prepared for all possibilities.

    If we read “randomly” in this sense as “random but fixed” input, then this goes to the beginning of our modal sentence, while “indefinitely” can stay on the right:

    randomlypotentiallyindefinitelyrandomly \Rightarrow potentially \Rightarrow indefinitely

    This is beginning to make more sense: If something definitely holds, but in a random way, then at the very least we deduce that it can potentially hold at all. If then we don’t even recall the definite random data, we remain with something random and indefinite.

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2022

    Seems a little odd to extract “randomly” from just one of “random but fixed” and “random and indefinite”, but I think maybe I’m missing something about what the end result should look like.

    I’m in the process of putting a grant proposal together and in conversations with colleagues promoting the (your) line that with the mathematics right and the logic right for quantum physics, there’s really little “interpretative” work left to do. This met with some scepticism. Think of the twin-slits experiment, they said, how can that not be something odd, demanding interpretation?

    So back to the task here, is that the idea that phrasing quantum physics in the right logic, the right modal HoTT, then with a good gloss of natural language words for modalities, the physics becomes plainer? Then we’d better first get the nonlinear case as best we can?

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022
    • (edited Nov 3rd 2022)

    To narrow in on the “correct” linguistic pronounciation of these monads, we can also ask: “What is it that a B\bigcirc_B-algebra handles?”, in the sense of monad-algebras as being “effect handlers” in programming (as Uustalu – and maybe only he – usefully highlights at the beginning of his Lecture 2).

    Now, a B\bigcirc_B-algebra is a gadget that knows how to take a list of data dependent on an unspecified parameter and turn it into definite data. So it “handles indefiniteness”, in a useful sense.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2022
    • (edited Nov 3rd 2022)

    What language does one use for the dual?

    “What is it that a B\star_B-coalgebra co-handles”? A B\star_B-coalgebra is a gadget that takes a list of data and returns data plus a specified parameter.

    Surprisingly, aside from some article titles at graded modality, the only reference to ’coeffect’ we only have is at graded monad:

    In computer science, monads model effects and comonads coeffects.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022
    • (edited Nov 3rd 2022)

    I believe the language for co-monads as co-effects should be like so:

    • Where a Kleisli morphism is a program that causes an external effect

      a co-Kleisli morphism is a program subject to an external effect.

    For instance

    • the reader monad causes the effect of producing indeterminate data,

      while the coreader comonad is effected by a random choice of data.


    • where a monad algebra handles (and so makes disappear) effects that were caused by programs

      a co-monad co-algebra produces an effect that programs get subjected to.

    Specifically for the co-reader:

    All those coreader coKleisli programs are sitting there waiting for the dice to fall and them to run on the resultuing value. The coreader coalgebra is the kind of black box that produces the actual value all these programs are waiting for.

    In particular, a coreader coalebra could produce a random element in the sense of random number generators. Or it could ask the user to produce such an element. Or it could compute such an element by some procedure that it happens to know about . In any case, the result will be random as in “random access memory” from the point of view all those coreader coKleislis waiting to be provided with such input.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022

    Maybe one should speak of cause and effect.

    Where a monad encodes a kind of effect of programs

    a comonad encodes a kind of cause for programs.

    In the case of (co-)readers we’d be speaking of the types of

    • indefinite effects


    • random causes.
    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2022
    • (edited Nov 4th 2022)

    Let’s see if I get this via the pair state monad and store comonad.

    The state monad causes indeterminate data on an unknown state and a way to update these states. (This generates a form of randomness, as here.) An algebra makes this effect disappear.

    The store comonad is effected by a random choice of state and a way to produce indeterminate data. A coalgebra produces such an effect, and is a kind of lens (as here).

    There must be ways to write this more clearly.

    • CommentRowNumber24.
    • CommentAuthorGuest
    • CommentTimeNov 5th 2022
    • (edited Nov 5th 2022 by Urs)

    [ it’s me, Urs, the system signed me out while I was editing ]

    Incidentally, one sees that computer scientists on the web used to be debating how to really think of what the costate comonad does:

    On Nov 29 in 2010 on r/haskell here, Russel O’Connor (if I am second-guessing the handle correctly?) polled for opinions on how to best think of the costate comonad. He received a fair number of suggestions. His own suggestion (here) was “selector comonad”.

    Curiously, if the time stamps are to be trusted, on the next day, Nov 30 (2010), the same O’Connor (if I am interpreting correctly how he is referred to here?) announces his finding (here) that costate coalgebras are equivalently “lenses” (rather: “very well-behaved lenses”, I gather).

    Not sure if this insight was ever fed back into the question of how to think of the costate monad: If “lenses” is the worthwhile paradigm, shouldn’t it be called something like the “lens reader”, providing programs the context of a lens on their input data?

    Curious here that even the data structure of “lenses” was advertised to capture situations that “computing is full of” and which are a “classical topic in the database literature” (according to the original 2007 article, p. 2).

    So computing has been full of costate coalgebras, all along, and nobody noticed until 2010! Maybe the computing community could have cut some corners had people done their category theory? :-)

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    I have added this pointer:

    and one quote form it (here)

    diff, v4, current

    • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2022

    Interesting to try to make sense of Aristotle’s Physics as a whole. Thomas Kuhn describes how he could make no sense of it by working backwards from Newtonian physics, say, to see how much Aristotle had anticipated. If you do it this way, Aristotle just seems like a bad scientist. Instead you have to see the total picture and how the parts relate.

    So, Aristotle’s idea of motion is very different, including not only locomotion, but the growth of a plant, the changing intensity of a quality, and so on. Change occurs by changing qualities at a place in the substrate, not through the motion of particles. Bodies just are the substrate sufficiently impregnated with qualities.

    This feeds into Kuhn’s argument against science converging on the real. It seems to him that in the path from Aristotle to Newton to Einstein that in some respects the outer two are quite similar, field-theoretic.

    This raises some interesting questions for us. By invoking Aristotle’s terms in the context of quantum physics, are we agreeing with Kuhn about that similarity?

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022

    Probably, instead of reading “Aristotle” it would have been more illuminating to read the notes on Physics made by the builders of the Atikythera mechanism; or those made by the builders of the Pyramids, or those from whoever it was who created the Baalbek megaliths. All lost to time – and what we are left with from all those civilizations now barely serves to provide justification for a good pun in naming a monad.

    • CommentRowNumber28.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2022

    Well, Ok, but then including fragments of Aristotle is just for amusement.

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeNov 10th 2022
    • (edited Nov 10th 2022)

    Maybe I am not following your train of thought.

    I would love for us to have a decent entry to which I could point people as a reference for what Aristotle said about potentiality+actuality and what Heisenberg made of it.

    I tried to add a minimum given what I could glean from what I found in stolen minutes. I know you have argued (here) against writing on the nnLab about philosophical subjects, and please feel free not to, but maybe somebody else reading here could be inspired to join in.

    • CommentRowNumber30.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 10th 2022

    I wouldn’t call that an argument against writing on the nLab about philosophical subjects.

    Writing on the history of philosophical thought is of course completely unproblematic. What Aristotle says about potentiality+actuality is a fine topic, though as I was pointing out in #26 it’s by no means a straightforward business, and really it would need to be embedded in a wider discussion of Aristotle’s Physics. We’d be looking for something like SEP: Aristotle’s Natural Philosophy. (But let’s not let the perfect be the enemy of the good.)

    The issue I was raising on that other thread is whether it’s right to have any entries which treat some or other philosophical topic timelessly, i.e., not as a series of thoughts particular philosophers have had on it, but as a topic in itself. So when in, say, electromagnetism we can start timelessly

    The electromagnetic field is is a gauge field which unifies the electric field and the magnetic field,

    Hacker’s argument is that philosophy doesn’t deliver such timeless statements. History, on the other hand, (including the history of philosophy) does deliver timeless statements – Aristotle thought X, Descartes thought Y, etc.

    The electromagnetic field will likely always be taken to be a gauge field. Physics has delivered us such a concept. We don’t need a great long back story. For Hacker, it isn’t philosophy’s job to do likewise. What the philosopher can do is enter into a dialogue with a practitioner of some other field to help with the process of conceptual clarification, but they don’t come with some special domain knowledge.

    Even amongst those who do see a role for philosophical theorising, just about any SEP article on a topic has little to say of the form ’X is…’, and lots to say about how X has been thought about in many ways, it’s all still highly debated what we should mean by X, etc.

    So an article on agency has an intro paragraph on the kind of scope of ’agency’ and then

    Debates about the nature of agency have flourished over the past few decades in philosophy…

    and off we go with loads of different conceptions and theories.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeAug 4th 2023

    added pointer to:

    • Lorenzo Ferroni, Luca Gili, Non-existent but potentially actual. Aristotle on plenitude (Met. Θ 3-4, 1047b1-6), Revue de philologie, de littérature et d’histoire anciennes, Tome XC (2016) 81-114 [doi:10.3917/phil.901.0081]

    diff, v5, current