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.12} n = (Fin2 n → Type ?u.12)

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

Equations

• instInhabitedTypeVec = { default := fun (x : Fin2 n) => PUnit.{?u.12 + 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

• α.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 g : α.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 (α.Arrow β)

Equations

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

def TypeVec.id {n : ℕ} {α : TypeVec.{u_1} n} : α.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 : β.Arrow γ) (f : α.Arrow β) : α.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 : α.Arrow β) : comp id f = f

@[simp]

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

theorem TypeVec.comp_assoc {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_3} n} {δ : TypeVec.{u_4} n} (h : γ.Arrow δ) (g : β.Arrow γ) (f : α.Arrow β) : comp (comp h g) f = comp h (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

• (α ::: β) i.fs = α 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

• α.drop i = α i.fs

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

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

Equations

• α.last = α Fin2.fz

instance TypeVec.last.inhabited {n : ℕ} (α : TypeVec.{u_1} (n + 1)) [Inhabited (α Fin2.fz)] : Inhabited α.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} : (α ::: β).drop i = α i

@[simp]

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

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

@[simp]

theorem TypeVec.append1_drop_last {n : ℕ} (α : TypeVec.{u_1} (n + 1)) : α.drop ::: α.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 γ = ⋯.mpr (H γ.drop γ.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) : append1Cases H (α ::: β) = H α β

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

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

Equations

• TypeVec.splitFun f g i.fs = f i
• TypeVec.splitFun f g Fin2.fz = g

def TypeVec.appendFun {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : β → β') : (α ::: β).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 : α.Arrow β) : α.drop.Arrow β.drop

split off the prefix of an arrow

Equations

• TypeVec.dropFun f i = f i.fs

def TypeVec.lastFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} (f : α.Arrow β) : α.last → β.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} : α.Arrow β

arrow in the category of 0-length vectors

Equations

• TypeVec.nilFun i = i.elim0

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

@[simp]

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

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

turn an equality into an arrow

Equations

• TypeVec.Arrow.mp h x✝ = ⋯.mp

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

turn an equality into an arrow, with reverse direction

Equations

• TypeVec.Arrow.mpr h x✝ = ⋯.mpr

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

decompose a vector into its prefix appended with its last element

Equations

• TypeVec.toAppend1DropLast = TypeVec.Arrow.mpr ⋯

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

stitch two bits of a vector back together

Equations

• TypeVec.fromAppend1DropLast = TypeVec.Arrow.mp ⋯

@[simp]

