How do I prove two applications of the absurd pattern result in the same in Cubical Agda?

Question

Heavy category theory (agda-categories) related question.

I'm trying to define a natural transformation and prove its naturality square commutes. Essentially, the error I run into is that two "applications" of a function that takes in the empty type (so ex falso quodlibdet principle) fail to return the same type. Here's the relevant hole:

plugin1unit : NaturalTransformation idF (constantPolynomial ∘F plugIn1)
plugin1unit = record { 
    η = λ X → (λ x → x , λ _ → tt) ⇄ λ fromPos () ;
    commute = λ f@(mapDir ⇄ mapPos) -> {!   !} ;
   }
}

The type of the commute hole is:

((λ x → Arrow.mapPosition f x , (λ _ → tt)) ⇄
       (λ fromPos z → Arrow.mapDirection f fromPos ((λ ()) z)))
      Cubical.≡
      ((λ x → Arrow.mapPosition f x , (λ x₁ → tt)) ⇄
       (λ fromPos z → (λ ()) z))

I don't want to include all the supporting definitions; I'll only include, in the "appendix" (end of the question) the definitions of the Polynomial type and its Arrow and so as to not flood this post with information. The error I get is simple. If I refine that hole enough, here's what I get, step-by-step: 1.

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → {!   !} ;

goal type:

Arrow X
      (MkPolynomial
       (Σ (Polynomial.position Y₁) (λ x → Polynomial.direction Y₁ x → ⊤))
       (λ _ → ⊥))

2. (some auto-solving/only obvious thing to do omitted)

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ {!   !} ;

goal type:

(fromPos : Polynomial.position X) →
      ⊥ → Polynomial.direction X fromPos

3. this refines to a function of two arguments, of course, one of which is the empty type ⊥:

    commute = λ f@(mapDir ⇄ mapPos) -> λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ λ fromPos x → {!   !} ;

but the obvious solution, of empty pattern matching, doesn't work with the following error: (λ { fromPos () }) fromPos z != Arrow.mapDirection f fromPos ((λ ()) z)

If I define a function that is _much more general than the requested type (fromPos : Polynomial.position X) → ⊥ → Polynomial.direction X fromPos:

fromAnythingToAnythingElse : {A B : Set} -> A -> ⊥ -> B
fromAnythingToAnythingElse x ()

and try to put it in the hole at step two, I get another error about inability of instantiating metavariables.

Here's another version of what I believe to be the essential error:

How can "(λ ()) z" be different from ANYTHING? By definition it returns any type!

Answer 1

I have found two solutions to this problem, which I will present on a minimal example. I have tested them both on your original problem, but will leave the details of adapting these solutions as a small exercise. I call these solutions the “right solution”, based on building an expression to fit the goal in your file, and the “left solution”, based on taking advantage of (co)pattern-matching (sometimes known as “programming on the left”) as a means to decompose the problem.

It may be worth noting that Agda 2.6.3 – specifically, the introduction of --cubical-compatible – breaks the code of the original question because agda-categories is written with --without-K but not (yet?) --cubical-compatible.

The problem (but simpler)

Let's start with the following file. --postfix-projections is optional, but I like it and will use it later (in a non-essential way; it's just surface syntax).

