<p>Let me first say that I did not look carefully at the second part of your question, nor your sketch of why the clock quantifier should commute with propositional existential quantification.</p>
<p>I will restrict my comments to the question about clock quantification and the topos-logic's existential-quantification of both the Bizjak-Møgelberg and Sterling-Harper topoi. (Note that the latter is the open subtopos of the former under the proposition <span class="math-container">$\exists k : K. \top$</span>). My comments should not be understood as pertaining to a notion of 'propositional truncation' for the PER model of Sterling and Harper; in PERs, there is not really a canonical notion of truncation (there are several possibilities that are quite inadequate in different ways), so let me really restrict my comments to the topos.</p>
<p>In this case, I do <em>not</em> expect the clock quantifier to distribute over the existential quantifier for arbitrary families of presheaves <span class="math-container">$A$</span> and predicates <span class="math-container">$\phi$</span>. This would seem to need that <span class="math-container">$K$</span> is projective, but I do not see why that should be the case. In particular, unraveling the Kripke-Joyal semantics of <span class="math-container">$\forall k. \exists x. \phi k x$</span>, it might be that there is no single <span class="math-container">$x$</span> that works for all clocks.</p>
<p>In particular, if we consider either the Bizjak-Møgelberg or Sterling-Harper topos, the following proposition holds: <span class="math-container">$\forall k. \exists n. \rhd^n_k \bot$</span>. This corresponds to the fact that the Bizjak-Møgelberg topos <a href="https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf" rel="nofollow noreferrer">classifies indexed families of filters on <span class="math-container">$\omega$</span></a> --- where the component of the generic generic family of filters at a given index <span class="math-container">$k$</span> is the predicate <span class="math-container">$\{n\mid \rhd^n_k \bot\}$</span>. If the discussed commutation law held in general, it thus would imply <span class="math-container">$K\cong \bot$</span>. This example was suggested by Max New.</p>
<p>On the other hand, if <span class="math-container">$A$</span> and <span class="math-container">$\phi$</span> are both clock-irrelevant, in the sense that <span class="math-container">$Ak \cong Ak'$</span> and modulo this isomorphism we have <span class="math-container">$\phi k = \phi k'$</span> and moreover it holds that <span class="math-container">$\exists k : K.\top$</span>, then it does follow that the clock quantifier commutes with the existential quantification. Thus in the Sterling-Harper topos under these assumptions, it follows that the commutation law you ask for would hold in the special case of clock-irrelevant types and predicates. I do not believe it holds globally in the Bizjak-Møgelberg topos, but I haven't checked carefully.</p>
<p><strong>Remark.</strong> Note that the reason the clock quantifier commuted with coproducts is that <code>K</code> is connected in the &quot;multiplexed topos of trees&quot; models of Bizjak-Møgelberg and Sterling-Harper. This property is also used, covertly(?), by <a href="https://arxiv.org/abs/2102.01969" rel="nofollow noreferrer">Kristensen, Møgelberg and Vezzosi</a> to do induction for HITs underneath a clock quantifier...</p>

CC BY-SA 4.0
2022-07-18T11:31:02.230Z
Just to confirm: in these topos models the clock quantification does commute with Sigma types?
Max New
CC BY-SA 4.0
2022-07-18T11:49:49.610Z
In fact, in MLTT for any type $K$ and families $k:K \vdash Ak$ and $k:K, x:Ak \vdash Bkx$ the sigma type commutation law that you described holds.
Jonathan Sterling
CC BY-SA 4.0
2022-07-18T12:05:59.023Z
Oh I see, if you interpret the clock quantification as just a Pi type this is essentially a form of axiom of choice, and commuting with Sigma types is the usual “incorrect” rendering of AC.
Max New
CC BY-SA 4.0
2022-07-18T12:09:36.640Z
That's right! Btw, I think that if `A` and `\phi` are both clock irrelevant, then it might **in fact** be possible to commute the existential under certain circumstances. Let me compute a bit more, and I'll update my answer.
Jonathan Sterling
CC BY-SA 4.0
2022-07-18T12:19:15.290Z
Updated my answer accordingly.
Jonathan Sterling
CC BY-SA 4.0
2022-07-18T13:32:25.060Z
"Axiom of clockable choice"?
Max New
CC BY-SA 4.0
2022-07-20T22:38:31.660Z
If you want to add in the explicit counterexample $$\forall k. \exists n. (\triangleright^k)^n \bot$$ we discussed on zulip I'll go ahead an accept the answer
Max New
CC BY-SA 4.0
2022-07-21T06:48:26.667Z
@MaxNew added the example
Jonathan Sterling
CC BY-SA 4.0
2022-07-18T10:41:07.990Z
2022-07-21T06:53:33.300Z
2022-07-21T06:53:33.300Z
Jonathan Sterling
<p>This question sounds related to <a href="https://iris-project.org/pdfs/2021-pldi-transfinite-iris-final.pdf" rel="nofollow noreferrer">Transfinite Iris</a>, which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have &quot;later&quot; commute with existentials.</p>

