Tuples of types, and their categorical structure.

Features

• TypeVec n - n-tuples of types
• α ⟹ β - n-tuples of maps
• f ⊚ g - composition

Also, support functions for operating with n-tuples of types, such as:

• append1 α β - append type β to n-tuple α to obtain an (n+1)-tuple
• drop α - drops the last element of an (n+1)-tuple
• last α - returns the last element of an (n+1)-tuple
• appendFun f g - appends a function g to an n-tuple of functions
• dropFun f - drops the last function from an n+1-tuple
• lastFun f - returns the last function of a tuple.

Since e.g. append1 α.drop α.last is propositionally equal to α but not definitionally equal to it, we need support functions and lemmas to mediate between constructions.

def TypeVec (n : ℕ) : Type (u_1 + 1)

n-tuples of types, as a category

Equations

• TypeVec.{u_1} n = (Fin2 n → Type u_1)

instance instInhabitedTypeVec {n : ℕ} : Inhabited (TypeVec.{u} n)

Equations

• instInhabitedTypeVec = { default := fun (x : Fin2 n) => PUnit.{u + 1} }

def TypeVec.Arrow {n : ℕ} (α : TypeVec.{u_1} n) (β : TypeVec.{u_2} n) : Type (max u_1 u_2)

arrow in the category of TypeVec

Equations

• TypeVec.Arrow α β = ((i : Fin2 n) → α i → β i)

def MvFunctor.«term_⟹_» : Lean.TrailingParserDescr

arrow in the category of TypeVec

Equations

• MvFunctor.«term_⟹_» = Lean.ParserDescr.trailingNode `MvFunctor.term_⟹_ 40 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 41))

theorem TypeVec.Arrow.ext {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α β) : (∀ (i : Fin2 n), f i = g i) → f = g

Extensionality for arrows

instance TypeVec.Arrow.inhabited {n : ℕ} (α : TypeVec.{u_1} n) (β : TypeVec.{u_2} n) [(i : Fin2 n) → Inhabited (β i)] : Inhabited (TypeVec.Arrow α β)

Equations

• TypeVec.Arrow.inhabited α β = { default := fun (x : Fin2 n) (x_1 : α x) => default }

def TypeVec.id {n : ℕ} {α : TypeVec.{u_1} n} : TypeVec.Arrow α α

identity of arrow composition

Equations

• TypeVec.id x✝ x = x

def TypeVec.comp {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_3} n} (g : TypeVec.Arrow β γ) (f : TypeVec.Arrow α β) : TypeVec.Arrow α γ

arrow composition in the category of TypeVec

Equations

• TypeVec.comp g f i x = g i (f i x)

def MvFunctor.«term_⊚_» : Lean.TrailingParserDescr

arrow composition in the category of TypeVec

Equations

• MvFunctor.«term_⊚_» = Lean.ParserDescr.trailingNode `MvFunctor.term_⊚_ 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊚ ") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem TypeVec.id_comp {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : TypeVec.Arrow α β) : TypeVec.comp TypeVec.id f = f

@[simp]

theorem TypeVec.comp_id {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : TypeVec.Arrow α β) : TypeVec.comp f TypeVec.id = f

theorem TypeVec.comp_assoc {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_3} n} {δ : TypeVec.{u_4} n} (h : TypeVec.Arrow γ δ) (g : TypeVec.Arrow β γ) (f : TypeVec.Arrow α β) : TypeVec.comp (TypeVec.comp h g) f = TypeVec.comp h (TypeVec.comp g f)

def TypeVec.append1 {n : ℕ} (α : TypeVec.{u_1} n) (β : Type u_1) : TypeVec.{u_1} (n + 1)

Support for extending a TypeVec by one element.

Equations

• (α ::: β) x = match x with | Fin2.fs i => α i | Fin2.fz => β

def TypeVec.«term_:::_» : Lean.TrailingParserDescr

Support for extending a TypeVec by one element.

Equations

• TypeVec.«term_:::_» = Lean.ParserDescr.trailingNode `TypeVec.term_:::_ 67 67 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::: ") (Lean.ParserDescr.cat `term 68))

def TypeVec.drop {n : ℕ} (α : TypeVec.{u} (n + 1)) : TypeVec.{u} n

retain only a n-length prefix of the argument

Equations

• TypeVec.drop α i = α (Fin2.fs i)

def TypeVec.last {n : ℕ} (α : TypeVec.{u} (n + 1)) : Type u

take the last value of a (n+1)-length vector

Equations

• TypeVec.last α = α Fin2.fz

instance TypeVec.last.inhabited {n : ℕ} (α : TypeVec.{u_1} (n + 1)) [Inhabited (α Fin2.fz)] : Inhabited (TypeVec.last α)

