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.
$$ \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?