{-# OPTIONS --postfix-projections --cubical #-}
module Gist where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

open import Data.Empty
open import Data.Product

Then, we can define two definitionally distinct functions of type ⊥ → ⊥:

id-⊥ : ⊥ → ⊥
id-⊥ x = x

!-⊥ : ⊥ → ⊥
!-⊥ ()

These functions are cubically equal by a simple argument eq. We can see that they are definitionally distinct because the proof cannot be refl.

eq : id-⊥ ≡ !-⊥
eq i ()

So far, so good. However, when we try to do a bigger proof quickly using interval variables, things fall apart. Here I use Path rather than _≡_ so as to give a type annotation to the pairs, because the type of the second component of a Σ-type is always unclear in lieu of annotations or contextual information.

eq2 : Path ((⊥ → ⊥) × (⊥ → ⊥)) (id-⊥ , id-⊥) (id-⊥ , !-⊥)
eq2 i = id-⊥ , λ ()

{-
x != (λ ()) x of type ⊥
when checking the definition of eq2
-}

What's wrong with this is that eq2 i0 = id-⊥ , λ (), where we expected it to be id-⊥ , id-⊥, matching the left-hand side of the equation we are trying to prove. When we define a path in cubical Agda, we have to check that the endpoints of each clause match definitionally when each interval variable is instantiated to i0 and i1. In eq, we had no checks to do because there were no clauses, whereas eq2 has a clause (signified by the = sign), and that clause fails one of the tests.

Right solution

Looking at the type of eq2 from a standard Agda perspective, the thing that jumps out at us is that both sides of the equation share a head constructor _,_ and the first component id-⊥. This is a prime candidate for a cong lemma. Unfortunately for us, the cong lemma from the cubical library allows full dependent Π-types for its function argument, making cong (id-⊥ ,_) ? suffer the same under-specification as what made us use Path above. Handily, however, Cubical.Foundations.Path provides a simpler lemma cong′ (quoted verbatim from the library):

-- Less polymorphic version of `cong`, to avoid some unresolved metas
cong′ : ∀ {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
      → Path B (f x) (f y)
cong′ f = cong f
{-# INLINE cong′ #-}

Using that lemma, we get our first solution:

eq2r : Path ((⊥ → ⊥) × (⊥ → ⊥)) (id-⊥ , id-⊥) (id-⊥ , !-⊥)
eq2r = cong′ (id-⊥ ,_) (λ { i () })

Note that, at the top level, eq2r is not defining a path via abstraction of an interval variable, so no boundary checks are required there. The extended λ-expression λ { i () } would be subject to boundary checks, except that it has no clauses to check (being essentially an inlining of eq). Note that λ i (), which is equivalent to λ i → λ (), does not work, because it has one clause returning λ (), which is not definitionally equal to id-⊥.

Left solution

When diagnosing the problem with eq2, we found that it had a clause, making it susceptible to boundary checks. In the right solution, we pushed the abstraction of the interval variable inside the clause, making the top-level definition not susceptible to boundary checks, and then eventually making a clausal definition of a path when we could refute any clauses.

Perhaps a more direct way to use cubical features is to ask Can we make the type of the path we're defining smaller?. The type (⊥ → ⊥) × (⊥ → ⊥) has quite a few moving parts, so if we can dig into it and just work at type ⊥, things might become simpler. To that end, we take an interval variable i, and then do a match with copatterns proj₁ and proj₂ to produce a pair. In the first case, we want a ⊥ → ⊥ which is id-⊥ when i = i0 and id-⊥ when i = i1. id-⊥ suffices. In the second case, id-⊥ and !-⊥ don't match on-the-nose, so we take an argument x : ⊥ and then match on x so as to not have any clauses to check. Note that the latter case is essentially an inlining of eq i.

eq2l : Path ((⊥ → ⊥) × (⊥ → ⊥)) (id-⊥ , id-⊥) (id-⊥ , !-⊥)
eq2l i .proj₁ = id-⊥
eq2l i .proj₂ ()

I'll let you decide which solution you prefer. I believe they behave equivalently, except maybe in some corner cases not respecting η-equality for records, like with. The behaviour of copatterns with respect to η for records may also have some performance implications for type-checking, which IIRC favour the left solution.

Answer 2

You're not going to be able to. It is consistent that there are multiple such functions. It is also consistent that there is only one.

When I ran into that issue (one of Laplaza's coherence conditions for Rig Categories when specialized to Agda's Set hinges on this), I solved it by carefully not matching on () but instead passing the impossibility through.

My guess is that there is some very subtle interactions between your definitions that you'll need to puzzle out to get there.

TL;DR: don't prematurely match (). That might not be the coherent definition.