# Commutativity of Clock Quantification and Disjunction/Existential Quantification in Guarded Type Theories

In Atkey & McBride ICFP 2013, 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 and Sterling & Harper LICS 2018. 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. 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?

• I don't know, but I've emailed @JonathanSterling about it... Jul 18 at 10:01
• Quick question : in your definition of weak bisimulation, do you not mean to existentially quantify over A rather than LA? Jul 18 at 10:18

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$$ --- 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 Max New.

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 to do induction for HITs underneath a clock quantifier...

• Just to confirm: in these topos models the clock quantification does commute with Sigma types? Jul 18 at 11:31
• 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. Jul 18 at 11:49
• 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. Jul 18 at 12:05
• 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. Jul 18 at 12:09
• "Axiom of clockable choice"? Jul 18 at 13:32

This question sounds related to Transfinite Iris, which proposes to change the Iris model from Nat-indexed propositions to Ordinal-indexed propositions to have "later" commute with existentials.

• 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. Jul 18 at 11:27
• 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. Jul 18 at 12:12