Why cannot match $Bool \equiv Bool$ with $refl$ while $1 \equiv 1$ can?

This code depends on agda-stdlib:

{-# OPTIONS --without-K #-}
open import Data.Nat
open import Data.Bool

open import Relation.Binary.PropositionalEquality

-- this code doesn't check, cannot match e with refl
why : (e : Bool ≡ Bool) -> ℕ
why refl = zero

but-why : (e : 1 ≡ 1) -> ℕ
but-why refl = zero

I know K-rule means I cannot match $$\forall a.a \equiv a$$ with $$refl$$, but if $$a$$ is a concrete value, it can (i.e. $$1 \equiv 1$$ can be matched with $$refl$$). But why I cannot match $$Bool \equiv Bool$$ with $$refl$$? Why is type and value treated differently in a dependently-typed programming language?

(Maybe related: What does it mean if we disable K-rule in Agda?)

Essentially, even without K, you can match against refl, but at least one of the endpoints must be an "unconstrained" variable. Both of these type check in Agda-sans-K:

foo : ∀ { A B : Set } -> A ≡ B → A → B
foo refl a = a

fooℕ : ∀ { A : Set } -> A ≡ ℕ → A → A
fooℕ refl a = a + 3

These cases are (probably) handled by a few standard induction principles for equality (AKA dependent elimination principles), such as "path induction" and "based path induction", which do not rely on axiom K, but are a fundamental ingredient in the definition of the equality type.

Instead, the following does not type check, since the two endpoints are constrained to be the same.

bar : ∀ { A : Set } -> A ≡ A → A → A
bar refl a = a

I'm unsure about why this does not work as expected. By comparison, in Coq this works fine:

Definition bar: forall A : Type, A = A -> A -> A :=
fun A p x =>
match p with
| eq_refl => x
end .

As the translation of the OP's code:

Definition foo: (bool = bool) -> nat :=
fun p =>
match p with
| eq_refl => 0
end .

In these two last cases, we do not even need dependent elimination, the regular non-dependent one suffices.

I guess that Agda, when no endpoint is "free", internally translates the match into some form which relies on axiom K, even if in some cases (like the above) there is no real need to do so.

One can indeed define the original why pattern match, by generalizing it so that at least one endpoint is "free".

why-generalized : {A : Set} -> (e : Bool ≡ A) -> ℕ
why-generalized {.Bool} refl = zero

why : (Bool ≡ Bool) -> ℕ
why = why-generalized

(Well, in this case we could also use why x = zero, but the point of the above code is to pattern match against refl)

• Perhaps the these particular functions don't actually depend on the argument is a factor in the behavior. – Derek Elkins Oct 12 '18 at 21:13
• @DerekElkins It's a possibility. I'm rather puzzled by Agda's behaviour here. – chi Oct 12 '18 at 21:20
• Agda doesn't bother trying to figure out if there is an equivalent non-K matching definition when your declared type is A = A. The type signature is primary. The reason The 1 = 1 example works indeed because it considers K to still hold for (you can write it with --without-K enabled). – Dan Doel Oct 13 '18 at 1:20
• I don't know why Coq would accept this definition, but it's definitely not possible to implement bar in basic Martin-Löf type theory with just the J eliminator for the identity type, which is (roughly) the guideline I used for implementing --without-K (see my thesis for more details). If Coq goes beyond that, then that's some peculiarity of the Coq theory. I think the main use case for --without-K is when you care particularly about compatibility with (extensions of) basic MLTT, so I would be hesitant to add some feature that goes beyond it just because Coq does the same. – Jesper Oct 13 '18 at 20:37
• (cross-posted from github.com/agda/agda/issues/3265) – Jesper Oct 13 '18 at 20:38

From the perspective of Homotopy Type Theory (HoTT), i.e. if we have the Univalence Axiom, there are definitely values of Bool ≡ Bool that are distinct from refl. Because Agda without Axiom K is compatible with univalence, it can't then assume that refl is the only value of type Bool ≡ Bool.

ℕ, on the other hand, is an h-set in HoTT (see Section 2.13 of the HoTT book). This is to say that Axiom K restricted to ℕ does hold. This is related to the fact that ℕ is inductively defined (with no parameters or indices) while Set is not.

I don't know the exact logic Agda uses. Presumably, it is something like it knows that nullary constructors of an inductive type are identified with themselves in only one way (which wouldn't be true for higher inductive types), and it knows suc is injective.

• I have to disagree with this. Coq (which does not assume axiom K) accepts the (translation of) code above just fine. Indeed, even with univalence, the induction principle of equality (AKA dependent elimination) still holds, and in order to define a function $f: a=b \to T$ it is enough to consider only the case where $b$ is $a$ and the argument of $f$ is reflexivity. The induction principle ensures that such a definition is automatically "extended" to all other inhabitants of $a=b$. So, the reason why Agda doesn't like this must be more subtle. – chi Oct 12 '18 at 11:33
• Still digging into what you said. I'll decide on accepting the answer after I know what is h-set and finish reading the "without K" paper. Sorry for a temporary unaccepting. – ice1000 Oct 12 '18 at 18:15