# 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
Instances For
instance instInhabitedTypeVec {n : } :
Equations
def TypeVec.Arrow {n : } (α : ) (β : ) :
Type (max u_1 u_2)

arrow in the category of TypeVec

Equations
• α.Arrow β = ((i : Fin2 n) → α iβ i)
Instances For

arrow in the category of TypeVec

Equations
Instances For
theorem TypeVec.Arrow.ext_iff {n : } {α : } {β : } {f : α.Arrow β} {g : α.Arrow β} :
f = g ∀ (i : Fin2 n), f i = g i
theorem TypeVec.Arrow.ext {n : } {α : } {β : } (f : α.Arrow β) (g : α.Arrow β) :
(∀ (i : Fin2 n), f i = g i)f = g

Extensionality for arrows

instance TypeVec.Arrow.inhabited {n : } (α : ) (β : ) [(i : Fin2 n) → Inhabited (β i)] :
Inhabited (α.Arrow β)
Equations
• = { default := fun (x : Fin2 n) (x_1 : α x) => default }
def TypeVec.id {n : } {α : } :
α.Arrow α

identity of arrow composition

Equations
Instances For
def TypeVec.comp {n : } {α : } {β : } {γ : } (g : β.Arrow γ) (f : α.Arrow β) :
α.Arrow γ

arrow composition in the category of TypeVec

Equations
Instances For

arrow composition in the category of TypeVec

Equations
Instances For
@[simp]
theorem TypeVec.id_comp {n : } {α : } {β : } (f : α.Arrow β) :
TypeVec.comp TypeVec.id f = f
@[simp]
theorem TypeVec.comp_id {n : } {α : } {β : } (f : α.Arrow β) :
TypeVec.comp f TypeVec.id = f
theorem TypeVec.comp_assoc {n : } {α : } {β : } {γ : } {δ : } (h : γ.Arrow δ) (g : β.Arrow γ) (f : α.Arrow β) :
def TypeVec.append1 {n : } (α : ) (β : Type u_1) :

Support for extending a TypeVec by one element.

Equations
• (α ::: β) i.fs = α i
• (α ::: β) Fin2.fz = β
Instances For

Support for extending a TypeVec by one element.

Equations
Instances For
def TypeVec.drop {n : } (α : TypeVec.{u} (n + 1)) :

retain only a n-length prefix of the argument

Equations
• α.drop i = α i.fs
Instances For
def TypeVec.last {n : } (α : TypeVec.{u} (n + 1)) :

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

Equations
• α.last = α Fin2.fz
Instances For
instance TypeVec.last.inhabited {n : } (α : TypeVec.{u_1} (n + 1)) [Inhabited (α Fin2.fz)] :
Inhabited α.last
Equations
• = { default := let_fun this := default; this }
theorem TypeVec.drop_append1 {n : } {α : } {β : Type u_1} {i : Fin2 n} :
(α ::: β).drop i = α i
@[simp]
theorem TypeVec.drop_append1' {n : } {α : } {β : Type u_1} :
(α ::: β).drop = α
theorem TypeVec.last_append1 {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 : (α : ) → (β : Type u_1) → C (α ::: β)) (γ : TypeVec.{u_1} (n + 1)) :
C γ

cases on (n+1)-length vectors

Equations
• = .mpr (H γ.drop γ.last)
Instances For
@[simp]
theorem TypeVec.append1_cases_append1 {n : } {C : TypeVec.{u_1} (n + 1)Sort u} (H : (α : ) → (β : Type u_1) → C (α ::: β)) (α : ) (β : Type u_1) :
TypeVec.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
Instances For
def TypeVec.appendFun {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
Instances For

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

Equations
Instances For
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
• = f i.fs
Instances For
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
• = f Fin2.fz
Instances For
def TypeVec.nilFun {α : } {β : } :
α.Arrow β

arrow in the category of 0-length vectors

Equations
• = i.elim0
Instances For
theorem TypeVec.eq_of_drop_last_eq {n : } {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} {f : α.Arrow β} {g : α.Arrow β} (h₀ : ) (h₁ : ) :
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) :
= f
def TypeVec.Arrow.mp {n : } {α : } {β : } (h : α = β) :
α.Arrow β

turn an equality into an arrow

Equations
• = .mp
Instances For
def TypeVec.Arrow.mpr {n : } {α : } {β : } (h : α = β) :
β.Arrow α

