Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 29th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIn light of Mike and Dan Licata's [paper](http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint.pdf) perhaps we should have a page on 'adjoint logic' I wonder if there's a way of getting at temporal logic without the need for a directed type, $Time$. I mean something temporal seems to happen when you have two adjunctions between four operators, which are dual pairs in some sense. So if $F$ and $G$ are 'dual' in the sense, $\neg F = G \neg$, and likewise $P$ and $H$. And if also, $F \dashv H$ and $P \dashv G$, then they can be interpreted as: > $F \phi$ : "$\phi$ will be true at some Future time", > $G \phi$ : "$\phi$ is always Going to be true", > $P \phi$ : "$\phi$ was true at some Past time" and > $H \phi$ : "$\phi$ Has always been true". It is claimed [here](http://ac-net.org/altmath/temporalization.pdf) that >the author showed that an adjoint pair of modal operators gives rise to a temporal logic. Of course, I'd be wanting to think about general types not just propositions, and then avoiding reliance on $\neg$, just as our version of possibility and necessity doesn't rely on negation.

   In light of Mike and Dan Licata’s paper perhaps we should have a page on ’adjoint logic’

   I wonder if there’s a way of getting at temporal logic without the need for a directed type, $Time$. I mean something temporal seems to happen when you have two adjunctions between four operators, which are dual pairs in some sense. So if $F$ and $G$ are ’dual’ in the sense, $\neg F = G \neg$, and likewise $P$ and $H$. And if also, $F \dashv H$ and $P \dashv G$, then they can be interpreted as:

   $F \phi$ : “$\phi$ will be true at some Future time”,

   $G \phi$ : “$\phi$ is always Going to be true”,

   $P \phi$ : “$\phi$ was true at some Past time” and

   $H \phi$ : “$\phi$ Has always been true”.

   It is claimed here that

   the author showed that an adjoint pair of modal operators gives rise to a temporal logic.

   Of course, I’d be wanting to think about general types not just propositions, and then avoiding reliance on $\neg$, just as our version of possibility and necessity doesn’t rely on negation.

2. • CommentRowNumber2.
   • CommentAuthorDavidRoberts
   • CommentTimeSep 29th 2015
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItex"Future Semiconditionally Modified Subinverted Plagal Past Subjunctive Intentional" Sorry...

   “Future Semiconditionally Modified Subinverted Plagal Past Subjunctive Intentional”

   Sorry…

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexIf we have an internal category $Time_1 \rightrightarrows Time_0$, then on the slice category $C/Time_0$ there are two induced monad/comonad adjoint pairs $F\dashv H$ and $P\dashv G$, whose algebras/coalgebras are contravariant and covariant internal diagrams on $Time$, respectively.

   If we have an internal category $Time_1 \rightrightarrows Time_0$, then on the slice category $C/Time_0$ there are two induced monad/comonad adjoint pairs $F\dashv H$ and $P\dashv G$, whose algebras/coalgebras are contravariant and covariant internal diagrams on $Time$, respectively.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2015
   • (edited Sep 29th 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI think that's an excellent point regarding modalities, the combination of David's question and Mike's reply. For bystanders, if any, I'lljust make explicit what Mike left implicit and mention that to make this come out as intuitively expected, then we'd take the internal category "$Time$" to be an internal poset. It's objects would then be interpreted as the instants of time, its morphisms as the possible translations to the future, and an "internal diagram" over this would hence be thought of as an assignment of a type of states to each instant and a map from past states to future states for each time translation from one instant to the next. Somebody should turn this into an nLab entry...

   I think that’s an excellent point regarding modalities, the combination of David’s question and Mike’s reply.

   For bystanders, if any, I’lljust make explicit what Mike left implicit and mention that to make this come out as intuitively expected, then we’d take the internal category “$Time$” to be an internal poset. It’s objects would then be interpreted as the instants of time, its morphisms as the possible translations to the future, and an “internal diagram” over this would hence be thought of as an assignment of a type of states to each instant and a map from past states to future states for each time translation from one instant to the next.

   Somebody should turn this into an nLab entry…

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 29th 2015
   • (edited Sep 29th 2015)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexSo if the two arrows $Time_1 \rightrightarrows Time_0$ mark the beginning, $b$, and end, $e$, of an interval, we base change along $b$ and then take dependent product and sum along $e$, and vice versa? Let's see, because $$ Hom(\sum_b e^{\ast} C(t), D(t)) = Hom(e^{\ast} C(t), b^{\ast} D(t)) = Hom(C(t), \prod_e b^{\ast} D(t)). $$

   So if the two arrows $Time_1 \rightrightarrows Time_0$ mark the beginning, $b$, and end, $e$, of an interval, we base change along $b$ and then take dependent product and sum along $e$, and vice versa?

   Let’s see, because

   $$Hom(\sum_b e^{\ast} C(t), D(t)) = Hom(e^{\ast} C(t), b^{\ast} D(t)) = Hom(C(t), \prod_e b^{\ast} D(t)).$$
6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2015
   • PermaLink
   Author: Urs
   Format: MarkdownItexThat by itself is the "[primary integral transform](http://ncatlab.org/nlab/show/dependent+linear+type+theory#PrimaryIntegralTransform)", if you wish, through the graph underlying the category $Time$. Then the composition operation in the category gives the (co-)monad structure.

   That by itself is the “primary integral transform”, if you wish, through the graph underlying the category $Time$. Then the composition operation in the category gives the (co-)monad structure.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2015
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRight, and $\sum_b e^*C$ means "there is some interval beginning now and such that $C$ is true at its end", i.e. $F C$; while $\prod_e b^*D$ means "for all intervals ending now, $D$ is true at their beginning", i.e. $H D$.

   Right, and $\sum_b e^*C$ means “there is some interval beginning now and such that $C$ is true at its end”, i.e. $F C$; while $\prod_e b^*D$ means “for all intervals ending now, $D$ is true at their beginning”, i.e. $H D$.

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 30th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI'll add some of this to an entry for 'temporal logic'. Just to be clear, what needs to be said about $Time_1 \rightrightarrows Time_0$? It's not only an [[internal category]], but an internal poset? In more abstract terms, whenever we have two adjoint triples (aka adjoints between adjoints) between the same two categories, $A \dashv B \dashv C$ and $P \dashv Q \dashv R$, we'll have $A Q \dashv R B$ and $P B \dashv C Q$. So that's already generating a modal logic of sorts? Then adding detail to the two triples brings me closer to temporal logic? Also to consider are conditions on time, such as branching futures, dense orderings, unboundedness, and so on. Naturally, I'd want to push the full type picture, i.e., see it working not just for propositions. There's something importantly radical, it seems to me, in the 'propositions as some types' story. Philosophy almost always focuses on propositions. As you may have noticed, I like to take every opportunity to think about what happens in the general situation.

   I’ll add some of this to an entry for ’temporal logic’. Just to be clear, what needs to be said about $Time_1 \rightrightarrows Time_0$? It’s not only an internal category, but an internal poset?

   In more abstract terms, whenever we have two adjoint triples (aka adjoints between adjoints) between the same two categories, $A \dashv B \dashv C$ and $P \dashv Q \dashv R$, we’ll have $A Q \dashv R B$ and $P B \dashv C Q$. So that’s already generating a modal logic of sorts? Then adding detail to the two triples brings me closer to temporal logic? Also to consider are conditions on time, such as branching futures, dense orderings, unboundedness, and so on.

   Naturally, I’d want to push the full type picture, i.e., see it working not just for propositions. There’s something importantly radical, it seems to me, in the ’propositions as some types’ story. Philosophy almost always focuses on propositions. As you may have noticed, I like to take every opportunity to think about what happens in the general situation.

9. • CommentRowNumber9.
   • CommentAuthorDavid_Corfield
   • CommentTimeSep 30th 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI added this [section](http://ncatlab.org/nlab/show/temporal+logic#temporal_logic_in_terms_of_adjoints) to [[temporal logic]]. I guess we needn't have our (better) treatments down the page of what others have written, such as at [necessity and possibility](http://ncatlab.org/nlab/show/necessity+and+possibility#InFirstOrderLogicAndTypeTheory). Aside from queries in #8, I didn't know what to say about the point Urs makes in #6.

   I added this section to temporal logic. I guess we needn’t have our (better) treatments down the page of what others have written, such as at necessity and possibility.

   Aside from queries in #8, I didn’t know what to say about the point Urs makes in #6.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 1st 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> It’s not only an internal category, but an internal poset? I guess. Parallel unequal arrows would mean there would be more than one "time interval" with the same endpoints --- not exactly the way we usually think about time. (-: > In more abstract terms, whenever we have two adjoint triples (aka adjoints between adjoints) between the same two categories, $A \dashv B \dashv C$ and $P \dashv Q \dashv R$, we'll have $A Q \dashv R B$ and $P B \dashv C Q$. Interesting! Yes, that's true. Of course in that situation we also have the more basic adjoint modalities $A B \dashv C B$ and $P Q \dashv R Q$. The meaning of those temporally is less clear -- maybe they degenerate on mere propositions? And there's also the identity-assigning map $Time_0 \to Time_1$, generating another adjoint triple in the *other* direction...

    It’s not only an internal category, but an internal poset?

    I guess. Parallel unequal arrows would mean there would be more than one “time interval” with the same endpoints — not exactly the way we usually think about time. (-:

    In more abstract terms, whenever we have two adjoint triples (aka adjoints between adjoints) between the same two categories, $A \dashv B \dashv C$ and $P \dashv Q \dashv R$, we’ll have $A Q \dashv R B$ and $P B \dashv C Q$.

    Interesting! Yes, that’s true. Of course in that situation we also have the more basic adjoint modalities $A B \dashv C B$ and $P Q \dashv R Q$. The meaning of those temporally is less clear – maybe they degenerate on mere propositions?

    And there’s also the identity-assigning map $Time_0 \to Time_1$, generating another adjoint triple in the other direction…

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 1st 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexInteresting you mention $Time_0 \to Time_1$ as a chain of thought had led me to Urs's monads/comonads and constant paths. Let's see how it went. I was thinking it's odd that despite 'Always' and 'Necessarily' being so similar, they're seemingly produced rather differently. The former by base change and dependent product in $Time_1 \rightrightarrows Time_0$, the latter by dependent product then base change for $W \to {\ast}$ (or $W \to W_0$ in what we called the local case). But then of course we can make the latter more like the former by thinking of the two projections: $PairsAccessibleWorlds \rightrightarrows Worlds$, the other way of rendering an equivalence relation. So then, given the parallel between possibility/necessity and the jet comonad structure ($H/X \to H/\Im(X))$ shouldn't we have a similar rewriting of the latter. I.e., instead of $X \to \Im(X)$ why not $D(X) \rightrightarrows X$, where $D(X)$ is the infinitesimal neighborhood of the diagonal of $X$? Returning to time, given we can give it extra features in the form $Time_1 \rightrightarrows Time_0$, such as being a poset, isn't there an advantage to doing things this way. I mean presumably there's no $Time_0 \to ??$ that will do.

    Interesting you mention $Time_0 \to Time_1$ as a chain of thought had led me to Urs’s monads/comonads and constant paths. Let’s see how it went.

    I was thinking it’s odd that despite ’Always’ and ’Necessarily’ being so similar, they’re seemingly produced rather differently. The former by base change and dependent product in $Time_1 \rightrightarrows Time_0$, the latter by dependent product then base change for $W \to {\ast}$ (or $W \to W_0$ in what we called the local case).

    But then of course we can make the latter more like the former by thinking of the two projections: $PairsAccessibleWorlds \rightrightarrows Worlds$, the other way of rendering an equivalence relation.

    So then, given the parallel between possibility/necessity and the jet comonad structure ($H/X \to H/\Im(X))$ shouldn’t we have a similar rewriting of the latter. I.e., instead of $X \to \Im(X)$ why not $D(X) \rightrightarrows X$, where $D(X)$ is the infinitesimal neighborhood of the diagonal of $X$?

    Returning to time, given we can give it extra features in the form $Time_1 \rightrightarrows Time_0$, such as being a poset, isn’t there an advantage to doing things this way. I mean presumably there’s no $Time_0 \to ??$ that will do.

12. • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 1st 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexSo $Time_0 \to Time_1$ gives rise to the triple (for predicates): $\phi \mapsto \phi$ on diagonal, false otherwise $\dashv$ $\psi(t_1, t_2) \mapsto \psi(t, t) \dashv \phi \mapsto \phi$ on diagonal, true otherwise. Perhaps that doesn't generate any interesting new monads/comonads as it would involve composing two dependent sums, two base changes or two dependent products.

    So $Time_0 \to Time_1$ gives rise to the triple (for predicates): $\phi \mapsto \phi$ on diagonal, false otherwise $\dashv$ $\psi(t_1, t_2) \mapsto \psi(t, t) \dashv \phi \mapsto \phi$ on diagonal, true otherwise.

    Perhaps that doesn’t generate any interesting new monads/comonads as it would involve composing two dependent sums, two base changes or two dependent products.

13. • CommentRowNumber13.
    • CommentAuthorDan Licata
    • CommentTimeOct 1st 2015
    • (edited Oct 1st 2015)
    • PermaLink
    Author: Dan Licata
    Format: MarkdownItexCool idea! There's some work on proof theory of temporal logic, e.g. [here](http://www.brics.dk/RS/95/51/BRICS-RS-95-51.pdf) and [here](http://www.cs.mcgill.ca/~bpientka/papers/ltl.pdf) and [here](http://www.cis.upenn.edu/~jpaykin/papers/popl16.pdf) so it would be interesting to try to connect with that.

    Cool idea! There’s some work on proof theory of temporal logic, e.g. here and here and here so it would be interesting to try to connect with that.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 1st 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexAcccording to the [SEP: temporal logic](http://plato.stanford.edu/entries/logic-temporal/) article, two typical approaches are the 'instant based' and the 'interval based' models of time. >Balbiani, P., Goranko, V. and Sciavicco, G., 2011, “Two-sorted Point-Interval Temporal logics”, in Proc. of the 7th International Workshop on Methods for Modalities (M4M7) (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45 ([pdf](http://www2.imm.dtu.dk/~vfgo/papers/ENTCS-M4M7-Two-sorted%20Point-Interval%20Temporal%20Logics.pdf) is given as an example of treating both at once. With time linearly ordered, it seems there are 13 different relations possible between intervals, these can be used to general different modalities. It seems, according to SEP, also worth expressing 'since' and 'until' >$\phi S \psi$: "$\phi$ has been true since a time when $\psi$ was true". >$\phi U \psi$: "$\phi$ will be true until a time when $\psi$ is true". Do we have the resources? For 'since', $\sum_e (b^{\ast} \psi)$ picks out intervals ending now where $\psi$ held at the beginning. So we need that for one of these, all subintervals with the same beginning has $\phi$ hold at the end (or all subintervals with the same end has $\phi$ hold at the beginning).

    Acccording to the SEP: temporal logic article, two typical approaches are the ’instant based’ and the ’interval based’ models of time.

    Balbiani, P., Goranko, V. and Sciavicco, G., 2011, “Two-sorted Point-Interval Temporal logics”, in Proc. of the 7th International Workshop on Methods for Modalities (M4M7) (Electronic Notes in Theoretical Computer Science: Volume 278), pp. 31–45 (pdf

    is given as an example of treating both at once.

    With time linearly ordered, it seems there are 13 different relations possible between intervals, these can be used to general different modalities.

    It seems, according to SEP, also worth expressing ’since’ and ’until’

    $\phi S \psi$: “$\phi$ has been true since a time when $\psi$ was true”.

    $\phi U \psi$: “$\phi$ will be true until a time when $\psi$ is true”.

    Do we have the resources? For ’since’, $\sum_e (b^{\ast} \psi)$ picks out intervals ending now where $\psi$ held at the beginning. So we need that for one of these, all subintervals with the same beginning has $\phi$ hold at the end (or all subintervals with the same end has $\phi$ hold at the beginning).

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeOct 1st 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> So we need that for one of these, all subintervals with the same beginning has $\phi$ hold at the end All subintervals with the same beginning, or just all subintervals with end in the past? I.e. does "since" make a claim about the future too?

    So we need that for one of these, all subintervals with the same beginning has $\phi$ hold at the end

    All subintervals with the same beginning, or just all subintervals with end in the past? I.e. does “since” make a claim about the future too?

16. • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 2nd 2015
    • (edited Oct 2nd 2015)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>I.e. does “since” make a claim about the future too? There may well be different 'since's if we look closely. I guess in the case >I've been unhappy since you left me expressed at time $t_1$, this means that there's an earlier time $t_0$, or interval $[t_0, t_1]$, where you left me at $t_0$, and I have been unhappy throughout the interval. This last condition might be translated as all subintervals $[t_0, t_2}$ have ends where I'm unhappy. I don't see that I'm committing myself to any claim about my future happiness, though rather odd if on uttering the sentence I suddenly become happy. But who knows the powerful effect of articulating one's emotions.

    I.e. does “since” make a claim about the future too?

    There may well be different ’since’s if we look closely. I guess in the case

    I’ve been unhappy since you left me

    expressed at time $t_1$, this means that there’s an earlier time $t_0$, or interval $[t_0, t_1]$, where you left me at $t_0$, and I have been unhappy throughout the interval. This last condition might be translated as all subintervals have ends where I’m unhappy.

    I don’t see that I’m committing myself to any claim about my future happiness, though rather odd if on uttering the sentence I suddenly become happy. But who knows the powerful effect of articulating one’s emotions.

17. • CommentRowNumber17.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 2nd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOr is your thought that it just needs one interval $[t_0, t_2]$ throughout which I'm unhappy, $t_0$ in the past when I'm left, and $t_2$ in the future? But then this has a subinterval curtailed on the right to now.

    Or is your thought that it just needs one interval $[t_0, t_2}[t_0, t_2]$ throughout which I’m unhappy, $t_0$ in the past when I’m left, and $t_2$ in the future? But then this has a subinterval curtailed on the right to now.

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAh, I think this is where we have to use the fact that $Time$ is a category, so that in addition to the two projections $p,q:Time_1\times_{Time_0} Time_1 \to Time_1$ we have composition $c:Time_1\times_{Time_0} Time_1 \to Time_1$. Now $\phi S \psi$ can be $$ \Sigma_e (b^* \psi \times \Pi_c (e p)^* \phi) $$ (note $e p = b q$). That is, there is a subinterval ending now such that $\psi$ was true at its beginning and $\phi$ was true at all points inside it.

    Ah, I think this is where we have to use the fact that $Time$ is a category, so that in addition to the two projections $p,q:Time_1\times_{Time_0} Time_1 \to Time_1$ we have composition $c:Time_1\times_{Time_0} Time_1 \to Time_1$. Now $\phi S \psi$ can be

    $$\Sigma_e (b^* \psi \times \Pi_c (e p)^* \phi)$$

    (note $e p = b q$). That is, there is a subinterval ending now such that $\psi$ was true at its beginning and $\phi$ was true at all points inside it.

19. • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 2nd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWe could have this temporal logic business cracked in a couple of weeks!

    We could have this temporal logic business cracked in a couple of weeks!

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexHere is a quick stub entry: _[[adjoint logic]]_.

    Here is a quick stub entry: adjoint logic.

21. • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 3rd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI added the contents of #18, and its dual 'until'. $$\phi U \psi := \Sigma_b (e^* \psi \times \Pi_c (e p)^* \phi).$$ But perhaps we also use 'until' in the sense where the condition may not happen, e.g., 'You are grounded until you say sorry'. On another theme, I wonder how far we can go to specifying the features of time that logicians have considered, such as density, continuity, (non)branching. Density, expressed as $F q \to F F q$ puts me in mind of Freyd's construction of the real interval as a terminal coalgebra. (There's probably some work to do in tidying up whether intervals can be points, whether the future includes the present, whether $\phi U \psi$ holds now if $\psi$ holds now, etc.)

    I added the contents of #18, and its dual ’until’.

    $$\phi U \psi := \Sigma_b (e^* \psi \times \Pi_c (e p)^* \phi).$$

    But perhaps we also use ’until’ in the sense where the condition may not happen, e.g., ’You are grounded until you say sorry’.

    On another theme, I wonder how far we can go to specifying the features of time that logicians have considered, such as density, continuity, (non)branching. Density, expressed as $F q \to F F q$ puts me in mind of Freyd’s construction of the real interval as a terminal coalgebra.

    (There’s probably some work to do in tidying up whether intervals can be points, whether the future includes the present, whether $\phi U \psi$ holds now if $\psi$ holds now, etc.)

22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeOct 4th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIn the current setup, with $Time$ a category (so in particular having identity maps, i.e. reflexivity in the case of a poset) I think it follows that intervals can be points, the future does include the present, and $\phi U \psi$ holds now if $\psi$ and $\phi$ both hold now (in general, as defined above it requires $\phi$ to still hold at the instant when $\psi$ becomes true). But if we want to change that, we could let $Time_1$ be the $\lt$-intervals instead of the $\le$-ones.

    In the current setup, with $Time$ a category (so in particular having identity maps, i.e. reflexivity in the case of a poset) I think it follows that intervals can be points, the future does include the present, and $\phi U \psi$ holds now if $\psi$ and $\phi$ both hold now (in general, as defined above it requires $\phi$ to still hold at the instant when $\psi$ becomes true). But if we want to change that, we could let $Time_1$ be the $\lt$-intervals instead of the $\le$-ones.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 4th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIt probably does make sense to let $Time_1$ be the $\lt$-intervals. Otherwise $\phi$ could be true now and at no other instant but we'd have $F \phi$ which is supposed to be “$\phi$ will be true at some Future time”. But then there are no identity morphisms in the category, right?

    It probably does make sense to let $Time_1$ be the $\lt$-intervals. Otherwise $\phi$ could be true now and at no other instant but we’d have $F \phi$ which is supposed to be “$\phi$ will be true at some Future time”.

    But then there are no identity morphisms in the category, right?

24. • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 5th 2015
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexNot sure this is helpful, but the adverb 'now' seems like it should be involved with identity morphisms.

    Not sure this is helpful, but the adverb ’now’ seems like it should be involved with identity morphisms.

25. • CommentRowNumber25.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 5th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI was suddenly reminded of the issue alluded to at [[FQFT]] >In basic quantum mechanics one also demands that >$U(t,t)=id.$ >(While this looks like the most innocent condition, this has technical subtleties for genuine quantum field theory, to deal with which however there exist established tools.) Where's that spelled out? Something about cobordisms and cylinders of different lengths, wasn't it? So an identity cobordism should lead to a identity linear operator between states, yet we need time evolution depending on length. (Or something like that.)

    I was suddenly reminded of the issue alluded to at FQFT

    In basic quantum mechanics one also demands that

    $U(t,t)=id.$

    (While this looks like the most innocent condition, this has technical subtleties for genuine quantum field theory, to deal with which however there exist established tools.)

    Where’s that spelled out? Something about cobordisms and cylinders of different lengths, wasn’t it? So an identity cobordism should lead to a identity linear operator between states, yet we need time evolution depending on length. (Or something like that.)

26. • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 5th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThis is the issue be dealt with [here](https://golem.ph.utexas.edu/category/2006/10/australian_category_theory.html#c005678): >Segal’s definition of a conformal field theory discusses “functors” for which the domain is not a category. There is an associative notion of composition for arrows, but there are no identities.

    This is the issue be dealt with here:

    Segal’s definition of a conformal field theory discusses “functors” for which the domain is not a category. There is an associative notion of composition for arrows, but there are no identities.

27. • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexDoes the adverb "now" actually mean anything in temporal logic? I mean, does "$\phi$ holds now" mean anything different from just "$\phi$"?

    Does the adverb “now” actually mean anything in temporal logic? I mean, does “$\phi$ holds now” mean anything different from just “$\phi$”?

28. • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexSo if we use the $\lt$-intervals, then yes, we have only a [[semicategory]], which in particular implies that our "modalities" are not monad/comonads since they lack units/counits. Which is maybe not a huge problem, but it means we can't axiomatize them in type theory the way we have for all other modalities and comodalities — although we couldn't do that anyway if we're not propositionally truncating, since then they wouldn't be idempotent. I guess if we encode them by breaking them down into $f^\ast$'s and $\Sigma$s and $\Pi$s using adjoint logic, that wouldn't be a problem. Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic?

    So if we use the $\lt$-intervals, then yes, we have only a semicategory, which in particular implies that our “modalities” are not monad/comonads since they lack units/counits. Which is maybe not a huge problem, but it means we can’t axiomatize them in type theory the way we have for all other modalities and comodalities — although we couldn’t do that anyway if we’re not propositionally truncating, since then they wouldn’t be idempotent. I guess if we encode them by breaking them down into $f^\ast$’s and $\Sigma$s and $\Pi$s using adjoint logic, that wouldn’t be a problem.

    Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic?

29. • CommentRowNumber29.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 6th 2015
    • (edited Oct 6th 2015)
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic? Not as far as I'm aware. However, looking around some more, we find Robert Goldblatt in [Logics of time and computation](http://sul-derivatives.stanford.edu/derivative?CSNID=00003782&mediaType=application/pdf) >The most common practice in temporal logic is to regard time as an irreflexive ordering, so that "henceforth", meaning "at all future times", does not refer to the present moment. On the other hand, the Greek philosopher Diodorus proposed that the necessary be identified with that which is now and will always be the case. This suggests a temporal interpretation of $\Box$ that is naturally formalised by using reflexive orderings. The same interpretation is adopted in the logic of concurrent programs to be discussed in §9. (p. 44)

    Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic?

    Not as far as I’m aware. However, looking around some more, we find Robert Goldblatt in Logics of time and computation

    The most common practice in temporal logic is to regard time as an irreflexive ordering, so that “henceforth”, meaning “at all future times”, does not refer to the present moment. On the other hand, the Greek philosopher Diodorus proposed that the necessary be identified with that which is now and will always be the case. This suggests a temporal interpretation of $\Box$ that is naturally formalised by using reflexive orderings. The same interpretation is adopted in the logic of concurrent programs to be discussed in §9. (p. 44)

30. • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI suppose we could always write $\phi \wedge F \phi$ if that's what we mean. Although that might not be compatible with a constructive viewpoint on the temporal ordering. One could I guess also go crazy and have *both* the reflexive and irreflexive orderings hanging around, inducing two different families of modalities.

    I suppose we could always write $\phi \wedge F \phi$ if that’s what we mean. Although that might not be compatible with a constructive viewpoint on the temporal ordering. One could I guess also go crazy and have both the reflexive and irreflexive orderings hanging around, inducing two different families of modalities.

31. • CommentRowNumber31.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexI don't know if "now" is used in temporal logic, but I envisaged it to denote something that it true at a particular time, and not elsewhen. Something like "It is 12 o'clock now". Doesn't "$\phi$", with no context, mean something that is "globally" true?

    I don’t know if “now” is used in temporal logic, but I envisaged it to denote something that it true at a particular time, and not elsewhen. Something like “It is 12 o’clock now”. Doesn’t “$\phi$”, with no context, mean something that is “globally” true?

32. • CommentRowNumber32.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #30, that route has been taken. See [here](https://books.google.co.uk/books?id=Ajsvo6jWNhgC&pg=PA132#v=onepage&q&f=false) in a handbook on temporal logic in AI. It's the difference between the box and the box with plus inside. Re #31, this is all in the context of $Time$. You can base change a timeless proposition to one which is time-dependent but constant, e.g., (1+1 = 2)(t) is always true. Timed propositions can be stated to hold now and at no other time by $\neg P \phi \wedge \phi \wedge \neg F \phi$.

    Re #30, that route has been taken. See here in a handbook on temporal logic in AI. It’s the difference between the box and the box with plus inside.

    Re #31, this is all in the context of $Time$. You can base change a timeless proposition to one which is time-dependent but constant, e.g., (1+1 = 2)(t) is always true. Timed propositions can be stated to hold now and at no other time by $\neg P \phi \wedge \phi \wedge \neg F \phi$.

33. • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRe #31, it's just like how in modal logic, "$\phi$" unadorned means that $\phi$ is true at the current world (or, more precisely, the "truth value" of unadorned $\phi$ is the set of worlds in which it's true), not that it's true in all worlds. And even in natural language, if I say just "it is 12 o'clock", what I mean is that it's 12 o'clock *now*, not that it's *always* 12 o'clock.

    Re #31, it’s just like how in modal logic, “$\phi$” unadorned means that $\phi$ is true at the current world (or, more precisely, the “truth value” of unadorned $\phi$ is the set of worlds in which it’s true), not that it’s true in all worlds.

    And even in natural language, if I say just “it is 12 o’clock”, what I mean is that it’s 12 o’clock now, not that it’s always 12 o’clock.

34. • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@David, your link takes me to a page unavailable for viewing or I have reached my viewing limit for this book.

    @David, your link takes me to a page unavailable for viewing or I have reached my viewing limit for this book.

35. • CommentRowNumber35.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWell, it's just saying there are box modalities * in the strict future * in the strict past * in the present and future * in the present and past * in the past, present and future

    Well, it’s just saying there are box modalities

    • in the strict future
    • in the strict past
    • in the present and future
    • in the present and past
    • in the past, present and future
36. • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGot it, thanks. Sounds like quite a menagerie!

    Got it, thanks. Sounds like quite a menagerie!

37. • CommentRowNumber37.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 8th 2015
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexOK, thanks for clarifying :-)

    OK, thanks for clarifying :-)

38. • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeJan 15th 2016
    • PermaLink
    Author: Urs
    Format: MarkdownItexAdded pointer to the nice [slides](http://dlicata.web.wesleyan.edu/pubs/ls15adjoint/ls15adjoint-lfcs-slides.pdf) that now go with _[Licata-Shulman](https://ncatlab.org/nlab/show/adjoint+logic#LicataShulman)_.

    Added pointer to the nice slides that now go with Licata-Shulman.

39. • CommentRowNumber39.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 7th 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIn view of the Lawverian and so Hegelian roots of adjoint logic, and of our adjoint representation of time above, it's perhaps interesting to read what [[R. G. Collingwood]], much influenced by Hegel, has to say about time. In _Some Perplexities about Time: With an Attempted Solution_, Proceedings of the Aristotelian Society, New Series, Vol. 26 (1925 - 1926), pp. 135-150, he is trying to find another way to think of time other than >"spatially," as something existing _totum simul_ or as >a ceaseless flow in which the present, perpetually changing, sloughs off its states into the abyss of the past and acquires new states from the abyss of the future. His solution is as follows: >The ideal is that which is thought, but not thought as real or existing; and in this class fall the future, which is possible but not necessary, and the past, which is necessary but not possible. The real is the present, conceived not as a mathematical point between the present and the past, but as the union of present and past in a duration or permanence that is at the same time change: the possible parting with its unnecessariness and the necessary parting with its impossibility in an actuality which is at once possible _and_ necessary, not (like the abstract mathematical present) neither. Within this present there are, as really as you like, two elements (necessity and possibility), each of which taken singly or in isolation characterizes a being which is not real but ideal---the past and future respectively. Thus the past _as past_ and the future _as future_ do not exist at all, but are purely ideal; the past as living in the present and the future as germinating in the present are wholly real and indeed are just the present itself. It is because of the presence of these two elements _in_ the present (not merely psychologically or illusorily, as in the doctrine of the specious present) that the present is a concrete and changing reality and not an empty mathematical point. >That which is ideal is for a mind, and has no other being except to be an object of mind. But the ideal and the real are not mutually exclusive. A thing may be ideal and also real. An example of this would be a duty, which is absolutely real in spite of the fact that it only exists for mind. But some things are merely ideal, and under this head fall the past and the future; unlike a duty, which exists only for thought but, for thought, really does exist, they have being for thought, but, even for thought, have no existence. Hence, if there were no mind, there would at any given moment be no past and no future; there would only be a present in which the past survived transformed and in which the future was present in germ. The past _as past_ and the future _as future_, in contradistinction from their fusion in the present, have being for mind and only so. We do call the past, _as such_, into being by recollecting and by thinking historically; but we do this by disentangling it out of the present in which it actually exists, transformed, and re-transforming it in thought into what it was. Hence time, as succession of past, present and future, really has its being _totum simul_ for the thought of a spectator, and this justifies its "spatialized" presentation as a line of which we can see the whole at once; it also justifies, so far as they go, subjectivist views of time like that of Kant. But time, as the ceaseless change of the present, is "transcendentally real," and the logical presupposition of any thought whatever; and this justifies the "pure flux" view of time and its treatment in philosophies like that of Bergson and Mr. Alexander. >But this conception, though the only one I can discover which gives any hope of escape from my perplexities about time, is only open to a logic which conceives the real as a synthesis of opposites and a metaphysic which has abandoned the hopeless attempt to think of all objects of thought as existent. If we must regard the real as a collocation of elements each of which is real by itself and in its own right, we must give up the solution which I have attempted to sketch and find another, if we can. Plenty of resonances there, such as adjunctions as 'synthesis of opposites' and maybe a whiff of the kinematics/dynamics distinction of [[higher category theory and physics]]. By the way, Bergson was supposedly instrumental in Einstein not receiving a second Nobel prize for relativity theory, the spatialization of time being evidently wrong.

    In view of the Lawverian and so Hegelian roots of adjoint logic, and of our adjoint representation of time above, it’s perhaps interesting to read what R. G. Collingwood, much influenced by Hegel, has to say about time.

    In Some Perplexities about Time: With an Attempted Solution, Proceedings of the Aristotelian Society, New Series, Vol. 26 (1925 - 1926), pp. 135-150, he is trying to find another way to think of time other than

    “spatially,” as something existing totum simul

    or as

    a ceaseless flow in which the present, perpetually changing, sloughs off its states into the abyss of the past and acquires new states from the abyss of the future.

    His solution is as follows:

    The ideal is that which is thought, but not thought as real or existing; and in this class fall the future, which is possible but not necessary, and the past, which is necessary but not possible. The real is the present, conceived not as a mathematical point between the present and the past, but as the union of present and past in a duration or permanence that is at the same time change: the possible parting with its unnecessariness and the necessary parting with its impossibility in an actuality which is at once possible and necessary, not (like the abstract mathematical present) neither. Within this present there are, as really as you like, two elements (necessity and possibility), each of which taken singly or in isolation characterizes a being which is not real but ideal—the past and future respectively. Thus the past as past and the future as future do not exist at all, but are purely ideal; the past as living in the present and the future as germinating in the present are wholly real and indeed are just the present itself. It is because of the presence of these two elements in the present (not merely psychologically or illusorily, as in the doctrine of the specious present) that the present is a concrete and changing reality and not an empty mathematical point.

    That which is ideal is for a mind, and has no other being except to be an object of mind. But the ideal and the real are not mutually exclusive. A thing may be ideal and also real. An example of this would be a duty, which is absolutely real in spite of the fact that it only exists for mind. But some things are merely ideal, and under this head fall the past and the future; unlike a duty, which exists only for thought but, for thought, really does exist, they have being for thought, but, even for thought, have no existence. Hence, if there were no mind, there would at any given moment be no past and no future; there would only be a present in which the past survived transformed and in which the future was present in germ. The past as past and the future as future, in contradistinction from their fusion in the present, have being for mind and only so. We do call the past, as such, into being by recollecting and by thinking historically; but we do this by disentangling it out of the present in which it actually exists, transformed, and re-transforming it in thought into what it was. Hence time, as succession of past, present and future, really has its being totum simul for the thought of a spectator, and this justifies its “spatialized” presentation as a line of which we can see the whole at once; it also justifies, so far as they go, subjectivist views of time like that of Kant. But time, as the ceaseless change of the present, is “transcendentally real,” and the logical presupposition of any thought whatever; and this justifies the “pure flux” view of time and its treatment in philosophies like that of Bergson and Mr. Alexander.

    But this conception, though the only one I can discover which gives any hope of escape from my perplexities about time, is only open to a logic which conceives the real as a synthesis of opposites and a metaphysic which has abandoned the hopeless attempt to think of all objects of thought as existent. If we must regard the real as a collocation of elements each of which is real by itself and in its own right, we must give up the solution which I have attempted to sketch and find another, if we can.

    Plenty of resonances there, such as adjunctions as ’synthesis of opposites’ and maybe a whiff of the kinematics/dynamics distinction of higher category theory and physics.

    By the way, Bergson was supposedly instrumental in Einstein not receiving a second Nobel prize for relativity theory, the spatialization of time being evidently wrong.

40. • CommentRowNumber40.
    • CommentAuthorKeithEPeterson
    • CommentTimeJan 7th 2017
    • PermaLink
    Author: KeithEPeterson
    Format: MarkdownItexSo Bergson views time as a topological point (maybe infinitesimal thickened)?

    So Bergson views time as a topological point (maybe infinitesimal thickened)?

41. • CommentRowNumber41.
    • CommentAuthorfastlane69
    • CommentTimeJan 9th 2017
    • PermaLink
    Author: fastlane69
    Format: TextMore modern thoughts on time. Like you, David, I get a strong whiff of CATS lurking in the shadows of what and how they speak. [Oxford Handbook on the Philosophy of Time](https://global.oup.com/academic/product/the-oxford-handbook-of-philosophy-of-time-9780199298204?cc=us&lang=en&) [(Oxford readings) The Philosophy of Time](https://global.oup.com/academic/product/the-philosophy-of-time-9780198239994?cc=us&lang=en&)

    More modern thoughts on time.
    Like you, David, I get a strong whiff of CATS lurking in the shadows of what and how they speak.
    
    [Oxford Handbook on the Philosophy of Time](https://global.oup.com/academic/product/the-oxford-handbook-of-philosophy-of-time-9780199298204?cc=us&lang=en&)
    [(Oxford readings) The Philosophy of Time](https://global.oup.com/academic/product/the-philosophy-of-time-9780198239994?cc=us&lang=en&)
42. • CommentRowNumber42.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 2nd 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI began a section on 'computation tree logic' at [[temporal logic]]. I'll add some more detail later. It seems a good candidate for adjoint logic treatment.

    I began a section on ’computation tree logic’ at temporal logic. I’ll add some more detail later. It seems a good candidate for adjoint logic treatment.

43. • CommentRowNumber43.
    • CommentAuthorspitters
    • CommentTimeNov 2nd 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexThere is a curry-howard correspondence between LTL and reactive programming. This is similar to the temporal semantics in the topos of trees (presheaves over omega). http://www.itu.dk/~mogel/papers/lics2011.pdf I can try to add more references later.

    There is a curry-howard correspondence between LTL and reactive programming. This is similar to the temporal semantics in the topos of trees (presheaves over omega). http://www.itu.dk/~mogel/papers/lics2011.pdf

    I can try to add more references later.

44. • CommentRowNumber44.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexInteresting! So we're in this neck of the woods [described](https://cstheory.stackexchange.com/a/14290) by Neel Krishnaswami: >Nick Benton and I have argued for programming explicitly with streams in our paper Ultrametric Semantics of Reactive Programs. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper LTL types FRP, an observation that Wolfgang Jeltsch also made in his paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. >The difference between the view Nick and I take, and the one that Alan and Wolfgang take is best understood (IMO) by comparing the construction given in Birkedal et al.'s First steps in synthetic guarded domain theory: step-indexing in the topos of trees with Alan's paper. The topos of trees (presheaves over the natural numbers ordered by size) is very similar to category of ultrametric spaces Nick and I used, but much easier to compare with Alan's category (presheaves over a discrete category of time), since these are both presheaf categories. >If you're interested in futures specifically for concurrency, then it might be a better idea to look at CTL rather than LTL, though. AFAIK, that's presently unexplored territory! Has anyone done a Curry-Howard correspondence for CTL or even CTL$^{\ast}$?

    Interesting! So we’re in this neck of the woods described by Neel Krishnaswami:

    Nick Benton and I have argued for programming explicitly with streams in our paper Ultrametric Semantics of Reactive Programs. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper LTL types FRP, an observation that Wolfgang Jeltsch also made in his paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming.

    The difference between the view Nick and I take, and the one that Alan and Wolfgang take is best understood (IMO) by comparing the construction given in Birkedal et al.’s First steps in synthetic guarded domain theory: step-indexing in the topos of trees with Alan’s paper. The topos of trees (presheaves over the natural numbers ordered by size) is very similar to category of ultrametric spaces Nick and I used, but much easier to compare with Alan’s category (presheaves over a discrete category of time), since these are both presheaf categories.

    If you’re interested in futures specifically for concurrency, then it might be a better idea to look at CTL rather than LTL, though. AFAIK, that’s presently unexplored territory!

    Has anyone done a Curry-Howard correspondence for CTL or even CTL$^{\ast}$?

45. • CommentRowNumber45.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 3rd 2017
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWhat we were doing above (in section 5 of [[temporal logic]]) seems to point in a very similar direction to * Alan Jeffrey, [LTL types FRP](http://ect.bell-labs.com/who/ajeffrey/papers/plpv12.pdf) Reactive types there are our $Time_0$-dependent types. Perhaps we were doing better. Jeffrey writes: >The implementation described here is based on interval types, rather than reactive types. This might be a better match to an interval temporal logic rather than LTL, which would admit the “chop” modality That 'chopping' of an interval is what Mike is addressing in #18.

    What we were doing above (in section 5 of temporal logic) seems to point in a very similar direction to

    • Alan Jeffrey, LTL types FRP

    Reactive types there are our $Time_0$-dependent types. Perhaps we were doing better. Jeffrey writes:

    The implementation described here is based on interval types, rather than reactive types. This might be a better match to an interval temporal logic rather than LTL, which would admit the “chop” modality

    That ’chopping’ of an interval is what Mike is addressing in #18.

46. • CommentRowNumber46.
    • CommentAuthorspitters
    • CommentTimeNov 3rd 2017
    • PermaLink
    Author: spitters
    Format: MarkdownItexHere's a recent paper. Temporal Type Theory: A topos-theoretic approach to systems and behavior Patrick Schultz, David I. Spivak https://arxiv.org/abs/1710.10258 It is an application of Sh(Int) to hybrid systems. Int is the interval domain. They relate it to discrete conduce fibrations, Martin-Lof has also been lecturing on such interval type theories. I am not sure whether there is a public record of the latter. In any case, I suspect Jeffrey's work to be related to such discrete conduce fibrations.

    Here’s a recent paper.

    Temporal Type Theory: A topos-theoretic approach to systems and behavior Patrick Schultz, David I. Spivak https://arxiv.org/abs/1710.10258

    It is an application of Sh(Int) to hybrid systems. Int is the interval domain.

    They relate it to discrete conduce fibrations, Martin-Lof has also been lecturing on such interval type theories. I am not sure whether there is a public record of the latter. In any case, I suspect Jeffrey’s work to be related to such discrete conduce fibrations.

47. • CommentRowNumber47.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWith the development from unary (the adjoint logic of #1) to simple to the hotly anticipated dependent type 2-theories, what's a good way to organise this material for nLab purposes? Is there any future for the term 'adjoint logic' (something of a pleonasm if we follow Lawvere, "we may more precisely identify logic with this scheme of interlocking adjoints")? So the 2-category of modes for a temporal logic we developed above in this discussion can be formulated as a superposed pair of walking adjunctions, generating cross-pair monads (#8). If one were to look to depict a type 2-theory diagrammatically, I guess you'd have a sheet for each mode, on which the types associated with the mode can be written. In the unary case, we could have the adjoint functors transferring types between sheets. One of these days, we'll find that Peirce was ahead of his time again, with his tinctured gamma graphs: "the tinctures enable Peirce to distinguish between different modes of modalities" ([Peirce’s Search for a Graphical Modal Logic](http://homepage.univie.ac.at/esther.ramharter/peirce-modal.pdf), p. 159)

    With the development from unary (the adjoint logic of #1) to simple to the hotly anticipated dependent type 2-theories, what’s a good way to organise this material for nLab purposes? Is there any future for the term ’adjoint logic’ (something of a pleonasm if we follow Lawvere, “we may more precisely identify logic with this scheme of interlocking adjoints”)?

    So the 2-category of modes for a temporal logic we developed above in this discussion can be formulated as a superposed pair of walking adjunctions, generating cross-pair monads (#8).

    If one were to look to depict a type 2-theory diagrammatically, I guess you’d have a sheet for each mode, on which the types associated with the mode can be written. In the unary case, we could have the adjoint functors transferring types between sheets.

    One of these days, we’ll find that Peirce was ahead of his time again, with his tinctured gamma graphs: “the tinctures enable Peirce to distinguish between different modes of modalities” (Peirce’s Search for a Graphical Modal Logic, p. 159)

48. • CommentRowNumber48.
    • CommentAuthorMike Shulman
    • CommentTimeJun 11th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYeah, I don't really like the term "adjoint logic" either.

    Yeah, I don’t really like the term “adjoint logic” either.

49. • CommentRowNumber49.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 11th 2018
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe my Peirce comment in #47, slides like 191 of Dan Licata's HiM [talk](http://dlicata.web.wesleyan.edu/pubs/lsr17multi/him-tutorial.pdf) are suggestive.

    Re my Peirce comment in #47, slides like 191 of Dan Licata’s HiM talk are suggestive.