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 → ⊤))
(λ _ → ⊥))
commute = λ f@(mapDir ⇄ mapPos) -> λ i → (λ x → mapDir x , λ x₁ → tt) ⇄ {! !} ;
goal type:
(fromPos : Polynomial.position X) →
⊥ → Polynomial.direction X fromPos
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!
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
.
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.
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-⊥
.
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.