# mathlibdocumentation

control.functor.multivariate

Functors between the category of tuples of types, and the category Type

Features:

mvfunctor n : the type class of multivariate functors f <> x : notation for map

@[class]
structure mvfunctor {n : } (F : Type u_2) :
Type (max (u_1+1) u_2)
• map : Π {α β : typevec n}, α.arrow βF αF β

multivariate functors, i.e. functor between the category of type vectors and the category of Type

Instances of this typeclass
Instances of other typeclasses for mvfunctor
• mvfunctor.has_sizeof_inst
def mvfunctor.liftp {n : } {F : Type v} [mvfunctor F] {α : typevec n} (p : Π (i : fin2 n), α i → Prop) (x : F α) :
Prop

predicate lifting over multivariate functors

Equations
def mvfunctor.liftr {n : } {F : Type v} [mvfunctor F] {α : typevec n} (r : Π {i : fin2 n}, α iα i → Prop) (x y : F α) :
Prop

relational lifting over multivariate functors

Equations
def mvfunctor.supp {n : } {F : Type v} [mvfunctor F] {α : typevec n} (x : F α) (i : fin2 n) :
set (α i)

given x : F α and a projection i of type vector α, supp x i is the set of α.i contained in x

Equations
• = {y : α i | ∀ ⦃p : Π (i : fin2 n), α i → Prop⦄, p i y}
theorem mvfunctor.of_mem_supp {n : } {F : Type v} [mvfunctor F] {α : typevec n} {x : F α} {p : Π ⦃i : fin2 n⦄, α i → Prop} (h : x) (i : fin2 n) (y : α i) (H : y ) :
p y
@[class]
structure is_lawful_mvfunctor {n : } (F : Type u_2) [mvfunctor F] :
Prop
• id_map : ∀ {α : typevec n} (x : F α),
• comp_map : ∀ {α β γ : typevec n} (g : α.arrow β) (h : β.arrow γ) (x : F α), x = x)

laws for mvfunctor

Instances of this typeclass
def mvfunctor.liftp' {n : } {α : typevec n} {F : Type v} [mvfunctor F] (p : α.arrow Prop)) :
F α → Prop

adapt mvfunctor.liftp to accept predicates as arrows

Equations
def mvfunctor.liftr' {n : } {α : typevec n} {F : Type v} [mvfunctor F] (r : (α.prod α).arrow Prop)) :
F αF α → Prop

adapt mvfunctor.liftp to accept relations as arrows

Equations
@[simp]
theorem mvfunctor.id_map {n : } {α : typevec n} {F : Type v} [mvfunctor F] (x : F α) :
@[simp]
theorem mvfunctor.id_map' {n : } {α : typevec n} {F : Type v} [mvfunctor F] (x : F α) :
mvfunctor.map (λ (i : fin2 n) (a : α i), a) x = x
theorem mvfunctor.map_map {n : } {α β γ : typevec n} {F : Type v} [mvfunctor F] (g : α.arrow β) (h : β.arrow γ) (x : F α) :
x) = x
theorem mvfunctor.exists_iff_exists_of_mono {n : } {α β : typevec n} (F : Type v) [mvfunctor F] {p : F α → Prop} {q : F β → Prop} (f : α.arrow β) (g : β.arrow α) (h₀ : g = typevec.id) (h₁ : ∀ (u : F α), p u q u)) :
(∃ (u : F α), p u) ∃ (u : F β), q u
theorem mvfunctor.liftp_def {n : } {α : typevec n} {F : Type v} [mvfunctor F] (p : α.arrow Prop)) (x : F α) :
∃ (u : F (typevec.subtype_ p)),
theorem mvfunctor.liftr_def {n : } {α : typevec n} {F : Type v} [mvfunctor F] (r : (α.prod α).arrow Prop)) (x y : F α) :
y ∃ (u : F (typevec.subtype_ r)),
theorem mvfunctor.liftp_last_pred_iff {n : } {F : typevec (n + 1)Type u_1} [mvfunctor F] {α : typevec n} {β : Type u} (p : β → Prop) (x : F ::: β)) :
theorem mvfunctor.liftr_last_rel_iff {n : } {F : typevec (n + 1)Type u_1} [mvfunctor F] {α : typevec n} {β : Type u} (rr : β → β → Prop) (x y : F ::: β)) :