CC BY-SA 4.0
2022-07-18T11:27:44.290Z
I think the question is a bit different; it is not about whether the later modality commutes with existentials, but whether the clock quantifier commutes with existentials.
Jonathan Sterling
CC BY-SA 4.0
2022-07-18T12:12:34.790Z
I think they are related, but gasche misstated the motivation in Transfinite Iris. In transfinite Iris, they wanted existentials to commute with the *meaning*, which was defined as |= Phi = forall i. Phi i, i.e., the proposition is “true at every step index”. Their motivation is to make a model where |= exists x. Phi is equivalent to exists x |= Phi, which is my intuitive reading of the commutativity of existentials with clock quantification.
Max New
CC BY-SA 4.0
2022-07-18T11:24:52.723Z
2022-07-18T11:24:52.723Z
gasche
<p>In <a href="https://dl.acm.org/doi/10.1145/2500365.2500597" rel="nofollow noreferrer">Atkey &amp; McBride ICFP 2013</a>, they extend a simple type theory with guarded recursion indexed by clock variables <span class="math-container">$\triangleright^k$</span> and a clock quantification <span class="math-container">$\forall k. A$</span> that conveniently commutes with a great deal of connectives, most notably for this question</p>
<p><span class="math-container">$$\forall k. A + B \cong (\forall k. A) + (\forall k. B)$$</span></p>
<p>This has been extended to dependent type theory, for instance <a href="https://doi.org/10.1017/S0960129520000080" rel="nofollow noreferrer">Bizjak &amp; Møgelberg MSCS 2020</a> and <a href="https://doi.org/10.1145/3209108.3209153" rel="nofollow noreferrer">Sterling &amp; Harper LICS 2018</a>. Sterling &amp; Harper's type theory supports the extension of the above to sigma-types (I think Bizjak &amp; Møgelberg's does as well but I couldn't find it explicitly in the paper):</p>
<p><span class="math-container">$$\forall k. \sum_{x:A} B \cong \sum_{x:\forall k. A} (\forall k. B[xk/x])$$</span></p>
<p>My first question is if the models in BM/HS accommodate a proof-irrelevant universe of propositions where</p>
<p><span class="math-container">$$\forall k. \exists{(x:A)} \phi \cong \exists {(x:\forall k. A)} (\forall k. \phi[xk/x])$$</span></p>
<p>The reason I ask is that my intuitive model of these guarded dependent type theories is that within a context with a single clock variable <span class="math-container">$k$</span>, a type <span class="math-container">$A$</span> can be interpreted in the topos of trees, i.e., a presheaf on <span class="math-container">$\omega$</span>. Next, the clock quantification <span class="math-container">$\forall k. A$</span> can be interpreted as the set of <span class="math-container">$\omega$</span>-chains, i.e., for each <span class="math-container">$i \in \omega$</span>, an element <span class="math-container">$x_i : A_i$</span> that commutes with all projections <span class="math-container">$p_i(x_{i+1}) = x_i$</span>. Finally a proposition <span class="math-container">$\phi$</span> would be a presheaf where every set <span class="math-container">$\phi_i$</span> is a subset of <span class="math-container">$1$</span>.</p>
<p>It makes sense to me that in this model the <span class="math-container">$\Sigma$</span>-type/coproduct would commute with taking the <span class="math-container">$\omega$</span>-chain as the chain has to commute with projections, so you cannot &quot;change from inl to inr&quot;, however, it seems false that an existential quantifier would! The example I have in mind is the weak bisimulation relation <span class="math-container">$\approx$</span> (valued in propositions) on the lift monad <span class="math-container">$L^k A \cong A + \triangleright^k (L^k A)$</span> from <a href="https://doi.org/10.1145/2933575.2934516" rel="nofollow noreferrer">Møgelberg &amp; Paviotti LICS '16</a>. The proposition would be</p>
<p><span class="math-container">$$\exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$</span></p>
<p>where <span class="math-container">$v:A$</span> is anything and <span class="math-container">$\Omega$</span> is the &quot;diverging&quot; element. In my intuitive model,</p>
<p><span class="math-container">$$\forall k. \exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$</span></p>
<p>is true because for each step-index <span class="math-container">$i\in\omega$</span>, We can take <span class="math-container">$x = x_i = \delta^{i+1}(\eta v)$</span> which is similar to <span class="math-container">$v$</span> by definition and similar to <span class="math-container">$\Omega$</span> by &quot;time out&quot;. However the trick is that we are picking a different <span class="math-container">$x$</span> depending on the step index, so the switched version:</p>
<p><span class="math-container">$$\exists (x: \forall k. L^k A) \forall k. (\eta v) \approx x k \wedge x k \approx \Omega$$</span></p>
<p>fails to allow this proof because we cannot assemble the <span class="math-container">$x_i$</span> into an <span class="math-container">$\omega$</span>-chain. I think this proposition is false under that interpretation because anything that is similar to <span class="math-container">$\eta v$</span> must terminate at finite index, and so any <span class="math-container">$\omega$</span>-chain of <span class="math-container">$x$</span>s that satisfies <span class="math-container">$(\eta v) \approx x k$</span> will eventually be terminating and so eventually <span class="math-container">$x k \approx \Omega$</span> will be false.</p>
<p>So my second question is, if the clock quantifiers <em>do</em> commute with existential quantification then where did I go wrong in my intuitive reasoning above? And if they don't commute is there a variation on these models where they do?</p>