turn an equality into an arrow, with reverse direction

Equations
• = .mpr
Instances For
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 =
Instances For
def TypeVec.fromAppend1DropLast {n : } {α : TypeVec.{u_1} (n + 1)} :
(α.drop ::: α.last).Arrow α

stitch two bits of a vector back together

Equations
• TypeVec.fromAppend1DropLast =
Instances For
@[simp]
theorem TypeVec.lastFun_splitFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.lastα'.last) :
= g
@[simp]
theorem TypeVec.dropFun_appendFun {n : } {α : } {α' : } {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : ββ') :
@[simp]
theorem TypeVec.lastFun_appendFun {n : } {α : } {α' : } {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : ββ') :
theorem TypeVec.split_dropFun_lastFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.Arrow α') :
theorem TypeVec.splitFun_inj {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} {f : α.drop.Arrow α'.drop} {f' : α.drop.Arrow α'.drop} {g : α.lastα'.last} {g' : α.lastα'.last} (H : = TypeVec.splitFun f' g') :
f = f' g = g'
theorem TypeVec.appendFun_inj {n : } {α : } {α' : } {β : Type u_1} {β' : Type u_2} {f : α.Arrow α'} {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) :
TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ g₀) = TypeVec.comp (TypeVec.splitFun f₁ g₁) (TypeVec.splitFun f₀ g₀)
theorem TypeVec.appendFun_comp_splitFun {n : } {α : } {γ : } {β : Type u_1} {δ : Type u_2} {ε : TypeVec.{u_3} (n + 1)} (f₀ : ε.drop.Arrow α) (f₁ : α.Arrow γ) (g₀ : ε.lastβ) (g₁ : βδ) :
TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ g₀)
theorem TypeVec.appendFun_comp {n : } {α₀ : } {α₁ : } {α₂ : } {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀β₁) (g₁ : β₁β₂) :
(TypeVec.comp f₁ f₀ ::: g₁ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)
theorem TypeVec.appendFun_comp' {n : } {α₀ : } {α₁ : } {α₂ : } {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀β₁) (g₁ : β₁β₂) :
TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀) = (TypeVec.comp f₁ f₀ ::: g₁ g₀)
theorem TypeVec.nilFun_comp {α₀ : } (f₀ : α₀.Arrow Fin2.elim0) :
TypeVec.comp TypeVec.nilFun f₀ = f₀
theorem TypeVec.appendFun_comp_id {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₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) :
@[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 α₂) :
theorem TypeVec.appendFun_aux {n : } {α : } {α' : } {β : Type u_1} {β' : Type u_2} (f : (α ::: β).Arrow (α' ::: β')) :
= f
theorem TypeVec.appendFun_id_id {n : } {α : } {β : Type u_1} :
(TypeVec.id ::: id) = TypeVec.id
Equations
def TypeVec.casesNil {β : Sort u_1} (f : β Fin2.elim0) (v : ) :
β v

cases distinction for 0-length type vector

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

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

