# Documentation

Mathlib.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 MvFunctor {n : } (F : Type u_1) : Type (max u_1 (u_2 + 1)) • map : {α β : } → F αF β Multivariate map, if f : α ⟹ β and x : F α then f <$$> x : F β.

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

Instances

Multivariate map, if f : α ⟹ β and x : F α then f <> x : F β

Instances For
def MvFunctor.LiftP {n : } {F : Type v} [] {α : } (P : (i : Fin2 n) → α iProp) (x : F α) :

predicate lifting over multivariate functors

Instances For
def MvFunctor.LiftR {n : } {F : Type v} [] {α : } (R : {i : Fin2 n} → α iα iProp) (x : F α) (y : F α) :

relational lifting over multivariate functors

Instances For
def MvFunctor.supp {n : } {F : Type v} [] {α : } (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

Instances For
theorem MvFunctor.of_mem_supp {n : } {F : Type v} [] {α : } {x : F α} {P : i : Fin2 n⦄ → α iProp} (h : ) (i : Fin2 n) (y : α i) :
y P i y
class LawfulMvFunctor {n : } (F : Type u_1) [] :
• id_map : ∀ {α : } (x : F α), MvFunctor.map TypeVec.id x = x

map preserved identities, i.e., maps identity on α to identity on F α

• comp_map : ∀ {α β γ : } (g : ) (h : ) (x : F α), MvFunctor.map () x = MvFunctor.map h ()

map preserves compositions

laws for MvFunctor

Instances
def MvFunctor.LiftP' {n : } {α : } {F : Type v} [] (P : ) :
F αProp

adapt MvFunctor.LiftP to accept predicates as arrows

Instances For
def MvFunctor.LiftR' {n : } {α : } {F : Type v} [] (R : TypeVec.Arrow () ()) :
F αF αProp

adapt MvFunctor.LiftR to accept relations as arrows

Instances For
@[simp]
theorem MvFunctor.id_map {n : } {α : } {F : Type v} [] [] (x : F α) :
MvFunctor.map TypeVec.id x = x
@[simp]
theorem MvFunctor.id_map' {n : } {α : } {F : Type v} [] [] (x : F α) :
MvFunctor.map (fun _i a => a) x = x
theorem MvFunctor.map_map {n : } {α : } {β : } {γ : } {F : Type v} [] [] (g : ) (h : ) (x : F α) :
theorem MvFunctor.exists_iff_exists_of_mono {n : } {α : } {β : } (F : Type v) [] [] {P : F αProp} {q : F βProp} (f : ) (g : ) (h₀ : = TypeVec.id) (h₁ : ∀ (u : F α), P u q ()) :
(u, P u) u, q u
theorem MvFunctor.LiftP_def {n : } {α : } {F : Type v} [] (P : ) [] (x : F α) :
u, = x
theorem MvFunctor.LiftR_def {n : } {α : } {F : Type v} [] (R : TypeVec.Arrow () ()) [] (x : F α) (y : F α) :
u, MvFunctor.map (TypeVec.comp TypeVec.prod.fst ()) u = x MvFunctor.map (TypeVec.comp TypeVec.prod.snd ()) u = y
theorem MvFunctor.LiftP_PredLast_iff {n : } {F : TypeVec (n + 1)Type u_1} [] [] {α : } {β : Type u} (P : βProp) (x : F (α ::: β)) :
theorem MvFunctor.LiftR_RelLast_iff {n : } {F : TypeVec (n + 1)Type u_1} [] [] {α : } {β : Type u} (rr : ββProp) (x : F (α ::: β)) (y : F (α ::: β)) :
MvFunctor.LiftR' () x y MvFunctor.LiftR (fun {i} => ) x y