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
append_fun f g : appends a function g to an n-tuple of functions
drop_fun f : drops the last function from an n+1-tuple
last_fun 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.
@[instance]
def
typevec.arrow.inhabited
{n : ℕ}
(α : typevec n)
(β : typevec n)
[Π (i : fin2 n), inhabited (β i)] :
Equations
- typevec.arrow.inhabited α β = {default := λ (_x : fin2 n) (_x_1 : α _x), inhabited.default (β _x)}
identity of arrow composition
Equations
- typevec.id = λ (i : fin2 n) (x : α i), x
@[simp]
theorem
typevec.id_comp
{n : ℕ}
{α : typevec n}
{β : typevec n}
(f : α.arrow β) :
typevec.comp typevec.id f = f
@[simp]
theorem
typevec.comp_id
{n : ℕ}
{α : typevec n}
{β : typevec n}
(f : α.arrow β) :
typevec.comp f typevec.id = f
theorem
typevec.comp_assoc
{n : ℕ}
{α : typevec n}
{β : typevec n}
{γ : typevec n}
{δ : typevec n}
(h : γ.arrow δ)
(g : β.arrow γ)
(f : α.arrow β) :
typevec.comp (typevec.comp h g) f = typevec.comp h (typevec.comp g f)
@[instance]
Equations
- typevec.last.inhabited α = {default := inhabited.default (α fin2.fz) _inst_1}
arrow in the category of 0-length vectors
Equations
- typevec.nil_fun = λ (i : fin2 0), i.elim0
theorem
typevec.eq_of_drop_last_eq
{n : ℕ}
{α : typevec (n + 1)}
{β : typevec (n + 1)}
{f g : α.arrow β} :
typevec.drop_fun f = typevec.drop_fun g → typevec.last_fun f = typevec.last_fun g → f = g
@[simp]
theorem
typevec.drop_fun_split_fun
{n : ℕ}
{α : typevec (n + 1)}
{α' : typevec (n + 1)}
(f : α.drop.arrow α'.drop)
(g : α.last → α'.last) :
typevec.drop_fun (typevec.split_fun f g) = f
turn an equality into an arrow
Equations
- typevec.arrow.mp h i = _.mp
turn an equality into an arrow, with reverse direction
Equations
- typevec.arrow.mpr h i = _.mpr
decompose a vector into its prefix appended with its last element
Equations
stitch two bits of a vector back together
Equations
@[simp]
theorem
typevec.last_fun_split_fun
{n : ℕ}
{α : typevec (n + 1)}
{α' : typevec (n + 1)}
(f : α.drop.arrow α'.drop)
(g : α.last → α'.last) :
typevec.last_fun (typevec.split_fun f g) = g
@[simp]
theorem
typevec.drop_fun_append_fun
{n : ℕ}
{α : typevec n}
{α' : typevec n}
{β : Type u_1}
{β' : Type u_2}
(f : α.arrow α')
(g : β → β') :
typevec.drop_fun (f ::: g) = f
@[simp]
theorem
typevec.last_fun_append_fun
{n : ℕ}
{α : typevec n}
{α' : typevec n}
{β : Type u_1}
{β' : Type u_2}
(f : α.arrow α')
(g : β → β') :
typevec.last_fun (f ::: g) = g
theorem
typevec.split_drop_fun_last_fun
{n : ℕ}
{α : typevec (n + 1)}
{α' : typevec (n + 1)}
(f : α.arrow α') :
typevec.split_fun (typevec.drop_fun f) (typevec.last_fun f) = f
theorem
typevec.split_fun_comp
{n : ℕ}
{α₀ : typevec (n + 1)}
{α₁ : typevec (n + 1)}
{α₂ : typevec (n + 1)}
(f₀ : α₀.drop.arrow α₁.drop)
(f₁ : α₁.drop.arrow α₂.drop)
(g₀ : α₀.last → α₁.last)
(g₁ : α₁.last → α₂.last) :
typevec.split_fun (typevec.comp f₁ f₀) (g₁ ∘ g₀) = typevec.comp (typevec.split_fun f₁ g₁) (typevec.split_fun f₀ g₀)
theorem
typevec.append_fun_comp_split_fun
{n : ℕ}
{α : typevec n}
{γ : typevec n}
{β : Type u_1}
{δ : Type u_2}
{ε : typevec (n + 1)}
(f₀ : ε.drop.arrow α)
(f₁ : α.arrow γ)
(g₀ : ε.last → β)
(g₁ : β → δ) :
typevec.comp (f₁ ::: g₁) (typevec.split_fun f₀ g₀) = typevec.split_fun (typevec.comp f₁ f₀) (g₁ ∘ g₀)
theorem
typevec.append_fun_comp
{n : ℕ}
{α₀ : typevec n}
{α₁ : typevec n}
{α₂ : typevec 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.append_fun_comp'
{n : ℕ}
{α₀ : typevec n}
{α₁ : typevec n}
{α₂ : typevec 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.nil_fun_comp
{α₀ : typevec 0}
(f₀ : α₀.arrow fin2.elim0) :
typevec.comp typevec.nil_fun f₀ = f₀
theorem
typevec.append_fun_comp_id
{n : ℕ}
{α : typevec n}
{β₀ β₁ β₂ : Type u_1}
(g₀ : β₀ → β₁)
(g₁ : β₁ → β₂) :
typevec.id ::: g₁ ∘ g₀ = typevec.comp (typevec.id ::: g₁) (typevec.id ::: g₀)
@[simp]
theorem
typevec.drop_fun_comp
{n : ℕ}
{α₀ : typevec (n + 1)}
{α₁ : typevec (n + 1)}
{α₂ : typevec (n + 1)}
(f₀ : α₀.arrow α₁)
(f₁ : α₁.arrow α₂) :
typevec.drop_fun (typevec.comp f₁ f₀) = typevec.comp (typevec.drop_fun f₁) (typevec.drop_fun f₀)
@[simp]
theorem
typevec.last_fun_comp
{n : ℕ}
{α₀ : typevec (n + 1)}
{α₁ : typevec (n + 1)}
{α₂ : typevec (n + 1)}
(f₀ : α₀.arrow α₁)
(f₁ : α₁.arrow α₂) :
typevec.last_fun (typevec.comp f₁ f₀) = typevec.last_fun f₁ ∘ typevec.last_fun f₀
theorem
typevec.append_fun_aux
{n : ℕ}
{α : typevec n}
{α' : typevec n}
{β : Type u_1}
{β' : Type u_2}
(f : (α ::: β).arrow (α' ::: β')) :
typevec.drop_fun f ::: typevec.last_fun f = f
@[instance]
Equations
simp set for the manipulation of typevec and arrow expressions
cases distinction for 0-length type vector
Equations
- typevec.cases_nil f = λ (v : typevec 0), cast _ f
def
typevec.typevec_cases_nil₃
{β : Π (v : typevec 0) (v' : typevec 0), v.arrow v' → Sort u_3}
(f : β fin2.elim0 fin2.elim0 typevec.nil_fun)
(v : typevec 0)
(v' : typevec 0)
(fs : v.arrow v') :
β v v' fs
cases distinction for an arrow in the category of 0-length type vectors
def
typevec.typevec_cases_cons₃
(n : ℕ)
{β : Π (v : typevec (n + 1)) (v' : typevec (n + 1)), v.arrow v' → Sort u_3}
(F : Π (t : Type u_1) (t' : Type u_2) (f : t → t') (v : typevec n) (v' : typevec n) (fs : v.arrow v'), β (v ::: t) (v' ::: t') (fs ::: f))
(v : typevec (n + 1))
(v' : typevec (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.typevec_cases_nil₂
{β : typevec.arrow fin2.elim0 fin2.elim0 → Sort u_3}
(f : β typevec.nil_fun)
(f_1 : typevec.arrow fin2.elim0 fin2.elim0) :
β f_1
specialized cases distinction for an arrow in the category of 0-length type vectors
Equations
- typevec.typevec_cases_nil₂ f = λ (g : typevec.arrow fin2.elim0 fin2.elim0), _.mpr f
def
typevec.typevec_cases_cons₂
(n : ℕ)
(t : Type u_1)
(t' : Type u_2)
(v : typevec n)
(v' : typevec 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.typevec_cases_cons₂ n t t' v v' F = λ (fs : (v ::: t).arrow (v' ::: t')), _.mpr (F (typevec.last_fun fs) (typevec.drop_fun fs))
theorem
typevec.typevec_cases_nil₂_append_fun
{β : typevec.arrow fin2.elim0 fin2.elim0 → Sort u_3}
(f : β typevec.nil_fun) :
theorem
typevec.typevec_cases_cons₂_append_fun
(n : ℕ)
(t : Type u_1)
(t' : Type u_2)
(v : typevec n)
(v' : typevec 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') :
typevec.typevec_cases_cons₂ n t t' v v' F (fs ::: f) = F f fs
def
typevec.rel_last
{n : ℕ}
(α : typevec n)
{β γ : Type u_1}
(r : β → γ → Prop)
⦃i : fin2 (n + 1)⦄ :
rel_last α r x y says that p the last elements of x y : α.append1 β are related by r and all the other elements are equal.
repeat n t is a n-length type vector that contains n occurences of t
Equations
- typevec.repeat i.succ t = typevec.repeat i t ::: t
- typevec.repeat 0 t = fin2.elim0
const x α is an arrow that ignores its source and constructs a typevec that
contains nothing but x
Equations
- typevec.const x α i.fs = typevec.const x α.drop i
- typevec.const x α fin2.fz = λ (_x : α fin2.fz), x
vector of equality on a product of vectors
Equations
theorem
typevec.const_append1
{β : Type u_1}
{γ : Type u_2}
(x : γ)
{n : ℕ}
(α : typevec n) :
typevec.const x (α ::: β) = typevec.const x α ::: λ (_x : β), x
theorem
typevec.repeat_eq_append1
{β : Type u_1}
{n : ℕ}
(α : typevec n) :
(α ::: β).repeat_eq = typevec.split_fun α.repeat_eq (function.uncurry eq)
def
typevec.pred_last'
{n : ℕ}
(α : typevec n)
{β : Type u_1} :
(β → Prop) → (α ::: β).arrow (typevec.repeat (n + 1) Prop)
predicate on a type vector to constrain only the last object
Equations
- α.pred_last' p = typevec.split_fun (typevec.const true α) p
predicate on the product of two type vectors to constrain only their last object
Equations
- α.rel_last' p = typevec.split_fun α.repeat_eq (function.uncurry p)
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]
def
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
def
typevec.drop_repeat
(α : Type u_1)
{n : ℕ} :
(typevec.repeat n.succ α).drop.arrow (typevec.repeat n α)
arrow to remove one element of a repeat vector
Equations
projection for a repeat vector
Equations
theorem
typevec.const_iff_true
{n : ℕ}
{α : typevec n}
{i : fin2 n}
{x : α i}
{p : Prop} :
typevec.of_repeat (typevec.const p α i x) ↔ p
left projection of a prod vector
Equations
right projection of a prod vector
Equations
introduce a product where both components are the same
Equations
- typevec.prod.diag i.fs x = typevec.prod.diag i x
- typevec.prod.diag fin2.fz x = (x, x)
constructor for prod
Equations
prod is functorial
Equations
- typevec.prod.map x y i.fs a = typevec.prod.map (typevec.drop_fun x) (typevec.drop_fun y) i a
- typevec.prod.map x y fin2.fz a = (x fin2.fz a.fst, y fin2.fz a.snd)
theorem
typevec.repeat_eq_iff_eq
{n : ℕ}
{α : typevec n}
{i : fin2 n}
{x y : α i} :
typevec.of_repeat (α.repeat_eq i (typevec.prod.mk i x y)) ↔ x = y
given a predicate vector p over vector α, subtype_ p is the type of vectors
that contain an α that satisfies p
Equations
- typevec.subtype_ p i.fs = typevec.subtype_ (typevec.drop_fun p) i
- typevec.subtype_ p fin2.fz = {x // p fin2.fz x}
def
typevec.subtype_val
{n : ℕ}
{α : typevec n}
(p : α.arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow α
projection on subtype_
Equations
def
typevec.to_subtype
{n : ℕ}
{α : typevec n}
(p : α.arrow (typevec.repeat n Prop)) :
typevec.arrow (λ (i : fin2 n), {x // typevec.of_repeat (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.to_subtype p i.fs x = typevec.to_subtype (typevec.drop_fun p) i x
- typevec.to_subtype p fin2.fz x = x
def
typevec.of_subtype
{n : ℕ}
{α : typevec n}
(p : α.arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i x)})
arrow that rearranges the type of subtype_ to turn a vector of subtypes
into a subtype of vector
Equations
- typevec.of_subtype p i.fs x = typevec.of_subtype (typevec.drop_fun p) i x
- typevec.of_subtype p fin2.fz x = x
def
typevec.to_subtype'
{n : ℕ}
{α : typevec n}
(p : (α.prod α).arrow (typevec.repeat n Prop)) :
typevec.arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i (typevec.prod.mk i x.fst x.snd))}) (typevec.subtype_ p)
similar to to_subtype adapted to relations (i.e. predicate on product)
Equations
- typevec.to_subtype' p i.fs x = typevec.to_subtype' (typevec.drop_fun p) i x
- typevec.to_subtype' p fin2.fz x = ⟨x.val, _⟩
def
typevec.of_subtype'
{n : ℕ}
{α : typevec n}
(p : (α.prod α).arrow (typevec.repeat n Prop)) :
(typevec.subtype_ p).arrow (λ (i : fin2 n), {x // typevec.of_repeat (p i (typevec.prod.mk i x.fst x.snd))})
similar to of_subtype adapted to relations (i.e. predicate on product)
Equations
- typevec.of_subtype' p i.fs x = typevec.of_subtype' (typevec.drop_fun p) i x
- typevec.of_subtype' p fin2.fz x = ⟨x.val, _⟩
similar to diag but the target vector is a subtype_
guaranteeing the equality of the components
Equations
- typevec.diag_sub i.fs x = typevec.diag_sub i x
- typevec.diag_sub fin2.fz x = ⟨(x, x), _⟩
theorem
typevec.append_prod_append_fun
{n : ℕ}
{α α' β β' : typevec n}
{φ φ' ψ ψ' : 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]
@[simp]
theorem
typevec.drop_fun_subtype_val
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
@[simp]
theorem
typevec.last_fun_subtype_val
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
@[simp]
theorem
typevec.drop_fun_to_subtype
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
typevec.drop_fun (typevec.to_subtype p) = typevec.to_subtype (λ (i : fin2 n) (x : α i.fs), p i.fs x)
@[simp]
theorem
typevec.last_fun_to_subtype
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
@[simp]
theorem
typevec.drop_fun_of_subtype
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
@[simp]
theorem
typevec.last_fun_of_subtype
{n : ℕ}
{α : typevec (n + 1)}
(p : α.arrow (typevec.repeat (n + 1) Prop)) :
@[simp]
theorem
typevec.drop_fun_rel_last
{n : ℕ}
{α : typevec n}
{β : Type u_1}
(R : β → β → Prop) :
typevec.drop_fun (α.rel_last' R) = α.repeat_eq
@[simp]
theorem
typevec.drop_fun_prod
{n : ℕ}
{α α' β β' : typevec (n + 1)}
(f : α.arrow β)
(f' : α'.arrow β') :
typevec.drop_fun (typevec.prod.map f f') = typevec.prod.map (typevec.drop_fun f) (typevec.drop_fun f')
@[simp]
theorem
typevec.last_fun_prod
{n : ℕ}
{α α' β β' : typevec (n + 1)}
(f : α.arrow β)
(f' : α'.arrow β') :
typevec.last_fun (typevec.prod.map f f') = prod.map (typevec.last_fun f) (typevec.last_fun f')
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
typevec.to_subtype_of_subtype
{n : ℕ}
{α : typevec n}
(p : α.arrow (typevec.repeat n Prop)) :
typevec.comp (typevec.to_subtype p) (typevec.of_subtype (λ (i : fin2 n) (x : α i), p i x)) = typevec.id
@[simp]
theorem
typevec.to_subtype_of_subtype_assoc
{n : ℕ}
{α : typevec n}
{β : typevec n}
(p : α.arrow (typevec.repeat n Prop))
(f : β.arrow (typevec.subtype_ p)) :
typevec.comp (typevec.to_subtype p) (typevec.comp (typevec.of_subtype (λ (i : fin2 n) (x : α i), p i x)) f) = f