Is the de Morgan interval Kan?

Question

I often read that the interval in cubical type theory does not have the structure of a Kan cubical set (i.e. is not fibrant), which justifies calling it a "pre-type" or "exo-type", aside from the "type" types we want to consider in the type theory, which support Kan operations. An example of this claim is in the initial paper on Cubical Agda, where the interval is given its own separate universe level.

While the interval in cartesian cubical type theory is clearly not Kan (because it lacks an inverse for the path from 0 to 1), I could not find a proof of this claim for the de Morgan interval (on which Cubical Agda is based) anywhere. So I tried to come up with a counter-example, but I think I may have proved that it is Kan instead.

Background

The de Morgan cube category 🧊 as presented in CCHM is the opposite of the Kleisli category for the free de Morgan algebra monad. This means that

• its objects are finite sets of names $\{i, j, ...\}$ (think of them as contexts $i : 𝕀, j : 𝕀, \dots$)
• its morphisms $I \to J$ are functions $J \to \text{dM}(I)$ assigning to each variable in $J$ a formal combination of elements of $I$ by de Morgan operations (think of this as substitution of contexts, or a drawing of the $I$-cube inside the $J$-cube)

The category of cubical sets is defined as the presheaf category on 🧊, and the basic $n$-cube $\square^n$ is the image $よ(n)$ under the Yoneda embedding of a set of $n$ variables. In particular, the interval $\square^1$ is the presheaf that maps $I$ to $\text{dM}(I)$.

A cubical set $X$ is Kan if, for each $n$-horn $\sqcup^{n,i,\epsilon} \to \square^n$ and boundary $\sqcup^{n,i,\epsilon} \to X$, there is a lifting $\square^n \to X$ making the obvious triangle commute.

Claim: $\square^1$ is Kan

