Tuples of types, and their categorical structure. #

Features #

TypeVec n - n-tuples of types
α ⟹ β⟹ β - n-tuples of maps
f ⊚ g⊚ 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.

source

ink

def TypeVec (n : ℕ) :

Type (u_1+1)

n-tuples of types, as a category

Equations

TypeVec n = (Fin2 n → Type u_1)

source

ink

instance instInhabitedTypeVec {n : ℕ} :

Inhabited (TypeVec n)

Equations

instInhabitedTypeVec = { default := fun x => PUnit }

source

ink

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

Type (maxu_1u_2)

arrow in the category of TypeVec

Equations

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

source

ink

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))

source

ink

theorem TypeVec.Arrow.ext {n : ℕ} {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α β) :

(∀ (i : Fin2 n), f i = g i) → f = g

Extensionality for arrows

source

ink

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

Inhabited (TypeVec.Arrow α β)

Equations

TypeVec.Arrow.inhabited α β = { default := fun x x_1 => default }

source

ink

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

TypeVec.Arrow α α

identity of arrow composition

Equations

TypeVec.id x x = x

source

ink

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

source

ink

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))

source

ink

@[simp]

theorem TypeVec.id_comp {n : ℕ} {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) :

TypeVec.comp TypeVec.id f = f

source

ink

@[simp]

theorem TypeVec.comp_id {n : ℕ} {α : TypeVec n} {β : TypeVec n} (f : TypeVec.Arrow α β) :

TypeVec.comp f TypeVec.id = f

source

ink

theorem TypeVec.comp_assoc {n : ℕ} {α : TypeVec n} {β : TypeVec n} {γ : TypeVec n} {δ : TypeVec n} (h : TypeVec.Arrow γ δ) (g : TypeVec.Arrow β γ) (f : TypeVec.Arrow α β) :

TypeVec.comp (TypeVec.comp h g) f = TypeVec.comp h (TypeVec.comp g f)

source

ink

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

TypeVec (n + 1)

Support for extending a TypeVec by one element.

Equations

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

source

ink

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))

source

ink

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

TypeVec n

retain only a n-length prefix of the argument

Equations

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

source

ink

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

Type u

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

Equations

TypeVec.last α = α Fin2.fz

source

ink

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

Inhabited (TypeVec.last α)

Equations

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

source

ink

theorem TypeVec.drop_append1 {n : ℕ} {α : TypeVec n} {β : Type u_1} {i : Fin2 n} :

TypeVec.drop (α ::: β) i = α i

source

ink

@[simp]

theorem TypeVec.drop_append1' {n : ℕ} {α : TypeVec n} {β : Type u_1} :

TypeVec.drop (α ::: β) = α

source

ink

theorem TypeVec.last_append1 {n : ℕ} {α : TypeVec n} {β : Type u_1} :

TypeVec.last (α ::: β) = β

source

ink

@[simp]

theorem TypeVec.append1_drop_last {n : ℕ} (α : TypeVec (n + 1)) :

TypeVec.drop α ::: TypeVec.last α = α

source

ink

def TypeVec.append1Cases {n : ℕ} {C : TypeVec (n + 1) → Sort u} (H : (α : TypeVec n) → (β : Type u_1) → C (α ::: β)) (γ : TypeVec (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 γ))

source

ink

@[simp]

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

TypeVec.append1Cases H (α ::: β) = H α β

source

ink

def TypeVec.splitFun {n : ℕ} {α : TypeVec (n + 1)} {α' : TypeVec (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

source

ink

def TypeVec.appendFun {n : ℕ} {α : TypeVec n} {α' : TypeVec 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

source

ink

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))

source

ink