Equations
• = cast (f v.last v.drop)
Instances For
theorem TypeVec.casesNil_append1 {β : 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 : ) → β (v ::: t)) (v : ) (α : Type u_2) :
TypeVec.casesCons n f (v ::: α) = f α v
def TypeVec.typevecCasesNil₃ {β : (v : ) → (v' : ) → v.Arrow v'Sort u_1} (f : β Fin2.elim0 Fin2.elim0 TypeVec.nilFun) (v : ) (v' : ) (fs : v.Arrow v') :
β v v' fs

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

Equations
Instances For
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 : tt') → (v : ) → (v' : ) → (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.
Instances For
def TypeVec.typevecCasesNil₂ {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0Sort 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
• = .mpr f
Instances For
def TypeVec.typevecCasesCons₂ (n : ) (t : Type u_1) (t' : Type u_2) (v : ) (v' : ) {β : (v ::: t).Arrow (v' ::: t')Sort u_3} (F : (f : tt') → (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
Instances For
theorem TypeVec.typevecCasesNil₂_appendFun {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0Sort 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 : ) (v' : ) {β : (v ::: t).Arrow (v' ::: t')Sort u_3} (F : (f : tt') → (fs : v.Arrow v') → β (fs ::: f)) (f : tt') (fs : v.Arrow v') :
TypeVec.typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs
def TypeVec.PredLast {n : } (α : ) {β : Type u_1} (p : βProp) ⦃i : Fin2 (n + 1) :
(α ::: β) iProp

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

Equations
• α.PredLast p = fun (x : (α ::: β) i.fs) => True
• α.PredLast p = p
Instances For
def TypeVec.RelLast {n : } (α : ) {β : Type u} {γ : Type u} (r : βγProp) ⦃i : Fin2 (n + 1) :
(α ::: β) i(α ::: γ) iProp

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
Instances For
def TypeVec.repeat (n : ) :
Type u_1 →

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

Equations
Instances For
def TypeVec.prod {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)
Instances For

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

Equations
Instances For
def TypeVec.const {β : Type u_1} (x : β) {n : } (α : ) :
α.Arrow (TypeVec.repeat n β)

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

Equations
Instances For
def TypeVec.repeatEq {n : } (α : ) :
(α.prod α).Arrow

vector of equality on a product of vectors

Equations
• x_2.repeatEq = TypeVec.nilFun
• α.repeatEq = (α.drop.repeatEq ::: )
Instances For
theorem TypeVec.const_append1 {β : Type u_1} {γ : Type u_2} (x : γ) {n : } (α : ) :
TypeVec.const x (α ::: β) = ( ::: fun (x_1 : β) => x)
theorem TypeVec.eq_nilFun {α : } {β : } (f : α.Arrow β) :
f = TypeVec.nilFun
theorem TypeVec.id_eq_nilFun {α : } :
TypeVec.id = TypeVec.nilFun
theorem TypeVec.const_nil {β : Type u_1} (x : β) (α : ) :
= TypeVec.nilFun
theorem TypeVec.repeat_eq_append1 {β : Type u_1} {n : } (α : ) :
(α ::: β).repeatEq = TypeVec.splitFun α.repeatEq (Function.uncurry Eq)
theorem TypeVec.repeat_eq_nil (α : ) :
α.repeatEq = TypeVec.nilFun
def TypeVec.PredLast' {n : } (α : ) {β : Type u_1} (p : βProp) :
(α ::: β).Arrow (TypeVec.repeat (n + 1) Prop)

predicate on a type vector to constrain only the last object

Equations
• α.PredLast' p =
Instances For
def TypeVec.RelLast' {n : } (α : ) {β : Type u_1} (p : ββProp) :
((α ::: β).prod (α ::: β)).Arrow (TypeVec.repeat (n + 1) Prop)

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

Equations
Instances For
def TypeVec.Curry {n : } (F : TypeVec.{u} (n + 1)Type u_1) (α : Type u) (β : ) :
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
Instances For
instance TypeVec.Curry.inhabited {n : } (F : TypeVec.{u} (n + 1)Type u_1) (α : Type u) (β : ) [I : Inhabited (F (β ::: α))] :
Equations
def TypeVec.dropRepeat (α : Type u_1) {n : } :
(TypeVec.repeat n.succ α).drop.Arrow (TypeVec.repeat n α)

arrow to remove one element of a repeat vector

Equations
Instances For
def TypeVec.ofRepeat {α : Type u_1} {n : } {i : Fin2 n} :
α

projection for a repeat vector

Equations
• TypeVec.ofRepeat = fun (a : α) => a
• TypeVec.ofRepeat = TypeVec.ofRepeat
Instances For
theorem TypeVec.const_iff_true {n : } {α : } {i : Fin2 n} {x : α i} {p : Prop} :
def TypeVec.prod.fst {n : } {α : } {β : } :
(α.prod β).Arrow α

left projection of a prod vector

Equations
Instances For
def TypeVec.prod.snd {n : } {α : } {β : } :
(α.prod β).Arrow β

right projection of a prod vector

Equations
Instances For
def TypeVec.prod.diag {n : } {α : } :
α.Arrow (α.prod α)

introduce a product where both components are the same

Equations
Instances For
def TypeVec.prod.mk {n : } {α : } {β : } (i : Fin2 n) :
α iβ iα.prod β i

constructor for prod

Equations
Instances For
@[simp]
theorem TypeVec.prod_fst_mk {n : } {α : } {β : } (i : Fin2 n) (a : α i) (b : β i) :
@[simp]
theorem TypeVec.prod_snd_mk {n : } {α : } {β : } (i : Fin2 n) (a : α i) (b : β i) :
def TypeVec.prod.map {n : } {α : } {α' : } {β : } {β' : } :
α.Arrow βα'.Arrow β'(α.prod α').Arrow (β.prod β')

prod is functorial

Equations
Instances For

prod is functorial

Equations
Instances For
theorem TypeVec.fst_prod_mk {n : } {α : } {α' : } {β : } {β' : } (f : α.Arrow β) (g : α'.Arrow β') :
TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst
theorem TypeVec.snd_prod_mk {n : } {α : } {α' : } {β : } {β' : } (f : α.Arrow β) (g : α'.Arrow β') :
TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd
theorem TypeVec.fst_diag {n : } {α : } :
TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id
theorem TypeVec.snd_diag {n : } {α : } :
TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id
theorem TypeVec.repeatEq_iff_eq {n : } {α : } {i : Fin2 n} {x : α i} {y : α i} :
TypeVec.ofRepeat (α.repeatEq i (TypeVec.prod.mk i x y)) x = y
def TypeVec.Subtype_ {n : } {α : } :
α.Arrow

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

Equations
Instances For
def TypeVec.subtypeVal {n : } {α : } (p : α.Arrow ) :
.Arrow α

projection on Subtype_

Equations
Instances For
def TypeVec.toSubtype {n : } {α : } (p : α.Arrow ) :
TypeVec.Arrow (fun (i : Fin2 n) => { x : α i // TypeVec.ofRepeat (p i x) })

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

Equations
Instances For
def TypeVec.ofSubtype {n : } {α : } (p : α.Arrow ) :
.Arrow 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
Instances For
def TypeVec.toSubtype' {n : } {α : } (p : (α.prod α).Arrow ) :
TypeVec.Arrow (fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) })

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

Equations
Instances For
def TypeVec.ofSubtype' {n : } {α : } (p : (α.prod α).Arrow ) :
.Arrow fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) }

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

Equations
Instances For
def TypeVec.diagSub {n : } {α : } :
α.Arrow (TypeVec.Subtype_ α.repeatEq)

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

Equations
Instances For
theorem TypeVec.subtypeVal_nil {α : } (ps : α.Arrow ) :
= TypeVec.nilFun
theorem TypeVec.diag_sub_val {n : } {α : } :
TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
theorem TypeVec.prod_id {n : } {α : } {β : } :
TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
theorem TypeVec.append_prod_appendFun {n : } {α : } {α' : } {β : } {β' : } {φ : Type u} {φ' : Type u} {ψ : Type u} {ψ' : Type u} {f₀ : α.Arrow α'} {g₀ : β.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 : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
@[simp]
theorem TypeVec.lastFun_subtypeVal {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
= Subtype.val
@[simp]
theorem TypeVec.dropFun_toSubtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
= TypeVec.toSubtype fun (i : Fin2 n) => p i.fs
@[simp]
theorem TypeVec.lastFun_toSubtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
@[simp]
theorem TypeVec.dropFun_of_subtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
@[simp]
theorem TypeVec.lastFun_of_subtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
@[simp]
theorem TypeVec.dropFun_RelLast' {n : } {α : } {β : Type u_1} (R : ββProp) :
TypeVec.dropFun (α.RelLast' R) = α.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 : α.Arrow β) (f' : α'.Arrow β') :
@[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 : α.Arrow β) (f' : α'.Arrow β') :
=
@[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.prod.map TypeVec.id TypeVec.id = TypeVec.id
@[simp]
theorem TypeVec.subtypeVal_diagSub {n : } {α : } :
TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
@[simp]
theorem TypeVec.toSubtype_of_subtype {n : } {α : } (p : α.Arrow ) :
= TypeVec.id
@[simp]
theorem TypeVec.subtypeVal_toSubtype {n : } {α : } (p : α.Arrow ) :
= fun (x : Fin2 n) => Subtype.val
@[simp]
theorem TypeVec.toSubtype_of_subtype_assoc {n : } {α : } {β : } (p : α.Arrow ) (f : β.Arrow ) :
= f
@[simp]
theorem TypeVec.toSubtype'_of_subtype' {n : } {α : } (r : (α.prod α).Arrow ) :
= TypeVec.id
theorem TypeVec.subtypeVal_toSubtype' {n : } {α : } (r : (α.prod α).Arrow ) :
= fun (i : Fin2 n) (x : { x : α i × α i // TypeVec.ofRepeat (r i (TypeVec.prod.mk i x.1 x.2)) }) => TypeVec.prod.mk i (↑x).1 (↑x).2