Streicher's K axiom but for List

Question

Some of the intuition behind relaxing Streicher's K axiom ("the only inhabitant of the identity type is reflexivity") is: "yes, there is only one uniformly definable element of the identity type $\mathrm{Id}_A$ as $A$ varies over all types, but why should that mean there is only one element of $\mathrm{Id}_{\mathrm{Bool}}$?".

$\mathrm{List}_A$ can be defined by the two constructors $\mathrm{Empty} : \mathrm{List}_A$ and $\mathrm{Cons} : A \to \mathrm{List}_A \to \mathrm{List}_A$.

Is there some implicit axiom here that the only inhabitants of $\mathrm{List}_A$ are those which are made from those two constructors - that is, some kind of K-but-for-lists? If we were to relax that axiom, what might a "non-uniformly-definable" member of $\mathrm{List}_{\mathrm{Bool}}$ look like? Or is it somehow the case that only $\mathrm{Id}$ has this property (which seems a bit unlikely to me)?

I recognise that we could just declare arbitrarily that $\mathrm{Fish}$ is a member of $\mathrm{List}_{\mathrm{Bool}}$, but that seems extremely artificial (much more so than univalence's "the identities are the equivalences").

Answer 1

The thing that does this for $\mathsf{List}_A$ is the inductive eliminator. We have an inductive eliminator which also lets us readily prove $\prod_{A:\mathcal U}\prod_{x:A}\mathsf{isContr}(\sum_{y:A}\mathsf{Id}_A(x,y))$ where $\mathsf{isContr}(T)\equiv\prod_{x,y:T}(\mathsf{Id}_T(x,y))$ which means $(x,\mathsf{refl}_x)$ is the "unique" value of $\sum_{y:A}\mathsf{Id}_A(x,y)$ for any appropriate $A$ and $x$.

The issue is that the definition of $\mathsf{Id}_A(x,y)$ is indexed (not parameterized) on $y$. This means that the definition doesn't say that $\mathsf{Id}_A(x,y)$ is inductively defined for every appropriate $A$, $x$, and $y$, but that $\sum_{y:A}\mathsf{Id}_A(x,y)$ is for every appropriate $A$ and $x$. (We could index by $x$ too leading to $\sum_{x,y:A}\mathsf{Id}_A(x,y)$ being inductively defined, but this is equivalent to having $x$ be a parameter.) As such, we have no basis for assuming that $\mathsf{refl}_x$ is the only value of type $\mathsf{Id}_A(x,x)$ because it is not an inductively defined type in general.

There's nothing terribly special about $\mathsf{Id}$. A similar sort of thing can apply to any indexed inductive type. For example, here's list membership defined as an inductively defined relation in Agda:

data _∈_ {A : Set} : A → List A → Set where
    Here : {x : A} → {xs : List A} → x ∈ Cons x xs
    There : {x y : A} → {xs : List A} → x ∈ xs → x ∈ Cons y xs

This should have the same sort of issues as $\mathsf{Id}$ (which is not surprising as I'm pretty confident you can prove that $\mathsf{Id}_A(x,y)$ is equivalent to $x\in_A\mathsf{Cons}(y,\mathsf{Empty})$). Namely, I claim that you can't prove (without $\mathsf K$) that $x\in_A\mathsf{Cons}(x,\mathsf{Empty})$ is only inhabited by $\mathsf{Here}_{x,\mathsf{Empty}}$.

Postulating $\mathsf{Fish}:\mathsf{List}_{\mathsf{Bool}}$ doesn't create a new value of $\mathsf{List}_{\mathsf{Bool}}$. It just produces a new constant that is a value of $\mathsf{List}_{\mathsf{Bool}}$, but we don't know what that value is. We can still do structural induction on it or show that it can't be anything other than $\mathsf{Empty}$ or $\mathsf{Cons}(x,xs)$ for some suitable $x$ and $xs$. We just can't actually calculate with it because we don't know which it is.