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?)

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.

StackExchange Computer Science Q#98460, answer score: 7