can't apply proposition to itself?

Stream: general

[Kenny Lau]

def R : Prop :=
∀ p : Prop, ¬ p

example : Prop :=
R R

Error:

function expected at
  R
term has type
  Prop

[Kenny Lau]

why does R R give an error?

[Kenny Lau]

oh I think this example makes the reason clearer:

def R : Prop :=
∀ p : ℕ, p = 0

example : Prop :=
R 0 -- fails

[Kenny Lau]

then where is my Russell's paradox?

[Kenny Lau]

more nonsense:

def R : Prop :=
∀ p : Prop, ¬ p

example : ¬ R :=
λ H, H true trivial

[Bryan Gin-ge Chen]

In your first and second examples, R can't be applied to anything, since R is a Prop, not a Pi type. On the other hand, in your first example, given a term r : R it makes sense to write r R, but this doesn't return a Prop, it returns a proof of a Prop (specifically, a proof of ¬ R):

def R : Prop :=
∀ p : Prop, ¬ p

example (r : R) : ¬ R :=
r R