def TypeVec.dropFun {n : ℕ} {α : TypeVec (n + 1)} {β : TypeVec (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)

source

ink

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

TypeVec.last α → TypeVec.last β

split off the last function of an arrow

Equations

TypeVec.lastFun f = f Fin2.fz

source

ink

def TypeVec.nilFun {α : TypeVec 0} {β : TypeVec 0} :

TypeVec.Arrow α β

arrow in the category of 0-length vectors

Equations

TypeVec.nilFun i = Fin2.elim0 i

source

ink

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

f = g

source

ink

@[simp]

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

TypeVec.dropFun (TypeVec.splitFun f g) = f

source

ink

def TypeVec.Arrow.mp {n : ℕ} {α : TypeVec n} {β : TypeVec 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)

source

ink

def TypeVec.Arrow.mpr {n : ℕ} {α : TypeVec n} {β : TypeVec 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)

source

ink

def TypeVec.toAppend1DropLast {n : ℕ} {α : TypeVec (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 α = α)

source

ink

def TypeVec.fromAppend1DropLast {n : ℕ} {α : TypeVec (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 α = α)

source

ink

@[simp]

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

TypeVec.lastFun (TypeVec.splitFun f g) = g

source

ink

@[simp]

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

TypeVec.dropFun (f ::: g) = f

source

ink

@[simp]

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

TypeVec.lastFun (f ::: g) = g

source

ink

theorem TypeVec.split_dropFun_lastFun {n : ℕ} {α : TypeVec (n + 1)} {α' : TypeVec (n + 1)} (f : TypeVec.Arrow α α') :

TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f) = f

source

ink

theorem TypeVec.splitFun_inj {n : ℕ} {α : TypeVec (n + 1)} {α' : TypeVec (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'

source

ink

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

(f ::: g) = (f' ::: g') → f = f' ∧ g = g'

source

ink

theorem TypeVec.splitFun_comp {n : ℕ} {α₀ : TypeVec (n + 1)} {α₁ : TypeVec (n + 1)} {α₂ : TypeVec (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₀)

source

ink

theorem TypeVec.appendFun_comp_splitFun {n : ℕ} {α : TypeVec n} {γ : TypeVec n} {β : Type u_1} {δ : Type u_2} {ε : TypeVec (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₀)

source

ink

theorem TypeVec.appendFun_comp {n : ℕ} {α₀ : TypeVec n} {α₁ : TypeVec n} {α₂ : TypeVec 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₀)

source

ink

theorem TypeVec.appendFun_comp' {n : ℕ} {α₀ : TypeVec n} {α₁ : TypeVec n} {α₂ : TypeVec 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₀)

source

ink

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

TypeVec.comp TypeVec.nilFun f₀ = f₀

source

ink

theorem TypeVec.appendFun_comp_id {n : ℕ} {α : TypeVec n} {β₀ : Type u_1} {β₁ : Type u_1} {β₂ : Type u_1} (g₀ : β₀ → β₁) (g₁ : β₁ → β₂) :

(TypeVec.id ::: g₁ ∘ g₀) = TypeVec.comp (TypeVec.id ::: g₁) (TypeVec.id ::: g₀)

source

ink

@[simp]

theorem TypeVec.dropFun_comp {n : ℕ} {α₀ : TypeVec (n + 1)} {α₁ : TypeVec (n + 1)} {α₂ : TypeVec (n + 1)} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) :

TypeVec.dropFun (TypeVec.comp f₁ f₀) = TypeVec.comp (TypeVec.dropFun f₁) (TypeVec.dropFun f₀)

source

ink

@[simp]

theorem TypeVec.lastFun_comp {n : ℕ} {α₀ : TypeVec (n + 1)} {α₁ : TypeVec (n + 1)} {α₂ : TypeVec (n + 1)} (f₀ : TypeVec.Arrow α₀ α₁) (f₁ : TypeVec.Arrow α₁ α₂) :

TypeVec.lastFun (TypeVec.comp f₁ f₀) = TypeVec.lastFun f₁ ∘ TypeVec.lastFun f₀

source

ink

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

(TypeVec.dropFun f ::: TypeVec.lastFun f) = f

source

ink

theorem TypeVec.appendFun_id_id {n : ℕ} {α : TypeVec n} {β : Type u_1} :

(TypeVec.id ::: id) = TypeVec.id

source

ink

instance TypeVec.subsingleton0 :

Subsingleton (TypeVec 0)

Equations

TypeVec.subsingleton0 = TypeVec.subsingleton0.proof_1

source

ink

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

β v

cases distinction for 0-length type vector

Equations

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

source

ink

def TypeVec.casesCons (n : ℕ) {β : TypeVec (n + 1) → Sort u_2} (f : (t : Type u_1) → (v : TypeVec n) → β (v ::: t)) (v : TypeVec (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))

source

ink

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

TypeVec.casesNil f Fin2.elim0 = f

source

ink

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

TypeVec.casesCons n f (v ::: α) = f α v

source

ink

def TypeVec.typevecCasesNil₃ {β : (v : TypeVec 0) → (v' : TypeVec 0) → TypeVec.Arrow v v' → Sort u_3} (f : β Fin2.elim0 Fin2.elim0 TypeVec.nilFun) (v : TypeVec 0) (v' : TypeVec 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

source

ink

def TypeVec.typevecCasesCons₃ (n : ℕ) {β : (v : TypeVec (n + 1)) → (v' : TypeVec (n + 1)) → TypeVec.Arrow v v' → Sort u_3} (F : (t : Type u_1) → (t' : Type u_2) → (f : t → t') → (v : TypeVec n) → (v' : TypeVec n) → (fs : TypeVec.Arrow v v') → β (v ::: t) (v' ::: t') (fs ::: f)) (v : TypeVec (n + 1)) (v' : TypeVec (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.

source

ink

def TypeVec.typevecCasesNil₂ {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0 → Sort u_3} (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 = Eq.mpr (_ : β g = β TypeVec.nilFun) f

source

ink

def TypeVec.typevecCasesCons₂ (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec n) (v' : TypeVec 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))

source

ink

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

TypeVec.typevecCasesNil₂ f TypeVec.nilFun = f

source

ink

theorem TypeVec.typevecCasesCons₂_appendFun (n : ℕ) (t : Type u_1) (t' : Type u_2) (v : TypeVec n) (v' : TypeVec 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

source

ink

def TypeVec.PredLast {n : ℕ} (α : TypeVec 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 => True | Fin2.fz => p

source

ink

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

source

ink

def TypeVec.repeat (n : ℕ) :

Type u_1 → TypeVec n

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

Equations

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

source

ink

def TypeVec.prod {n : ℕ} :

TypeVec n → TypeVec n → TypeVec 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 β)

source

ink

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))

source

ink

def TypeVec.const {β : Type u_1} (x : β) {n : ℕ} (α : TypeVec 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 => x

source

ink

def TypeVec.repeatEq {n : ℕ} (α : TypeVec 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)

source

ink

theorem TypeVec.const_append1 {β : Type u_1} {γ : Type u_2} (x : γ) {n : ℕ} (α : TypeVec n) :

TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x => x)

source

ink

theorem TypeVec.eq_nilFun {α : TypeVec 0} {β : TypeVec 0} (f : TypeVec.Arrow α β) :

f = TypeVec.nilFun

source

ink

theorem TypeVec.id_eq_nilFun {α : TypeVec 0} :

TypeVec.id = TypeVec.nilFun

source

ink

theorem TypeVec.const_nil {β : Type u_1} (x : β) (α : TypeVec 0) :

TypeVec.const x α = TypeVec.nilFun

source

ink

theorem TypeVec.repeat_eq_append1 {β : Type u_1} {n : ℕ} (α : TypeVec n) :

TypeVec.repeatEq (α ::: β) = TypeVec.splitFun (TypeVec.repeatEq α) (Function.uncurry Eq)

source

ink

theorem TypeVec.repeat_eq_nil (α : TypeVec 0) :

TypeVec.repeatEq α = TypeVec.nilFun

source

ink

def TypeVec.PredLast' {n : ℕ} (α : TypeVec 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

source

ink

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

source

ink

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

Type u_1

given F : TypeVec.{u} (n+1) → Type u→ Type u, curry F : Type u → TypeVec.{u} → Type u→ TypeVec.{u} → Type 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 (β ::: α)

source

ink

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

Inhabited (TypeVec.Curry F α β)

Equations

TypeVec.Curry.inhabited F α β = I

source

ink

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

source

ink

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

source

ink

theorem TypeVec.const_iff_true {n : ℕ} {α : TypeVec n} {i : Fin2 n} {x : α i} {p : Prop} :

TypeVec.ofRepeat (TypeVec.const p α i x) ↔ p

source

ink

def TypeVec.prod.fst {n : ℕ} {α : TypeVec n} {β : TypeVec 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

source

ink

def TypeVec.prod.snd {n : ℕ} {α : TypeVec n} {β : TypeVec 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

source

ink

def TypeVec.prod.diag {n : ℕ} {α : TypeVec 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)

source

ink

def TypeVec.prod.mk {n : ℕ} {α : TypeVec n} {β : TypeVec 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

source

ink

@[simp]

theorem TypeVec.prod_fst_mk {n : ℕ} {α : TypeVec n} {β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :

TypeVec.prod.fst i (TypeVec.prod.mk i a b) = a

source

ink

@[simp]

theorem TypeVec.prod_snd_mk {n : ℕ} {α : TypeVec n} {β : TypeVec n} (i : Fin2 n) (a : α i) (b : β i) :

TypeVec.prod.snd i (TypeVec.prod.mk i a b) = b

source

ink

def TypeVec.prod.map {n : ℕ} {α : TypeVec n} {α' : TypeVec n} {β : TypeVec n} {β' : TypeVec 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)

source

ink

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))

source

ink

theorem TypeVec.fst_prod_mk {n : ℕ} {α : TypeVec n} {α' : TypeVec n} {β : TypeVec n} {β' : TypeVec n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α' β') :

TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst

source

ink

theorem TypeVec.snd_prod_mk {n : ℕ} {α : TypeVec n} {α' : TypeVec n} {β : TypeVec n} {β' : TypeVec n} (f : TypeVec.Arrow α β) (g : TypeVec.Arrow α' β') :

TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd

source

ink

theorem TypeVec.fst_diag {n : ℕ} {α : TypeVec n} :

TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id

source

ink

theorem TypeVec.snd_diag {n : ℕ} {α : TypeVec n} :

TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id

source

ink

theorem TypeVec.repeatEq_iff_eq {n : ℕ} {α : TypeVec n} {i : Fin2 n} {x : α i} {y : α i} :

TypeVec.ofRepeat (TypeVec.repeatEq α i (TypeVec.prod.mk i x y)) ↔ x = y

source

ink

def TypeVec.Subtype_ {n : ℕ} {α : TypeVec n} :

TypeVec.Arrow α (TypeVec.repeat n Prop) → TypeVec 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 // p Fin2.fz x }
TypeVec.Subtype_ p (Fin2.fs i) = TypeVec.Subtype_ (TypeVec.dropFun p) i

source

ink

def TypeVec.subtypeVal {n : ℕ} {α : TypeVec 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

source

ink

def TypeVec.toSubtype {n : ℕ} {α : TypeVec n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) :

TypeVec.Arrow (fun i => { x // 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

source

ink

def TypeVec.ofSubtype {n : ℕ} {α : TypeVec n} (p : TypeVec.Arrow α (TypeVec.repeat n Prop)) :

TypeVec.Arrow (TypeVec.Subtype_ p) fun i => { x // 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

source

ink

def TypeVec.toSubtype' {n : ℕ} {α : TypeVec n} (p : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) :

TypeVec.Arrow (fun i => { x // 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

One or more equations did not get rendered due to their size.
TypeVec.toSubtype' p_2 (Fin2.fs i) x_2 = TypeVec.toSubtype' (TypeVec.dropFun p_2) i x_2

source

ink

def TypeVec.ofSubtype' {n : ℕ} {α : TypeVec n} (p : TypeVec.Arrow (TypeVec.prod α α) (TypeVec.repeat n Prop)) :

TypeVec.Arrow (TypeVec.Subtype_ p) fun i => { x // 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.val, property := (_ : TypeVec.ofRepeat (p_2 Fin2.fz (TypeVec.prod.mk Fin2.fz x_2.val.fst x_2.val.snd))) }

source

ink

def TypeVec.diagSub {n : ℕ} {α : TypeVec 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) }

source

ink

theorem TypeVec.subtypeVal_nil {α : TypeVec 0} (ps : TypeVec.Arrow α (TypeVec.repeat 0 Prop)) :

TypeVec.subtypeVal ps = TypeVec.nilFun

source

ink

theorem TypeVec.diag_sub_val {n : ℕ} {α : TypeVec n} :

TypeVec.comp (TypeVec.subtypeVal (TypeVec.repeatEq α)) TypeVec.diagSub = TypeVec.prod.diag

source

ink

theorem TypeVec.prod_id {n : ℕ} {α : TypeVec n} {β : TypeVec n} :

TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id

source

ink

theorem TypeVec.append_prod_appendFun {n : ℕ} {α : TypeVec n} {α' : TypeVec n} {β : TypeVec n} {β' : TypeVec n} {φ : Type u} {φ' : Type u} {ψ : Type u} {ψ' : Type u} {f₀ : TypeVec.Arrow α α'} {g₀ : TypeVec.Arrow β β'} {f₁ : φ → φ'} {g₁ : ψ → ψ'} :