Is the absence of bananas the same as the absence of anchovis (up to isomorphism)?
This and similar hole-istic questions drove me to this:

First, let's define lists and their length (in Coq):

Inductive list' (X:Type): Type :=
nil : list' X
cons : X -> list' X -> list' X.
Arguments nil {X}.
Arguments cons {X} _ _.
Notation "x :: y" := (cons x y).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Check list'.
Fixpoint length' {X : Type } (l : list' X) : nat :=
match l with
nil => O
cons h t => 1 + (length' t)
end.
Example test_length'1 : length' ([1;2;3]) = 3.
Proof. reflexivity. Qed.

It seems obvious that for any Type X the length of an empty list
of Type X elements is zero. And indeed this is provable in Coq:

Theorem length_type_invar: forall (X: Type), length (@nil X) = 0.
Proof.
intros X.
simpl.
reflexivity.
Qed.

But without the quantified Type, Coq cannot check the length of an empty list:

Example test_length'1 : length' ([]) = 0.
Error: Cannot infer the implicit parameter X of nil

Holey Schlamoney!
Two empty lists, one not containing natural numbers, the other not containing booleans,
cannot be compared:

Check @nil nat = @nil bool.
Error: The term "[ ]" has type "list bool" while it is expected to have type "list nat".

Coq can infer the Type of an empty list:

Example test_nil_nat: [] = @nil nat.
Proof. reflexivity. Qed.
Example test_nil_bool: [] = @nil bool.
Proof. reflexivity. Qed.

But an untyped nothingness cannot be compared to itself:

Example test_nil: [] = [].
Error: Cannot infer the implicit parameter X of nil whose type is "Type".

It is no wonder that philosophers concern themselves
with the concept of holes.