How come identity encodes absurdity

Question

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?

Answer 1

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!