Let's see what this means. The condition for $n = 1$ is boring (a point can always be lifted to a constant path), so let's start with $\sqcup^{2,1,0} \to \square^2$: the literal embedding of the shape $\sqcup$ inside the shape $\square$. (I claim that it doesn't matter which specific 2-horn $\sqcup^{2,i,\epsilon}$ we choose, because de Morgan cubes have enough symmetries.)

Lemma 1. For all $X : \text{dM}(I + \{i\})$, we have $i \land X[i=1] \leq X$ and $\neg i \land X[i=0] \leq X$.
Proof. Let $X = \bigvee_k x_k$ be a disjunctive normal form; we show that $i \land x_k[i=1] \leq x_k$. If $x_k$ contains $\neg i$ as a literal, then this amounts to $0 \leq x_k$. Otherwise, every literal in $x_k$ is either $i$ or a literal in $x_k[i=1]$. The case for $i = 0$ is dual. $\blacksquare$

We are given a bottom side $B : \text{dM}(\{i\})$, a left side $L : \text{dM}(\{j\})$ and a right side $R : \text{dM}(\{j\})$ such that $B[i=0] = L[j=0]$ and $B[i=1] = R[j=0]$. I claim that $F = (\neg j \land B) \lor (\neg i \land L) \lor (i \land R) : \text{dM}(\{i, j\})$ is the required filler. Let's check: $F[i=0] = (\neg j \land B[i=0]) \lor L = (\neg j \land L[j=0]) \lor L = L$ by lemma 1, and similarly $F[i=1] = R$ and $F[j=0] = B$.

A dimension higher, for the 3-horn $\sqcup^{3,1,0} \to \square^3$ (an open box missing a top face), we are given $B : \text{dM}(\{i, j\})$, $W, E : \text{dM}(\{j, k\})$ and $S, N : \text{dM}(\{i, k\})$ with agreement conditions on edges. Then the box is filled by $F = (\neg k \land B) \lor (\neg i \land W) \lor (i \land E) \lor (\neg j \land S) \land (j \land N)$. We can check similarly that e.g. \begin{align*} F[k=0] &= B \lor (\neg i \land W[k=0]) \lor (i \land E[k=0]) \lor (\neg j \land S[k=0]) \lor (j \land N[k=0]) \\\\ &= B \lor (\neg i \land B[i=0]) \lor (i \land B[i=1]) \lor (\neg j \land B[j=0]) \lor (j \land B[j=1]) \\\\ &= B\text{ (by lemma 1)} \end{align*} It is quite clear that this trick works in any dimension, so that the de Morgan interval is Kan(?)

Note that fillers exist but are not unique: for example, both $j$ and $j \land (i \lor \neg i)$ fill the square with sides $j$, $0$ and $j$.

Here's an Agda snippet to play around with liftings of $\sqcup^{2,1,0} \to \square^1$:

-- The built-in I lives in its own "non-fibrant" universe, so Agda won't let
-- us express partial elements and subtypes.
-- Hence we define a "wrapper" HIT, but do not make use of its Kan structure!
data Interval : Type where
  i0' : Interval
  i1' : Interval
  inI : i0' ≡ i1'

B L R : I → I
B i = i ∨ ~ i    --
L j = i1         -- replace these with anything (as long as they agree on endpoints)
R j = ~ j        --

module 2D (i j : I) where
  ⊔ : I
  ⊔ = ~ j ∨ ~ i ∨ i
  horn : Partial ⊔ Interval
  horn (j = i0) = inI (B i)
  horn (i = i0) = inI (L j)
  horn (i = i1) = inI (R j)
  filler : Interval [ ⊔ ↦ horn ]
  filler = inS (inI ((~ j ∧ B i) ∨ (~ i ∧ L j) ∨ (i ∧ R j)))

What about the other cubes, then? The point $\square^0$ is clearly Kan. For the $n$-cube $\square^n$, the same argument seems to work componentwise: morphisms into $\square^n$ are $n$-tuples of elements of the appropriate free de Morgan algebra. A mapping $\sqcup^{2,1,0} \to \square^n$ consists of $B : \text{dM}(\{i\})^n$ and $L, R : \text{dM}(\{j\})^n$ agreeing on endpoints componentwise, and $F_k = (\neg j \land B_k) \lor (\neg i \land L_k) \lor (i \land R_k)$ fills the square; this generalises to higher-dimensional horns as above.

Questions

• Is this actually true? Did I make any obvious mistakes?
• Is this known?
• Are de Morgan cubical sets formalised somewhere that isn't NuPRL, so that I can try to formalise this?
• Is fibrancy preserved by colimits? Does that mean every de Morgan cubical set is Kan?
• Does this have any consequences? For example, can we move Cubical Agda's I into Type and implement Kan operations for it as shown above? Or do we still want to keep a separation between "types that are Kan by accident" and "types that are Kan because we want them to be"?

Answer 1

Short answer: The interval is not fibrant according to the CCHM definition of Kan fibration which is stronger than the one given in the question.

Long answer: Regarding the (non) fibrancy of the interval there are a few key points:

1. For Kan fibrations, as defined in Definition 13 of CCHM, the generating left maps aren't just horn inclusions of boxes, but the pushout product of any cofibration with an endpoint inclusion of the interval. Cofibrations are determined by the face lattice notated $\mathbb{F}$ in CCHM.

2. If we define Kan fibrations in terms of subobjects of cubes we need to add uniformity conditions stating that fillers are stable under reindexing under arbitrary maps between cubes $\sigma : \square_n \to \square_m$, again following the definition in CCHM. This includes e.g. automorphisms $\square_n \cong \square_n$, degeneracy maps, diagonals (even though they are not included in the face lattice), connections and involution.

3. The face lattice $\mathbb{F}$ is a quotient of $\mathbb{I}$ identifying $\varphi$ and $\psi$ when they evaluate to 1 on the same subobject. E.g. $0$ and $i \wedge \neg i$ never evaluate to $1$ so they are the same cofibration (the empty cofibration) even though they are different as elements of $\mathsf{dM}(i)$. $\mathbb{F}$ will always be trivially fibrant (i.e. $\mathbb{F} \to 1$ has the right lifting property against all cofibrations) for purely formal reasons, from the fact that it is the classifier for all cofibrations. In particular, this implies $\mathbb{F}$ is fibrant, and so we need to exploit that $\mathbb{I}$ is different from $\mathbb{F}$ to get a counterexample.

To get a specific counterexample, we first look at the trivial open box $u$ in direction $j$ with base $0$ and no sides. The chosen filler of $u$ can only possibly be $0$, $j$ or $j \wedge \neg j$. For illustration, we will just consider the case where the filler is $0$, with the other cases following from similar arguments.

We next consider another open box $v$ this time in $\mathbb{I}(i, j)$, again with base $0$, again in direction $j$, but now with one side equal to $j$ when $(i = 1)$. The filler is some $\psi(i, j)$ such that $\psi(i := 1) = j$. Note that $u = v(i := 0)$, and so we also have $\psi(i := 0) = 0$. Putting $\psi$ into disjunctive normal form, and checking through cases, the only way this can happen is when $\psi = i \wedge j$. Note that $\psi(i := i \wedge \neg i) = i \wedge \neg i \wedge j$. However, $v(i := i \wedge \neg i)$ is the image of $u$ under the degeneracy map $i \hookrightarrow \mathsf{dM}(i, j)$ (because the "shape" of the open box is determined by the cofibration, which is determined by equality in $\mathbb{F}$, making $v(i := i \wedge \neg i)$ an open box with no sides), and so again by uniformity $\psi(i := i \wedge \neg i)$ must be $0$. This gives a contradiction since $i \wedge \neg i \wedge j \neq 0$ in $\mathsf{dM}(i, j)$.