CC BY-SA 4.0
2022-07-18T10:01:46.183Z
I don't know, but I've emailed @JonathanSterling about it...
Neel Krishnaswami
CC BY-SA 4.0
2022-07-18T10:18:08.883Z
Quick question : in your definition of weak bisimulation, do you not mean to existentially quantify over `A` rather than `LA`?
Jonathan Sterling
<type-theory><ct.category-theory><domain-theory><step-indexing><guarded-domain-theory>
Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories
Max New
# Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

(Asked by: username_0 on 2022-07-17)

In [Atkey & McBride ICFP 2013](https://dl.acm.org/doi/10.1145/2500365.2500597), they extend a simple type theory with guarded recursion indexed by clock variables $\triangleright^k$ and a clock quantification $\forall k. A$ that conveniently commutes with a great deal of connectives, most notably for this question

$$\forall k. A + B \cong (\forall k. A) + (\forall k. B)$$

This has been extended to dependent type theory, for instance [Bizjak & Møgelberg MSCS 2020](https://doi.org/10.1017/S0960129520000080) and [Sterling & Harper LICS 2018](https://doi.org/10.1145/3209108.3209153). Sterling & Harper's type theory supports the extension of the above to sigma-types (I think Bizjak & Møgelberg's does as well but I couldn't find it explicitly in the paper):

$$\forall k. \sum\_{x:A} B \cong \sum\_{x:\forall k. A} (\forall k. B[xk/x])$$

My first question is if the models in BM/HS accommodate a proof-irrelevant universe of propositions where

$$\forall k. \exists{(x:A)} \phi \cong \exists {(x:\forall k. A)} (\forall k. \phi[xk/x])$$

The reason I ask is that my intuitive model of these guarded dependent type theories is that within a context with a single clock variable $k$, a type $A$ can be interpreted in the topos of trees, i.e., a presheaf on $\omega$. Next, the clock quantification $\forall k. A$ can be interpreted as the set of $\omega$-chains, i.e., for each $i \in \omega$, an element $x\_i : A\_i$ that commutes with all projections $p\_i(x\_{i+1}) = x\_i$. Finally a proposition $\phi$ would be a presheaf where every set $\phi\_i$ is a subset of $1$.

It makes sense to me that in this model the $\Sigma$-type/coproduct would commute with taking the $\omega$-chain as the chain has to commute with projections, so you cannot "change from inl to inr", however, it seems false that an existential quantifier would! The example I have in mind is the weak bisimulation relation $\approx$ (valued in propositions) on the lift monad $L^k A \cong A + \triangleright^k (L^k A)$ from [Møgelberg & Paviotti LICS '16](https://doi.org/10.1145/2933575.2934516). The proposition would be

$$\exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$

where $v:A$ is anything and $\Omega$ is the "diverging" element. In my intuitive model,

$$\forall k. \exists (x: L^k A) (\eta v) \approx x \wedge x \approx \Omega$$

is true because for each step-index $i\in\omega$, We can take $x = x\_i = \delta^{i+1}(\eta v)$ which is similar to $v$ by definition and similar to $\Omega$ by "time out". However the trick is that we are picking a different $x$ depending on the step index, so the switched version:

$$\exists (x: \forall k. L^k A) \forall k. (\eta v) \approx x k \wedge x k \approx \Omega$$

fails to allow this proof because we cannot assemble the $x\_i$ into an $\omega$-chain. I think this proposition is false under that interpretation because anything that is similar to $\eta v$ must terminate at finite index, and so any $\omega$-chain of $x$s that satisfies $(\eta v) \approx x k$ will eventually be terminating and so eventually $x k \approx \Omega$ will be false.

So my second question is, if the clock quantifiers *do* commute with existential quantification then where did I go wrong in my intuitive reasoning above? And if they don't commute is there a variation on these models where they do?

**Tags:** type-theory, ct.category-theory, domain-theory, step-indexing, guarded-domain-theory

> **Comments:**
> **username_1**: I don't know, but I've emailed @JonathanSterling about it...  
> **username_2**: Quick question : in your definition of weak bisimulation, do you not mean to existentially quantify over `A` rather than `LA`?  

---

## 2 answers

### Answer by username_2 on 2022-07-18. Score: 4 | Accepted answer

Let me first say that I did not look carefully at the second part of your question, nor your sketch of why the clock quantifier should commute with propositional existential quantification.

I will restrict my comments to the question about clock quantification and the topos-logic's existential-quantification of both the Bizjak-Møgelberg and Sterling-Harper topoi. (Note that the latter is the open subtopos of the former under the proposition $\exists k : K. \top$). My comments should not be understood as pertaining to a notion of 'propositional truncation' for the PER model of Sterling and Harper; in PERs, there is not really a canonical notion of truncation (there are several possibilities that are quite inadequate in different ways), so let me really restrict my comments to the topos.

In this case, I do *not* expect the clock quantifier to distribute over the existential quantifier for arbitrary families of presheaves $A$ and predicates $\phi$. This would seem to need that $K$ is projective, but I do not see why that should be the case. In particular, unraveling the Kripke-Joyal semantics of $\forall k. \exists x. \phi k x$, it might be that there is no single $x$ that works for all clocks.

In particular, if we consider either the Bizjak-Møgelberg or Sterling-Harper topos, the following proposition holds: $\forall k. \exists n. \rhd^n\_k \bot$. This corresponds to the fact that the Bizjak-Møgelberg topos [classifies indexed families of filters on $\omega$](https://www.jonmsterling.com/papers/palombi-sterling:2022.pdf) --- where the component of the generic generic family of filters at a given index $k$ is the predicate $\{n\mid \rhd^n\_k \bot\}$. If the discussed commutation law held in general, it thus would imply $K\cong \bot$. This example was suggested by username_0.

On the other hand, if $A$ and $\phi$ are both clock-irrelevant, in the sense that $Ak \cong Ak'$ and modulo this isomorphism we have $\phi k = \phi k'$ and moreover it holds that $\exists k : K.\top$, then it does follow that the clock quantifier commutes with the existential quantification. Thus in the Sterling-Harper topos under these assumptions, it follows that the commutation law you ask for would hold in the special case of clock-irrelevant types and predicates. I do not believe it holds globally in the Bizjak-Møgelberg topos, but I haven't checked carefully.

**Remark.** Note that the reason the clock quantifier commuted with coproducts is that `K` is connected in the "multiplexed topos of trees" models of Bizjak-Møgelberg and Sterling-Harper. This property is also used, covertly(?), by [Kristensen, Møgelberg and Vezzosi](https://arxiv.org/abs/2102.01969) to do induction for HITs underneath a clock quantifier...

> **Comments:**
> **username_0**: Just to confirm: in these topos models the clock quantification does commute with Sigma types?  
> **username_2**: In fact, in MLTT for any type $K$ and families $k:K \vdash Ak$ and $k:K, x:Ak \vdash Bkx$ the sigma type commutation law that you described holds.  
> **username_0**: Oh I see, if you interpret the clock quantification as just a Pi type this is essentially a form of axiom of choice, and commuting with Sigma types is the usual “incorrect” rendering of AC.  
> **username_2**: That's right! Btw, I think that if `A` and `\phi` are both clock irrelevant, then it might **in fact** be possible to commute the existential under certain circumstances. Let me compute a bit more, and I'll update my answer.  
> **username_2**: Updated my answer accordingly.  
> **username_0**: "Axiom of clockable choice"?  
> **username_0**: If you want to add in the explicit counterexample $$\forall k. \exists n. (\triangleright^k)^n \bot$$ we discussed on zulip I'll go ahead an accept the answer  
> **username_2**: @MaxNew added the example  

---

### Answer by username_3 on 2022-07-18. Score: 2

This question sounds related to [Transfinite Iris](https://iris-project.org/pdfs/2021-pldi-transfinite-iris-final.pdf), which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have "later" commute with existentials.

> **Comments:**
> **username_2**: I think the question is a bit different; it is not about whether the later modality commutes with existentials, but whether the clock quantifier commutes with existentials.  
> **username_0**: I think they are related, but username_3 misstated the motivation in Transfinite Iris. In transfinite Iris, they wanted existentials to commute with the *meaning*, which was defined as |= Phi = forall i. Phi i, i.e., the proposition is “true at every step index”. Their motivation is to make a model where |= exists x. Phi is equivalent to exists x |= Phi, which is my intuitive reading of the commutativity of existentials with clock quantification.  

---