Equations

• TypeVec.last.inhabited α = { default := let_fun this := default; this }

theorem TypeVec.drop_append1 {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} {i : Fin2 n} : TypeVec.drop (α ::: β) i = α i

@[simp]

theorem TypeVec.drop_append1' {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} : TypeVec.drop (α ::: β) = α

theorem TypeVec.last_append1 {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} : TypeVec.last (α ::: β) = β

@[simp]

theorem TypeVec.append1_drop_last {n : ℕ} (α : TypeVec.{u_1} (n + 1)) : TypeVec.drop α ::: TypeVec.last α = α

def TypeVec.append1Cases {n : ℕ} {C : TypeVec.{u_1} (n + 1) → Sort u} (H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)) (γ : TypeVec.{u_1} (n + 1)) : C γ

cases on (n+1)-length vectors

Equations

• TypeVec.append1Cases H γ = Eq.mpr (_ : C γ = C (TypeVec.drop γ ::: TypeVec.last γ)) (H (TypeVec.drop γ) (TypeVec.last γ))

@[simp]

theorem TypeVec.append1_cases_append1 {n : ℕ} {C : TypeVec.{u_1} (n + 1) → Sort u} (H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)) (α : TypeVec.{u_1} n) (β : Type u_1) : TypeVec.append1Cases H (α ::: β) = H α β

def TypeVec.splitFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop α')) (g : TypeVec.last α → TypeVec.last α') : TypeVec.Arrow α α'

append an arrow and a function for arbitrary source and target type vectors

Equations

• TypeVec.splitFun f g x = match (motive := (x : Fin2 (n + 1)) → α x → α' x) x with | Fin2.fs i => f i | Fin2.fz => g

def TypeVec.appendFun {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : TypeVec.Arrow α α') (g : β → β') : TypeVec.Arrow (α ::: β) (α' ::: β')

append an arrow and a function as well as their respective source and target types / typevecs

Equations

• (f ::: g) = TypeVec.splitFun f g

def TypeVec.«term_:::__1» : Lean.TrailingParserDescr

append an arrow and a function as well as their respective source and target types / typevecs

Equations

• TypeVec.«term_:::__1» = Lean.ParserDescr.trailingNode `TypeVec.term_:::__1 0 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::: ") (Lean.ParserDescr.cat `term 1))

def TypeVec.dropFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow α β) : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop β)

split off the prefix of an arrow

Equations

• TypeVec.dropFun f i = f (Fin2.fs i)

def TypeVec.lastFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow α β) : TypeVec.last α → TypeVec.last β

split off the last function of an arrow

Equations

• TypeVec.lastFun f = f Fin2.fz

def TypeVec.nilFun {α : TypeVec.{u_1} 0} {β : TypeVec.{u_2} 0} : TypeVec.Arrow α β

arrow in the category of 0-length vectors

Equations

• TypeVec.nilFun i = Fin2.elim0 i

theorem TypeVec.eq_of_drop_last_eq {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} {f : TypeVec.Arrow α β} {g : TypeVec.Arrow α β} (h₀ : TypeVec.dropFun f = TypeVec.dropFun g) (h₁ : TypeVec.lastFun f = TypeVec.lastFun g) : f = g

@[simp]

theorem TypeVec.dropFun_splitFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop α')) (g : TypeVec.last α → TypeVec.last α') : TypeVec.dropFun (TypeVec.splitFun f g) = f

