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) → τ.

Equations

• Function.FromTypes x_3 x = x
• Function.FromTypes p x = (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) x)

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

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

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

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

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

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

Equations

• Function.fromTypes_zero_equiv p τ = Equiv.refl (Function.FromTypes p τ)

@[simp]

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

@[simp]

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

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

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

Equations

• Function.fromTypes_nil_equiv τ = Function.fromTypes_zero_equiv ![] τ

@[simp]

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

@[simp]

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

def Function.fromTypes_succ_equiv {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) : Function.FromTypes p τ ≃ (Matrix.vecHead p → Function.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 τ.

Equations

• Function.fromTypes_succ_equiv p τ = Equiv.refl (Function.FromTypes p τ)

@[simp]

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

@[simp]

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

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

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

Equations

• Function.fromTypes_cons_equiv α p τ = Function.fromTypes_succ_equiv (Matrix.vecCons α p) τ

@[simp]

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

@[simp]

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

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

Constant n-ary function with value t.

Equations

• Function.FromTypes.const x_4 x = x
• Function.FromTypes.const p x = fun (x_1 : Matrix.vecHead p) => Function.FromTypes.const (Matrix.vecTail p) x

@[simp]

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

@[simp]

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

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

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

Equations

• Function.FromTypes.inhabited = { default := Function.FromTypes.const p default }