what is an "arrow type"?

Stream: new members

[rzeta0]

The following is a quite from the beginning of TPIL chapter 7:

It is remarkable that it is possible to construct a substantial edifice of mathematics based on nothing more than the type universes, dependent arrow types, and inductive types; everything else follows from those.

I tink I understand 2 of the 3 objects: type universes (eg ℕ and Prop), and I am about to find out a lot more about inductive types.

But what is an "arrow type"? Is it a function? That is a thing that maps from one type to another?

Is the following Triangle " an arrow type", specifically of type ℕ → Prop?

(and just to check this arrow has nothing to do with logical implication?)

import Mathlib.Tactic

def Triangle (a : ℕ) : Prop := ∃ n, 2 * a = n * (n + 1)

example : Triangle 10 := by
  dsimp [Triangle]
  use 4

#check @Triangle --------- Triangle : ℕ → Prop

[Johan Commelin]

rzeta0 said:

If the following Triangle " an arrow type", specifically of type ℕ → Prop?

Yes.

(and just to check this arrow has nothing to do with logical implication?)

every logical implication is an arrow type, but not every arrow type is a logical implication.

[Johan Commelin]

The type of functions X -> Y is an arrow type. But more generally, there are dependent function types (also called Pi types), and those are the most general kind of arrow types in Lean.