def TypeVec.Arrow.mp {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (h : α = β) : TypeVec.Arrow α β

turn an equality into an arrow

Equations

• TypeVec.Arrow.mp h x = match (motive := (x : Fin2 n) → α x → β x) x with | x => Eq.mp (_ : α x = β x)

def TypeVec.Arrow.mpr {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (h : α = β) : TypeVec.Arrow β α

turn an equality into an arrow, with reverse direction

Equations

• TypeVec.Arrow.mpr h x = match (motive := (x : Fin2 n) → β x → α x) x with | x => Eq.mpr (_ : α x = β x)

def TypeVec.toAppend1DropLast {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.Arrow α (TypeVec.drop α ::: TypeVec.last α)

decompose a vector into its prefix appended with its last element

Equations

• TypeVec.toAppend1DropLast = TypeVec.Arrow.mpr (_ : TypeVec.drop α ::: TypeVec.last α = α)

def TypeVec.fromAppend1DropLast {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.Arrow (TypeVec.drop α ::: TypeVec.last α) α

stitch two bits of a vector back together

Equations

• TypeVec.fromAppend1DropLast = TypeVec.Arrow.mp (_ : TypeVec.drop α ::: TypeVec.last α = α)

@[simp]

theorem TypeVec.lastFun_splitFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop α')) (g : TypeVec.last α → TypeVec.last α') : TypeVec.lastFun (TypeVec.splitFun f g) = g

@[simp]

theorem TypeVec.dropFun_appendFun {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : TypeVec.Arrow α α') (g : β → β') : TypeVec.dropFun (f ::: g) = f

@[simp]

theorem TypeVec.lastFun_appendFun {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : TypeVec.Arrow α α') (g : β → β') : TypeVec.lastFun (f ::: g) = g

theorem TypeVec.split_dropFun_lastFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : TypeVec.Arrow α α') : TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f) = f

theorem TypeVec.splitFun_inj {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} {f : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop α')} {f' : TypeVec.Arrow (TypeVec.drop α) (TypeVec.drop α')} {g : TypeVec.last α → TypeVec.last α'} {g' : TypeVec.last α → TypeVec.last α'} (H : TypeVec.splitFun f g = TypeVec.splitFun f' g') : f = f' ∧ g = g'

theorem TypeVec.appendFun_inj {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} {f : TypeVec.Arrow α α'} {f' : TypeVec.Arrow α α'} {g : β → β'} {g' : β → β'} : (f ::: g) = (f' ::: g') → f = f' ∧ g = g'

theorem TypeVec.splitFun_comp {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : TypeVec.Arrow (TypeVec.drop α₀) (TypeVec.drop α₁)) (f₁ : TypeVec.Arrow (TypeVec.drop α₁) (TypeVec.drop α₂)) (g₀ : TypeVec.last α₀ → TypeVec.last α₁) (g₁ : TypeVec.last α₁ → TypeVec.last α₂) : TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀) = TypeVec.comp (TypeVec.splitFun f₁ g₁) (TypeVec.splitFun f₀ g₀)

theorem TypeVec.appendFun_comp_splitFun {n : ℕ} {α : TypeVec.{u_1} n} {γ : TypeVec.{u_2} n} {β : Type u_1} {δ : Type u_2} {ε : TypeVec.{u_3} (n + 1)} (f₀ : TypeVec.Arrow (TypeVec.drop ε) α) (f₁ : TypeVec.Arrow α γ) (g₀ : TypeVec.last ε → β) (g₁ : β → δ) : TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀)

theorem TypeVec.appendFun_comp {n : ℕ} {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) : (TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)

theorem TypeVec.appendFun_comp' {n : ℕ} {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) : TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀) = (TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀)

theorem TypeVec.nilFun_comp {α₀ : TypeVec.{u_1} 0} (f₀ : TypeVec.Arrow α₀ Fin2.elim0) : TypeVec.comp TypeVec.nilFun f₀ = f₀

theorem TypeVec.appendFun_comp_id {n : ℕ} {α : TypeVec.{u} n} {β₀ : Type u} {β₁ : Type u} {β₂ : Type u} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) : (TypeVec.id ::: g₁ ∘ g₀) = TypeVec.comp (TypeVec.id ::: g₁) (TypeVec.id ::: g₀)

@[simp]

theorem TypeVec.dropFun_comp {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) : TypeVec.dropFun (TypeVec.comp f₁ f₀) = TypeVec.comp (TypeVec.dropFun f₁) (TypeVec.dropFun f₀)

@[simp]

theorem TypeVec.lastFun_comp {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) : TypeVec.lastFun (TypeVec.comp f₁ f₀) = TypeVec.lastFun f₁ ∘ TypeVec.lastFun f₀

theorem TypeVec.appendFun_aux {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : TypeVec.Arrow (α ::: β) (α' ::: β')) : (TypeVec.dropFun f ::: TypeVec.lastFun f) = f

theorem TypeVec.appendFun_id_id {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} : (TypeVec.id ::: id) = TypeVec.id

instance TypeVec.subsingleton0 : Subsingleton (TypeVec.{u_1} 0)

Equations

• TypeVec.subsingleton0 = (_ : Subsingleton (TypeVec.{u_1} 0))

def TypeVec.casesNil {β : TypeVec.{u_2} 0 → Sort u_1} (f : β Fin2.elim0) (v : TypeVec.{u_2} 0) : β v

cases distinction for 0-length type vector

Equations

• TypeVec.casesNil f v = cast (_ : β Fin2.elim0 = β v) f

def TypeVec.casesCons (n : ℕ) {β : TypeVec.{u_2} (n + 1) → Sort u_1} (f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)) (v : TypeVec.{u_2} (n + 1)) : β v

cases distinction for (n+1)-length type vector

Equations

• TypeVec.casesCons n f v = cast (_ : β (TypeVec.drop v ::: TypeVec.last v) = β v) (f (TypeVec.last v) (TypeVec.drop v))

