Function types of a given heterogeneous arity

This provides Function.FromTypes, such that FromTypes ![α, β] τ = α → β → τ. Note that it is often preferable to use ((i : Fin n) → p i) → τ in place of FromTypes p τ.

Main definitions

• Function.FromTypes p τ: n-ary function p 0 → p 1 → ... → p (n - 1) → β.

def Function.FromTypes {n : ℕ} : (Fin n → Type u) → Type u → Type u

The type of n-ary functions p 0 → p 1 → ... → p (n - 1) → τ.

theorem Function.fromTypes_zero (p : Fin 0 → Type u) (τ : Type u) : FromTypes p τ = τ

theorem Function.fromTypes_nil (τ : Type u) : FromTypes ![] τ = τ

theorem Function.fromTypes_succ {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) : FromTypes p τ = (Matrix.vecHead p → FromTypes (Matrix.vecTail p) τ)

theorem Function.fromTypes_cons {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) : FromTypes (Matrix.vecCons α p) τ = (α → FromTypes p τ)

def Function.fromTypes_zero_equiv (p : Fin 0 → Type u) (τ : Type u) : FromTypes p τ ≃ τ

The definitional equality between 0-ary heterogeneous functions into τ and τ.

@[simp]

theorem Function.fromTypes_zero_equiv_apply (p : Fin 0 → Type u) (τ : Type u) (a : FromTypes p τ) : (fromTypes_zero_equiv p τ) a = a

@[simp]

theorem Function.fromTypes_zero_equiv_symm_apply (p : Fin 0 → Type u) (τ : Type u) (a : FromTypes p τ) : (fromTypes_zero_equiv p τ).symm a = a

def Function.fromTypes_nil_equiv (τ : Type u) : FromTypes ![] τ ≃ τ

The definitional equality between ![]-ary heterogeneous functions into τ and τ.

@[simp]

theorem Function.fromTypes_nil_equiv_symm_apply (τ : Type u) (a : FromTypes ![] τ) : (fromTypes_nil_equiv τ).symm a = a

@[simp]

theorem Function.fromTypes_nil_equiv_apply (τ : Type u) (a : FromTypes ![] τ) : (fromTypes_nil_equiv τ) a = a

def Function.fromTypes_succ_equiv {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) : FromTypes p τ ≃ (Matrix.vecHead p → FromTypes (Matrix.vecTail p) τ)

The definitional equality between p-ary heterogeneous functions into τ and function from vecHead p to (vecTail p)-ary heterogeneous functions into τ.

@[simp]

theorem Function.fromTypes_succ_equiv_apply {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : FromTypes p τ) : (fromTypes_succ_equiv p τ) a = a

@[simp]

theorem Function.fromTypes_succ_equiv_symm_apply {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : FromTypes p τ) : (fromTypes_succ_equiv p τ).symm a = a

def Function.fromTypes_cons_equiv {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) : FromTypes (Matrix.vecCons α p) τ ≃ (α → FromTypes p τ)

The definitional equality between (vecCons α p)-ary heterogeneous functions into τ and function from α to p-ary heterogeneous functions into τ.

@[simp]

theorem Function.fromTypes_cons_equiv_symm_apply {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) (a : FromTypes (Matrix.vecCons α p) τ) : (fromTypes_cons_equiv α p τ).symm a = a

@[simp]

theorem Function.fromTypes_cons_equiv_apply {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) (a : FromTypes (Matrix.vecCons α p) τ) : (fromTypes_cons_equiv α p τ) a = a

def Function.FromTypes.const {n : ℕ} (p : Fin n → Type u) {τ : Type u} (t : τ) : FromTypes p τ

Constant n-ary function with value t.

@[simp]

theorem Function.FromTypes.const_zero (p : Fin 0 → Type u) {τ : Type u} (t : τ) : const p t = t

@[simp]

theorem Function.FromTypes.const_succ {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) : const p t = fun (x : Matrix.vecHead p) => const (Matrix.vecTail p) t

theorem Function.FromTypes.const_succ_apply {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) (x : p 0) : const p t x = const (Matrix.vecTail p) t

@[implicit_reducible]

instance Function.FromTypes.inhabited {n : ℕ} {p : Fin n → Type u} {τ : Type u} [Inhabited τ] : Inhabited (FromTypes p τ)