How can I write an n-ary predicate type

Stream: new members

[nemo]

I need a function f such that for n : Nat and \alpha : Sort*, it returns the n-ary predicate type f n \alpha := \alpha -> \alpha -> ... -> \alpha -> Prop.

I tried to find such a function and got Function.OfArity. But Function.OfArity requires that the domain and codomain are on the same universe level, so if I use it, then I would have to lift Prop up to the same universe as alpha, which is undesired. I tried to find a version for predicates and failed.

Do I have to implement it by myself?

[Robin Arnez]

Why not use (Fin n -> \alpha) -> Prop or Vector \alpha n -> Prop?

[nemo]

Because I want it to be definitionally \alpha -> Prop and \alpha->\alpha->Prop for the cases where n = 1 or n = 2

[Robin Arnez]

What do you want to use it for?

[Eric Wieser]

You could use OfArity a (a -> Prop) (n - 1)

[nemo]

I want to defined a Kripke frame and I need to define the accessibility relation in the most general sence, which is an n-ary relation.

[nemo]

If I use OfArity a (a -> Prop) (n-1), then it would fail at the case where n=0

[Robin Arnez]

The thing is that Prop lives in universe Type and \alpha -> Prop (where alpha : Type u) lives in Type u. But if you unify them under one f they need to have the same universe

[Robin Arnez]

You could use one of these though:

def f (α : Type u) (n : Nat) := Function.OfArity α (ULift Prop) n
def f' (α : Type u) (n : Nat) := Function.OfArity α (PUnit.{u + 1} → Prop) n

[Robin Arnez]

Or the very weird and awkward to work with

def f (α : Type u) (n : Nat) :=
  match n with
  | 0 => ULift Prop
  | k + 1 => Function.OfArity α (α → Prop) k

[nemo]

I have just found it necessary to leave out the case for 0-ary predicates, since Prop is in Type but \alpha \to prop is in a higher universe

[nemo]

So I think I'm going to take the OfArity \alpha (\alpha \to Prop) approach