theorem TypeVec.lastFun_splitFun {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.last → α'.last) : lastFun (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 : α.Arrow α') (g : β → β') : 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 : α.Arrow α') (g : β → β') : lastFun (f ::: g) = g

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

theorem TypeVec.splitFun_inj {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} {f f' : α.drop.Arrow α'.drop} {g g' : α.last → α'.last} (H : splitFun f g = 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 f' : α.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₀ : α₀.drop.Arrow α₁.drop) (f₁ : α₁.drop.Arrow α₂.drop) (g₀ : α₀.last → α₁.last) (g₁ : α₁.last → α₂.last) : splitFun (comp f₁ f₀) (g₁ ∘ g₀) = comp (splitFun f₁ g₁) (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₀ : ε.drop.Arrow α) (f₁ : α.Arrow γ) (g₀ : ε.last → β) (g₁ : β → δ) : comp (f₁ ::: g₁) (splitFun f₀ g₀) = splitFun (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₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) : (comp f₁ f₀ ::: g₁ ∘ g₀) = 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₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) : comp (f₁ ::: g₁) (f₀ ::: g₀) = (comp f₁ f₀ ::: g₁ ∘ g₀)

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

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

@[simp]

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

@[simp]

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

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

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

instance 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 ⋯ 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 ⋯ (f v.last v.drop)

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) → v.Arrow v' → Sort u_1} (f : β Fin2.elim0 Fin2.elim0 nilFun) (v : TypeVec.{u_2} 0) (v' : TypeVec.{u_3} 0) (fs : v.Arrow 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 ⋯ f

def TypeVec.typevecCasesCons₃ (n : ℕ) {β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v.Arrow 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 : v.Arrow v') → β (v ::: t) (v' ::: t') (fs ::: f)) (v : TypeVec.{u_2} (n + 1)) (v' : TypeVec.{u_3} (n + 1)) (fs : v.Arrow 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₂ {β : Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} (f : β nilFun) (f✝ : 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 = ⋯.mpr f

def TypeVec.typevecCasesCons₂ (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n) {β : (v ::: t).Arrow (v' ::: t') → Sort u_3} (F : (f : t → t') → (fs : v.Arrow v') → β (fs ::: f)) (fs : (v ::: t).Arrow (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 = ⋯.mpr (F (TypeVec.lastFun fs) (TypeVec.dropFun fs))

theorem TypeVec.typevecCasesNil₂_appendFun {β : Arrow Fin2.elim0 Fin2.elim0 → Sort u_1} (f : β nilFun) : typevecCasesNil₂ f 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) {β : (v ::: t).Arrow (v' ::: t') → Sort u_3} (F : (f : t → t') → (fs : v.Arrow v') → β (fs ::: f)) (f : t → t') (fs : v.Arrow v') : 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

• α.PredLast p = fun (x : (α ::: β) i.fs) => True
• α.PredLast p = p

def TypeVec.RelLast {n : ℕ} (α : TypeVec.{u} n) {β γ : 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

• α.RelLast r = Eq
• α.RelLast r = 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 i.succ 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

• x_3.prod x_4 = Fin2.elim0
• α.prod β = α.drop.prod β.drop ::: (α.last × β.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) : α.Arrow («repeat» n β)

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

Equations

• TypeVec.const x α a.fs = TypeVec.const x α.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) : (α.prod α).Arrow («repeat» n Prop)

vector of equality on a product of vectors

Equations

• x_2.repeatEq = TypeVec.nilFun
• α.repeatEq = (α.drop.repeatEq ::: 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 : α.Arrow β) : f = nilFun

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

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

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

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

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

predicate on a type vector to constrain only the last object

Equations

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

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

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

Equations

• α.RelLast' p = TypeVec.splitFun α.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 (Curry F α β)

Equations

• TypeVec.Curry.inhabited F α β = I

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

arrow to remove one element of a repeat vector

Equations

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

def TypeVec.ofRepeat {α : Type u_1} {n : ℕ} {i : Fin2 n} : «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} : ofRepeat (TypeVec.const p α i x) ↔ p

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

left projection of a prod vector

Equations

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

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

right projection of a prod vector

Equations

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

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

introduce a product where both components are the same

Equations

• TypeVec.prod.diag a.fs 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} (i : Fin2 n) : α i → β i → α.prod β i

constructor for prod

Equations

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

@[simp]

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

@[simp]

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

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

prod is functorial

Equations

• TypeVec.prod.map x_9 y a.fs 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.1, y Fin2.fz a.2)

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} (f : α.Arrow β) (g : α'.Arrow β') : comp prod.fst (prod.map f g) = comp f prod.fst

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

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

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

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

def TypeVec.Subtype_ {n : ℕ} {α : TypeVec.{u} n} : α.Arrow («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 i.fs = TypeVec.Subtype_ (TypeVec.dropFun p) i

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

projection on Subtype_

Equations

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

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

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

Equations

• TypeVec.toSubtype p i.fs 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 : α.Arrow («repeat» n Prop)) : (Subtype_ p).Arrow fun (i : Fin2 n) => { x : α i // 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 i.fs 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 : (α.prod α).Arrow («repeat» n Prop)) : Arrow (fun (i : Fin2 n) => { x : α i × α i // ofRepeat (p i (prod.mk i x.1 x.2)) }) (Subtype_ p)

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

Equations

• TypeVec.toSubtype' p_2 i.fs x_2 = TypeVec.toSubtype' (TypeVec.dropFun p_2) i x_2
• TypeVec.toSubtype' p_2 Fin2.fz x_2 = ⟨↑x_2, ⋯⟩

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

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

Equations

• TypeVec.ofSubtype' p_2 i.fs x_2 = TypeVec.ofSubtype' (TypeVec.dropFun p_2) i x_2
• TypeVec.ofSubtype' p_2 Fin2.fz x_2 = ⟨↑x_2, ⋯⟩

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

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

Equations

• TypeVec.diagSub a.fs x_2 = TypeVec.diagSub a x_2
• TypeVec.diagSub Fin2.fz x_2 = ⟨(x_2, x_2), ⋯⟩

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem TypeVec.subtypeVal_toSubtype {n : ℕ} {α : TypeVec.{u_1} n} (p : α.Arrow («repeat» n Prop)) : comp (subtypeVal p) (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 : α.Arrow («repeat» n Prop)) (f : β.Arrow (Subtype_ p)) : comp (toSubtype p) (comp (ofSubtype p) f) = f

@[simp]

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

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