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

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

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

arrow in the category of TypeVec

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

arrow in the category of TypeVec

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

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

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

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

identity of arrow composition

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

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

arrow composition in the category of TypeVec

@[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.

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

Support for extending a TypeVec by one element.

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

retain only a n-length prefix of the argument

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

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

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

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

@[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

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

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

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

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

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

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

arrow in the category of 0-length vectors

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

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

turn an equality into an arrow, with reverse direction

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

decompose a vector into its prefix appended with its last element

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

stitch two bits of a vector back together

@[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

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

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

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

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

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

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 β.

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.

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

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

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

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

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

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

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

vector of equality on a product of vectors

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

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

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

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

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

arrow to remove one element of a repeat vector

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

projection for a repeat vector

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

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

right projection of a prod vector

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

introduce a product where both components are the same

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

constructor for prod

@[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

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

prod is functorial

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

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

projection on Subtype_

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

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

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)

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)

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

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