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

Question

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?

Answer 1

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...

Answer 2

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.