How come identity encodes absurdity

From P5 in this paper: https://hal.inria.fr/hal-01094195/file/CIC.pdf


Using this purely functional part, it is possible to encode many int
eresting notions. For instance
∀
C
:
Prop
, C
is a logical proposition (a term of type
Prop
) which encodes absurdity (
⊥
) : there is
no closed term of type
∀
C
:
Prop
, C
(so no proof of
⊥
without hypothesis) and also from a proof
t
of
∀
C
:
Prop
, C
one can build a proof
t C
of an arbitrary proposition
C
so the natural deduction
rule for eliminating
⊥
is derivable in the logic.

where

$$
\forall C: Prop, C
$$

looks entirely identity function to me, which can definitely be inhabited by a closed term. Why the author said it encodes absurdity?

If I were to encode absurdity, I would do

$$
\exists P: Prop, P \to \forall Q:Prop, Q
$$

That is, there exists a proposition which derives everything. From category theoretic perspective, it's precisely how the initial object is defined, which can encode absurdity with no doubt.

Did I misread it in a terrible wrong way that the author was actually right? How about my encoding, does it make sense to you?

looks entirely identity function to me, which can definitely be inhabited by a closed term

A proof of $\forall C : Prop, C$ is a function from an arbitrary proposition to its proof. Since a proposition isn't a proof, an identity function is not a function from propositions to proofs.

The identity function (or rather, a function returning the identity function on proofs of $C$) corresponds instead to the proof of $\forall C : Prop, C \to C$. That's even the example on the beginning of page 3!

StackExchange Computer Science Q#81500, answer score: 6