mathlib documentation

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 : } :
(typevec nType u_2)Type (max (u_1+1) u_2)
  • map : Π {α β : typevec n}, α βF αF β

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

Instances
def mvfunctor.liftp {n : } {F : typevec nType v} [mvfunctor F] {α : typevec n} :
(Π (i : fin2 n), α i → Prop)F α → Prop

predicate lifting over multivariate functors

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

relational lifting over multivariate functors

Equations
def mvfunctor.supp {n : } {F : typevec nType 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
theorem mvfunctor.of_mem_supp {n : } {F : typevec nType v} [mvfunctor F] {α : typevec n} {x : F α} {p : Π ⦃i : fin2 n⦄, α i → Prop} (h : mvfunctor.liftp p x) (i : fin2 n) (y : α i) :
y mvfunctor.supp x ip y

@[class]
structure is_lawful_mvfunctor {n : } (F : typevec nType u_2) [mvfunctor F] :
Prop

laws for mvfunctor

Instances
def mvfunctor.liftp' {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] :
α typevec.repeat n PropF α → Prop

adapt mvfunctor.liftp to accept predicates as arrows

Equations
def mvfunctor.liftr' {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] :
α α typevec.repeat n PropF αF α → Prop

adapt mvfunctor.liftp to accept relations as arrows

Equations
@[simp]
theorem mvfunctor.id_map {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] [is_lawful_mvfunctor F] (x : F α) :

@[simp]
theorem mvfunctor.id_map' {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] [is_lawful_mvfunctor F] (x : F α) :
(λ (i : fin2 n) (a : α i), a) <$$> x = x

theorem mvfunctor.map_map {n : } {α β γ : typevec n} {F : typevec nType v} [mvfunctor F] [is_lawful_mvfunctor F] (g : α β) (h : β γ) (x : F α) :
h <$$> g <$$> x = (h g) <$$> x

theorem mvfunctor.exists_iff_exists_of_mono {n : } {α β : typevec n} (F : typevec nType v) [mvfunctor F] [is_lawful_mvfunctor F] {p : F α → Prop} {q : F β → Prop} (f : α β) (g : β α) :
f g = typevec.id(∀ (u : F α), p u q (f <$$> u))((∃ (u : F α), p u) ∃ (u : F β), q u)

theorem mvfunctor.liftp_def {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] (p : α typevec.repeat n Prop) [is_lawful_mvfunctor F] (x : F α) :

theorem mvfunctor.liftr_def {n : } {α : typevec n} {F : typevec nType v} [mvfunctor F] (r : α α typevec.repeat n Prop) [is_lawful_mvfunctor F] (x y : F α) :

theorem mvfunctor.liftp_last_pred_iff {n : } {F : typevec (n + 1)Type u_1} [mvfunctor F] [is_lawful_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] [is_lawful_mvfunctor F] {α : typevec n} {β : Type u} (rr : β → β → Prop) (x y : F ::: β)) :