Word count: 866

Wonderfully vague title, yes? As some of you might know, I’m now maintaining the implementation of Cubical Agda. Undoubtedly, if you know, it’s because I’ve been talking your ear off about it: I’m sorry. The “little kid with new toy” energy will continue until morale improves.

Anyway, part of what I’ve been doing is refactoring the implementation to make it easier for me, and for others, to understand it. I already pulled out and documented the implementation of every single Kan operation from the massive module that all the primitives were stuck in the same module (PR 6034), but also fixed a tiny soundness issue (PR 6032) and a bug in the conversion checker (PR 6013).

But I’m not here today to brag (my changes are but a single drop in the ocean that is Agda), or to complain — I think Andrea Vezzosi did an absolutely stellar job implementing Cubical Agda, as can be seen by how much research is going on based on it, and today I’d like to commemorate that by sharing my favourite bit of trivia: How boundary constraints for higher pattern matching work.

## Patterns & copatterns

If you’re familiar with functional programming, with Haskell if not Agda
itself, you might recognise the following function as an instance of
*definition by pattern-matching*. Admittedly, it’s quite a trivial
instance, but it’s one nonetheless.

```
: ∀ {l} {A : Type l} (x : A) → x ≡ x
refl = x refl x i
```

But, dear reader, that’s where you’re wrong: That’s right, I’ve tricked
you. This isn’t a definition by pattern matching at all! It’s a
definition by *co*pattern matching. While the variable `x`

*is* a
variable, the `i`

is something much sneakier: an ** IApply copattern**.
By the way,

`IApply`

is the internal name we use for this, but another
perfectly valid name would be a *path copattern*.

Since `refl`

has a `Path`

-headed type after introducing `x`

, we
internally treat the pattern `i`

as being not a variable binder, but
rather specifying how `refl x`

behaves when applied to interval
variables — and, since being applied to interval variables is an
*observation* you can make of paths, we call this a copattern, by
analogy with how record copatterns specify what the destructors do to
your definition.

So, internally, we have something like

`Var x) (IApply .x .x i) = ... refl (`

where the second co/pattern in the left-hand-side specifies not only the
name of the bound interval variable, but also what endpoints it has.
But, of course, interval copatterns aren’t *that* simple: we really must
have that, when applied to `i0`

(resp. `i1`

), the right-hand-side must
equal `x`

(resp. `x`

; bad example because both endpoints are the same,
here). So, how is this checked?

## IApplyConfluence

If you’ve heard me speak of `IApplyConfluence`

before, this is that. The
name might be a bit weird: at first it looks like a Java interface name,
something you can apply confluence to, but really it stands for
“interval application confluence.” Recall that, in cubical type theory,
we have the following judgemental computation for the endpoints of a
path, even when the path itself is neutral: If `p : Path A x y`

, then `p i0 = x`

(resp. `p i1 = y`

).

In Agda, path lambdas are really just lambdas, but path *application* is
different from function application: That’s what `IApply`

means, it’s an
*elimination* just like `Apply`

(ordinary function application) or
`Proj`

(record projections). So, in Agda, we reduce the boundary
constraints in paths defined by copattern matching to something called
“`IApply`

confluence”: the definition reduces in a way that is
*confluent* with `IApply`

reductions, in the sense of a nondeterministic
rewrite system (but note that Agda still has deterministic reduction:
it’s just a name.)

As a different example, let’s look at the following definition, now by matching on a higher-inductive type:

```
data Interval : Type where
: Interval
left right : left ≡ right
seg
: ∀ {l} {A : Type l} (x y : A) → Interval → A
xtoy = x
xtoy x y left = y
xtoy x y right (seg i) = {! !} xtoy x y
```

How does Agda know what the interaction point’s endpoints should be?
`IApply`

confluence to the rescue! You guessed it: since the `i`

variable appears at a `Path`

-headed type, it’s really an `IApply`

copattern. The precise endpoints don’t matter here, but what does *is*
that `seg i0`

and `seg i1`

*will* reduce to them. So, what we must check
is that, regardless of if you first reduce `seg i0`

to an endpoint
*then* apply `xtoy x y`

, it’s the same as first reducing `xtoy x y (seg i)`

, then substituting `i0`

for `i`

.

And how can we do that generically? This is, in my opinion, the most
beautiful idea in the Agda codebase: We can just ask that, under the
substitutions `i → i0`

and `i → i1`

, the left-hand-side is equal to the
right-hand-side. That’s right: Agda will compare

`(seg i) = {! !} i ∨ ~ i ⊢ xtoy x y `

which is why, in the currently released version of Agda, the most
reliable place to get boundaries is from the unsolved unification
constraints. If there are more `IApply`

copatterns in the clause, the
interval formula on the left of the `⊢`

(we call that a “cofibration”)
will grow to include those variables, too. In general, it’ll be the
disjunction of the boundaries of every variable bound by an `IApply`

copattern in the clause.

Agda’s reduction rules guarantee that `xtoy x y (seg i0)`

will reduce
first to `xtoy x y left`

(by `IApply`

), then to `x`

(by computation);
Symetrically for `seg i1`

eventually reducing to `y`

. But the
right-hand-side will, in this case, do no such thing: That’s how we end
with the constraints (handwaving)

```
= ?0 (i = i0)
x = ?0 (i = i1) y
```

That’s all for today, folks! I want to write a blog post about
*quotients* soon, their relationship to the univalent completion of a
precategory, and their generalization to delooping of internal
$\infty$-groupoid objects, so stay tuned for that if you care.