theorem TypeVec.casesNil_append1 {β : TypeVec.{u_2} 0 → Sort u_1} (f : β Fin2.elim0) : TypeVec.casesNil f Fin2.elim0 = f

theorem TypeVec.casesCons_append1 (n : ℕ) {β : TypeVec.{u_2} (n + 1) → Sort u_1} (f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)) (v : TypeVec.{u_2} n) (α : Type u_2) : TypeVec.casesCons n f (v ::: α) = f α v

def TypeVec.typevecCasesNil₃ {β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → TypeVec.Arrow v v' → Sort u_1} (f : β Fin2.elim0 Fin2.elim0 TypeVec.nilFun) (v : TypeVec.{u_2} 0) (v' : TypeVec.{u_3} 0) (fs : TypeVec.Arrow v v') : β v v' fs

cases distinction for an arrow in the category of 0-length type vectors

Equations

• TypeVec.typevecCasesNil₃ f v v' fs = cast (_ : β Fin2.elim0 Fin2.elim0 TypeVec.nilFun = β v v' fs) f

def TypeVec.typevecCasesCons₃ (n : ℕ) {β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → TypeVec.Arrow v v' → Sort u_1} (F : (t : Type u_2) → (t' : Type u_3) → (f : t → t') → (v : TypeVec.{u_2} n) → (v' : TypeVec.{u_3} n) → (fs : TypeVec.Arrow v v') → β (v ::: t) (v' ::: t') (fs ::: f)) (v : TypeVec.{u_2} (n + 1)) (v' : TypeVec.{u_3} (n + 1)) (fs : TypeVec.Arrow v v') : β v v' fs

cases distinction for an arrow in the category of (n+1)-length type vectors

Equations

• One or more equations did not get rendered due to their size.

def TypeVec.typevecCasesNil₂ {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} (f : β TypeVec.nilFun) (f : TypeVec.Arrow Fin2.elim0 Fin2.elim0) : β f

specialized cases distinction for an arrow in the category of 0-length type vectors

Equations

• TypeVec.typevecCasesNil₂ f g = let_fun this := (_ : g = TypeVec.nilFun); Eq.mpr (_ : β g = β TypeVec.nilFun) f

def TypeVec.typevecCasesCons₂ (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n) {β : TypeVec.Arrow (v ::: t) (v' ::: t') → Sort u_3} (F : (f : t → t') → (fs : TypeVec.Arrow v v') → β (fs ::: f)) (fs : TypeVec.Arrow (v ::: t) (v' ::: t')) : β fs

specialized cases distinction for an arrow in the category of (n+1)-length type vectors

Equations

• TypeVec.typevecCasesCons₂ n t t' v v' F fs = Eq.mpr (_ : β fs = β (TypeVec.splitFun (TypeVec.dropFun fs) (TypeVec.lastFun fs))) (F (TypeVec.lastFun fs) (TypeVec.dropFun fs))

theorem TypeVec.typevecCasesNil₂_appendFun {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} (f : β TypeVec.nilFun) : TypeVec.typevecCasesNil₂ f TypeVec.nilFun = f

theorem TypeVec.typevecCasesCons₂_appendFun (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n) {β : TypeVec.Arrow (v ::: t) (v' ::: t') → Sort u_3} (F : (f : t → t') → (fs : TypeVec.Arrow v v') → β (fs ::: f)) (f : t → t') (fs : TypeVec.Arrow v v') : TypeVec.typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs

def TypeVec.PredLast {n : ℕ} (α : TypeVec.{u_1} n) {β : Type u_1} (p : β → Prop) ⦃i : Fin2 (n + 1)⦄ : (α ::: β) i → Prop

PredLast α p x predicates p of the last element of x : α.append1 β.

Equations

• TypeVec.PredLast α p = match (motive := (x : Fin2 (n + 1)) → (α ::: β) x → Prop) x with | Fin2.fs a => fun (x : (α ::: β) (Fin2.fs a)) => True | Fin2.fz => p

def TypeVec.RelLast {n : ℕ} (α : TypeVec.{u} n) {β : Type u} {γ : Type u} (r : β → γ → Prop) ⦃i : Fin2 (n + 1)⦄ : (α ::: β) i → (α ::: γ) i → Prop

RelLast α r x y says that p the last elements of x y : α.append1 β are related by r and all the other elements are equal.

Equations

• TypeVec.RelLast α r = match (motive := (x : Fin2 (n + 1)) → (α ::: β) x → (α ::: γ) x → Prop) x with | Fin2.fs a => Eq | Fin2.fz => r

def TypeVec.repeat (n : ℕ) : Type u_1 → TypeVec.{u_1} n

repeat n t is a n-length type vector that contains n occurrences of t

Equations

• TypeVec.repeat 0 x = Fin2.elim0
• TypeVec.repeat (Nat.succ i) x = TypeVec.repeat i x ::: x

def TypeVec.prod {n : ℕ} : TypeVec.{u} n → TypeVec.{u} n → TypeVec.{u} n

prod α β is the pointwise product of the components of α and β

Equations

• TypeVec.prod x_3 x_4 = Fin2.elim0
• TypeVec.prod α β = TypeVec.prod (TypeVec.drop α) (TypeVec.drop β) ::: (TypeVec.last α × TypeVec.last β)

def MvFunctor.«term_⊗_» : Lean.TrailingParserDescr

prod α β is the pointwise product of the components of α and β

Equations

• MvFunctor.«term_⊗_» = Lean.ParserDescr.trailingNode `MvFunctor.term_⊗_ 45 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 46))

def TypeVec.const {β : Type u_1} (x : β) {n : ℕ} (α : TypeVec.{u_2} n) : TypeVec.Arrow α (TypeVec.repeat n β)

const x α is an arrow that ignores its source and constructs a TypeVec that contains nothing but x

Equations

• TypeVec.const x α (Fin2.fs a) = TypeVec.const x (TypeVec.drop α) a
• TypeVec.const x x_4 Fin2.fz = fun (x_1 : x_4 Fin2.fz) => x

def TypeVec.repeatEq {n : ℕ} (α : TypeVec.{u_1} n) : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)

vector of equality on a product of vectors

Equations

• TypeVec.repeatEq x_2 = TypeVec.nilFun
• TypeVec.repeatEq α = (TypeVec.repeatEq (TypeVec.drop α) ::: Function.uncurry Eq)

theorem TypeVec.const_append1 {β : Type u_1} {γ : Type u_2} (x : γ) {n : ℕ} (α : TypeVec.{u_1} n) : TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun (x_1 : β) => x)

theorem TypeVec.eq_nilFun {α : TypeVec.{u_1} 0} {β : TypeVec.{u_2} 0} (f : TypeVec.Arrow α β) : f = TypeVec.nilFun

theorem TypeVec.id_eq_nilFun {α : TypeVec.{u_1} 0} : TypeVec.id = TypeVec.nilFun

theorem TypeVec.const_nil {β : Type u_1} (x : β) (α : TypeVec.{u_2} 0) : TypeVec.const x α = TypeVec.nilFun

theorem TypeVec.repeat_eq_append1 {β : Type u_1} {n : ℕ} (α : TypeVec.{u_1} n) : TypeVec.repeatEq (α ::: β) = TypeVec.splitFun (TypeVec.repeatEq α) (Function.uncurry Eq)

theorem TypeVec.repeat_eq_nil (α : TypeVec.{u_1} 0) : TypeVec.repeatEq α = TypeVec.nilFun

def TypeVec.PredLast' {n : ℕ} (α : TypeVec.{u_1} n) {β : Type u_1} (p : β → Prop) : TypeVec.Arrow (α ::: β) (TypeVec.repeat (n + 1) Prop)

predicate on a type vector to constrain only the last object

Equations

• TypeVec.PredLast' α p = TypeVec.splitFun (TypeVec.const True α) p

def TypeVec.RelLast' {n : ℕ} (α : TypeVec.{u_1} n) {β : Type u_1} (p : β → β → Prop) : TypeVec.Arrow (TypeVec.prod (α ::: β) (α ::: β)) (TypeVec.repeat (n + 1) Prop)

predicate on the product of two type vectors to constrain only their last object

Equations

• TypeVec.RelLast' α p = TypeVec.splitFun (TypeVec.repeatEq α) (Function.uncurry p)

def TypeVec.Curry {n : ℕ} (F : TypeVec.{u} (n + 1) → Type u_1) (α : Type u) (β : TypeVec.{u} n) : Type u_1

given F : TypeVec.{u} (n+1) → Type u, curry F : Type u → TypeVec.{u} → Type u, i.e. its first argument can be fed in separately from the rest of the vector of arguments

Equations

• TypeVec.Curry F α β = F (β ::: α)

instance TypeVec.Curry.inhabited {n : ℕ} (F : TypeVec.{u} (n + 1) → Type u_1) (α : Type u) (β : TypeVec.{u} n) [I : Inhabited (F (β ::: α))] : Inhabited (TypeVec.Curry F α β)

Equations

• TypeVec.Curry.inhabited F α β = I

def TypeVec.dropRepeat (α : Type u_1) {n : ℕ} : TypeVec.Arrow (TypeVec.drop (TypeVec.repeat (Nat.succ n) α)) (TypeVec.repeat n α)

arrow to remove one element of a repeat vector

Equations

• TypeVec.dropRepeat α (Fin2.fs i) = TypeVec.dropRepeat α i
• TypeVec.dropRepeat α Fin2.fz = fun (a : α) => a

def TypeVec.ofRepeat {α : Type u_1} {n : ℕ} {i : Fin2 n} : TypeVec.repeat n α i → α

projection for a repeat vector

Equations

• TypeVec.ofRepeat = fun (a : α) => a
• TypeVec.ofRepeat = TypeVec.ofRepeat

theorem TypeVec.const_iff_true {n : ℕ} {α : TypeVec.{u_1} n} {i : Fin2 n} {x : α i} {p : Prop} : TypeVec.ofRepeat (TypeVec.const p α i x) ↔ p

def TypeVec.prod.fst {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{u} n} : TypeVec.Arrow (TypeVec.prod α β) α

left projection of a prod vector

Equations

• TypeVec.prod.fst (Fin2.fs i) = TypeVec.prod.fst i
• TypeVec.prod.fst Fin2.fz = Prod.fst

def TypeVec.prod.snd {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{u} n} : TypeVec.Arrow (TypeVec.prod α β) β

right projection of a prod vector

Equations

• TypeVec.prod.snd (Fin2.fs i) = TypeVec.prod.snd i
• TypeVec.prod.snd Fin2.fz = Prod.snd

def TypeVec.prod.diag {n : ℕ} {α : TypeVec.{u} n} : TypeVec.Arrow α (TypeVec.prod α α)

introduce a product where both components are the same

Equations

• TypeVec.prod.diag (Fin2.fs a) x_4 = TypeVec.prod.diag a x_4
• TypeVec.prod.diag Fin2.fz x_5 = (x_5, x_5)

def TypeVec.prod.mk {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{u} n} (i : Fin2 n) : α i → β i → TypeVec.prod α β i

constructor for prod

Equations

• TypeVec.prod.mk (Fin2.fs i) = TypeVec.prod.mk i
• TypeVec.prod.mk Fin2.fz = Prod.mk

@[simp]

theorem TypeVec.prod_fst_mk {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i) : TypeVec.prod.fst i (TypeVec.prod.mk i a b) = a

@[simp]

theorem TypeVec.prod_snd_mk {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i) : TypeVec.prod.snd i (TypeVec.prod.mk i a b) = b

def TypeVec.prod.map {n : ℕ} {α : TypeVec.{u} n} {α' : TypeVec.{u} n} {β : TypeVec.{u} n} {β' : TypeVec.{u} n} : TypeVec.Arrow α β → TypeVec.Arrow α' β' → TypeVec.Arrow (TypeVec.prod α α') (TypeVec.prod β β')

prod is functorial

Equations

• TypeVec.prod.map x_9 y (Fin2.fs a) a_1 = TypeVec.prod.map (TypeVec.dropFun x_9) (TypeVec.dropFun y) a a_1
• TypeVec.prod.map x_13 y Fin2.fz a = (x_13 Fin2.fz a.fst, y Fin2.fz a.snd)

def MvFunctor.«term_⊗'_» : Lean.TrailingParserDescr

prod is functorial

Equations

• MvFunctor.«term_⊗'_» = Lean.ParserDescr.trailingNode `MvFunctor.term_⊗'_ 45 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗' ") (Lean.ParserDescr.cat `term 46))

theorem TypeVec.fst_prod_mk {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} {β' : TypeVec.{u_1} n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α' β') : TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst

theorem TypeVec.snd_prod_mk {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} {β' : TypeVec.{u_1} n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α' β') : TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd

theorem TypeVec.fst_diag {n : ℕ} {α : TypeVec.{u_1} n} : TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id

theorem TypeVec.snd_diag {n : ℕ} {α : TypeVec.{u_1} n} : TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id

theorem TypeVec.repeatEq_iff_eq {n : ℕ} {α : TypeVec.{u_1} n} {i : Fin2 n} {x : α i} {y : α i} : TypeVec.ofRepeat (TypeVec.repeatEq α i (TypeVec.prod.mk i x y)) ↔ x = y

def TypeVec.Subtype_ {n : ℕ} {α : TypeVec.{u} n} : TypeVec.Arrow α (TypeVec.repeat n Prop) → TypeVec.{u} n

given a predicate vector p over vector α, Subtype_ p is the type of vectors that contain an α that satisfies p

Equations

• TypeVec.Subtype_ p Fin2.fz = { x : x_4 Fin2.fz // p Fin2.fz x }
• TypeVec.Subtype_ p (Fin2.fs i) = TypeVec.Subtype_ (TypeVec.dropFun p) i

def TypeVec.subtypeVal {n : ℕ} {α : TypeVec.{u} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) : TypeVec.Arrow (TypeVec.Subtype_ p) α

projection on Subtype_

Equations

• TypeVec.subtypeVal x_5 (Fin2.fs i) = TypeVec.subtypeVal (TypeVec.dropFun x_5) i
• TypeVec.subtypeVal x_5 Fin2.fz = Subtype.val

def TypeVec.toSubtype {n : ℕ} {α : TypeVec.{u} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) : TypeVec.Arrow (fun (i : Fin2 n) => { x : α i // TypeVec.ofRepeat (p i x) }) (TypeVec.Subtype_ p)

arrow that rearranges the type of Subtype_ to turn a subtype of vector into a vector of subtypes

Equations

• TypeVec.toSubtype p (Fin2.fs i) x_6 = TypeVec.toSubtype (TypeVec.dropFun p) i x_6
• TypeVec.toSubtype x_6 Fin2.fz x_7 = x_7

def TypeVec.ofSubtype {n : ℕ} {α : TypeVec.{u} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) : TypeVec.Arrow (TypeVec.Subtype_ p) fun (i : Fin2 n) => { x : α i // TypeVec.ofRepeat (p i x) }

arrow that rearranges the type of Subtype_ to turn a vector of subtypes into a subtype of vector

Equations

• TypeVec.ofSubtype p_2 (Fin2.fs i) x_2 = TypeVec.ofSubtype (TypeVec.dropFun p_2) i x_2
• TypeVec.ofSubtype p_2 Fin2.fz x_2 = x_2

def TypeVec.toSubtype' {n : ℕ} {α : TypeVec.{u} n} (p : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) : TypeVec.Arrow (fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.fst x.snd)) }) (TypeVec.Subtype_ p)

similar to toSubtype adapted to relations (i.e. predicate on product)

Equations

• TypeVec.toSubtype' p_2 (Fin2.fs i) x_2 = TypeVec.toSubtype' (TypeVec.dropFun p_2) i x_2
• TypeVec.toSubtype' p_2 Fin2.fz x_2 = { val := ↑x_2, property := (_ : p_2 Fin2.fz ↑x_2) }

def TypeVec.ofSubtype' {n : ℕ} {α : TypeVec.{u} n} (p : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) : TypeVec.Arrow (TypeVec.Subtype_ p) fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.fst x.snd)) }

similar to of_subtype adapted to relations (i.e. predicate on product)

Equations

• TypeVec.ofSubtype' p_2 (Fin2.fs i) x_2 = TypeVec.ofSubtype' (TypeVec.dropFun p_2) i x_2
• TypeVec.ofSubtype' p_2 Fin2.fz x_2 = { val := ↑x_2, property := (_ : TypeVec.ofRepeat (p_2 Fin2.fz (TypeVec.prod.mk Fin2.fz (↑x_2).fst (↑x_2).snd))) }

def TypeVec.diagSub {n : ℕ} {α : TypeVec.{u} n} : TypeVec.Arrow α (TypeVec.Subtype_ (TypeVec.repeatEq α))

similar to diag but the target vector is a Subtype_ guaranteeing the equality of the components

Equations

• TypeVec.diagSub (Fin2.fs a) x_2 = TypeVec.diagSub a x_2
• TypeVec.diagSub Fin2.fz x_2 = { val := (x_2, x_2), property := (_ : (x_2, x_2).fst = (x_2, x_2).fst) }

theorem TypeVec.subtypeVal_nil {α : TypeVec.{u} 0} (ps : TypeVec.Arrow α (TypeVec.repeat 0 Prop)) : TypeVec.subtypeVal ps = TypeVec.nilFun

theorem TypeVec.diag_sub_val {n : ℕ} {α : TypeVec.{u} n} : TypeVec.comp (TypeVec.subtypeVal (TypeVec.repeatEq α)) TypeVec.diagSub = TypeVec.prod.diag

theorem TypeVec.prod_id {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{u} n} : TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id

theorem TypeVec.append_prod_appendFun {n : ℕ} {α : TypeVec.{u} n} {α' : TypeVec.{u} n} {β : TypeVec.{u} n} {β' : TypeVec.{u} n} {φ : Type u} {φ' : Type u} {ψ : Type u} {ψ' : Type u} {f₀ : TypeVec.Arrow α α'} {g₀ : TypeVec.Arrow β β'} {f₁ : φ → φ'} {g₁ : ψ → ψ'} : (TypeVec.prod.map f₀ g₀ ::: Prod.map f₁ g₁) = TypeVec.prod.map (f₀ ::: f₁) (g₀ ::: g₁)

@[simp]

theorem TypeVec.dropFun_diag {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.dropFun TypeVec.prod.diag = TypeVec.prod.diag

@[simp]

theorem TypeVec.dropFun_subtypeVal {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.dropFun (TypeVec.subtypeVal p) = TypeVec.subtypeVal (TypeVec.dropFun p)

@[simp]

theorem TypeVec.lastFun_subtypeVal {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.lastFun (TypeVec.subtypeVal p) = Subtype.val

@[simp]

theorem TypeVec.dropFun_toSubtype {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.dropFun (TypeVec.toSubtype p) = TypeVec.toSubtype fun (i : Fin2 n) (x : α (Fin2.fs i)) => p (Fin2.fs i) x

@[simp]

theorem TypeVec.lastFun_toSubtype {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.lastFun (TypeVec.toSubtype p) = id

@[simp]

theorem TypeVec.dropFun_of_subtype {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.dropFun (TypeVec.ofSubtype p) = TypeVec.ofSubtype (TypeVec.dropFun p)

@[simp]

theorem TypeVec.lastFun_of_subtype {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : TypeVec.Arrow α (TypeVec.repeat (n + 1) Prop)) : TypeVec.lastFun (TypeVec.ofSubtype p) = id

@[simp]

theorem TypeVec.dropFun_RelLast' {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1} (R : β → β → Prop) : TypeVec.dropFun (TypeVec.RelLast' α R) = TypeVec.repeatEq α

@[simp]

theorem TypeVec.dropFun_prod {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_1} (n + 1)} {β' : TypeVec.{u_1} (n + 1)} (f : TypeVec.Arrow α β) (f' : TypeVec.Arrow α' β') : TypeVec.dropFun (TypeVec.prod.map f f') = TypeVec.prod.map (TypeVec.dropFun f) (TypeVec.dropFun f')

@[simp]

theorem TypeVec.lastFun_prod {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_1} (n + 1)} {β' : TypeVec.{u_1} (n + 1)} (f : TypeVec.Arrow α β) (f' : TypeVec.Arrow α' β') : TypeVec.lastFun (TypeVec.prod.map f f') = Prod.map (TypeVec.lastFun f) (TypeVec.lastFun f')

@[simp]

theorem TypeVec.dropFun_from_append1_drop_last {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.dropFun TypeVec.fromAppend1DropLast = TypeVec.id

@[simp]

theorem TypeVec.lastFun_from_append1_drop_last {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.lastFun TypeVec.fromAppend1DropLast = id

@[simp]

theorem TypeVec.dropFun_id {n : ℕ} {α : TypeVec.{u_1} (n + 1)} : TypeVec.dropFun TypeVec.id = TypeVec.id

@[simp]

theorem TypeVec.prod_map_id {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} : TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id

@[simp]

theorem TypeVec.subtypeVal_diagSub {n : ℕ} {α : TypeVec.{u_1} n} : TypeVec.comp (TypeVec.subtypeVal (TypeVec.repeatEq α)) TypeVec.diagSub = TypeVec.prod.diag

@[simp]

theorem TypeVec.toSubtype_of_subtype {n : ℕ} {α : TypeVec.{u_1} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) : TypeVec.comp (TypeVec.toSubtype p) (TypeVec.ofSubtype p) = TypeVec.id

@[simp]

theorem TypeVec.subtypeVal_toSubtype {n : ℕ} {α : TypeVec.{u_1} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) : TypeVec.comp (TypeVec.subtypeVal p) (TypeVec.toSubtype p) = fun (x : Fin2 n) => Subtype.val

@[simp]

theorem TypeVec.toSubtype_of_subtype_assoc {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) (f : TypeVec.Arrow β (TypeVec.Subtype_ p)) : TypeVec.comp (TypeVec.toSubtype p) (TypeVec.comp (TypeVec.ofSubtype fun (i : Fin2 n) (x : α i) => p i x) f) = f

@[simp]

theorem TypeVec.toSubtype'_of_subtype' {n : ℕ} {α : TypeVec.{u_1} n} (r : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) : TypeVec.comp (TypeVec.toSubtype' r) (TypeVec.ofSubtype' r) = TypeVec.id

theorem TypeVec.subtypeVal_toSubtype' {n : ℕ} {α : TypeVec.{u_1} n} (r : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) : TypeVec.comp (TypeVec.subtypeVal r) (TypeVec.toSubtype' r) = fun (i : Fin2 n) (x : (fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (r i (TypeVec.prod.mk i x.fst x.snd)) }) i) => TypeVec.prod.mk i (↑x).fst (↑x).snd