# 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)) Multivariate functors, i.e. functor between the category of type vectors and the category of Type • map : {α β : } → α.Arrow βF αF β Multivariate map, if f : α ⟹ β and x : F α then f <$$> x : F β.

Instances

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

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

predicate lifting over multivariate functors

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

relational lifting over multivariate functors

Equations
• One or more equations did not get rendered due to their size.
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

Equations
• = {y : α i | ∀ ⦃P : (i : Fin2 n) → α iProp⦄, P i y}
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 y
class LawfulMvFunctor {n : } (F : Type u_1) [] :

laws for MvFunctor

• 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 : α.Arrow β) (h : β.Arrow γ) (x : F α), MvFunctor.map () x = MvFunctor.map h ()

map preserves compositions

Instances
theorem LawfulMvFunctor.id_map {n : } {F : Type u_1} [] [self : ] {α : } (x : F α) :
MvFunctor.map TypeVec.id x = x

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

theorem LawfulMvFunctor.comp_map {n : } {F : Type u_1} [] [self : ] {α : } {β : } {γ : } (g : α.Arrow β) (h : β.Arrow γ) (x : F α) :

map preserves compositions

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

adapt MvFunctor.LiftP to accept predicates as arrows

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

adapt MvFunctor.LiftR to accept relations as arrows

Equations
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 : Fin2 n) (a : α _i) => a) x = x
theorem MvFunctor.map_map {n : } {α : } {β : } {γ : } {F : Type v} [] [] (g : α.Arrow β) (h : β.Arrow γ) (x : F α) :
theorem MvFunctor.exists_iff_exists_of_mono {n : } {α : } {β : } (F : Type v) [] [] {P : F αProp} {q : F βProp} (f : α.Arrow β) (g : β.Arrow α) (h₀ : = TypeVec.id) (h₁ : ∀ (u : F α), P u q ()) :
(∃ (u : F α), P u) ∃ (u : F β), q u
theorem MvFunctor.LiftP_def {n : } {α : } {F : Type v} [] (P : α.Arrow ()) [] (x : F α) :
∃ (u : F ()), = x
theorem MvFunctor.LiftR_def {n : } {α : } {F : Type v} [] (R : (α.prod α).Arrow ()) [] (x : F α) (y : F α) :
∃ (u : F ()), 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.{u} (n + 1)Type u_1} [] [] {α : } {β : Type u} (P : βProp) (x : F (α ::: β)) :
MvFunctor.LiftP' (α.PredLast' P) x MvFunctor.LiftP (α.PredLast P) x
theorem MvFunctor.LiftR_RelLast_iff {n : } {F : TypeVec.{u} (n + 1)Type u_1} [] [] {α : } {β : Type u} (rr : ββProp) (x : F (α ::: β)) (y : F (α ::: β)) :
MvFunctor.LiftR' (α.RelLast' rr) x y MvFunctor.LiftR (fun {i : Fin2 (n + 1)} => α.RelLast rr) x y
def MvFunctor.ofEquiv {n : } {F : Type u_1} {F' : Type u_2} [] (eqv : (α : ) → F α F' α) :

Any type function that is (extensionally) equivalent to a functor, is itself a functor

Equations
• = { map := fun {α β : } (f : α.Arrow β) (x : F α) => (eqv β).symm (MvFunctor.map f ((eqv α) x)) }
Instances For