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 : TypeVec.{u_2} n → 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 {α β : TypeVec.{u_2} n} : α.Arrow β → F α → F β

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

def MvFunctor.«term_<$$>_» : Lean.TrailingParserDescr

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

def MvFunctor.LiftP {n : ℕ} {F : TypeVec.{u} n → Type v} [MvFunctor F] {α : TypeVec.{u} n} (P : (i : Fin2 n) → α i → Prop) (x : F α) : Prop

predicate lifting over multivariate functors

def MvFunctor.LiftR {n : ℕ} {F : TypeVec.{u} n → Type v} [MvFunctor F] {α : TypeVec.{u} n} (R : ⦃i : Fin2 n⦄ → α i → α i → Prop) (x y : F α) : Prop

relational lifting over multivariate functors

def MvFunctor.supp {n : ℕ} {F : TypeVec.{u} n → Type v} [MvFunctor F] {α : TypeVec.{u} 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

theorem MvFunctor.of_mem_supp {n : ℕ} {F : TypeVec.{u} n → Type v} [MvFunctor F] {α : TypeVec.{u} n} {x : F α} {P : ⦃i : Fin2 n⦄ → α i → Prop} (h : LiftP P x) (i : Fin2 n) (y : α i) : y ∈ supp x i → P y

class LawfulMvFunctor {n : ℕ} (F : TypeVec.{u_2} n → Type u_1) [MvFunctor F] : Prop

laws for MvFunctor

• id_map {α : TypeVec.{u_2} n} (x : F α) : MvFunctor.map TypeVec.id x = x

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

• comp_map {α β γ : TypeVec.{u_2} n} (g : α.Arrow β) (h : β.Arrow γ) (x : F α) : MvFunctor.map (TypeVec.comp h g) x = MvFunctor.map h (MvFunctor.map g x)

  map preserves compositions

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

adapt MvFunctor.LiftP to accept predicates as arrows

def MvFunctor.LiftR' {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] (R : (α.prod α).Arrow (TypeVec.repeat n Prop)) : F α → F α → Prop

adapt MvFunctor.LiftR to accept relations as arrows

@[simp]

theorem MvFunctor.id_map {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) : map TypeVec.id x = x

@[simp]

theorem MvFunctor.id_map' {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) : map (fun (_i : Fin2 n) (a : α _i) => a) x = x

theorem MvFunctor.map_map {n : ℕ} {α β γ : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] [LawfulMvFunctor F] (g : α.Arrow β) (h : β.Arrow γ) (x : F α) : map h (map g x) = map (TypeVec.comp h g) x

theorem MvFunctor.exists_iff_exists_of_mono {n : ℕ} {α β : TypeVec.{u} n} (F : TypeVec.{u} n → Type v) [MvFunctor F] [LawfulMvFunctor F] {P : F α → Prop} {q : F β → Prop} (f : α.Arrow β) (g : β.Arrow α) (h₀ : TypeVec.comp f g = TypeVec.id) (h₁ : ∀ (u : F α), P u ↔ q (map f u)) : (∃ (u : F α), P u) ↔ ∃ (u : F β), q u

theorem MvFunctor.LiftP_def {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] (P : α.Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x : F α) : LiftP' P x ↔ ∃ (u : F (TypeVec.Subtype_ P)), map (TypeVec.subtypeVal P) u = x

theorem MvFunctor.LiftR_def {n : ℕ} {α : TypeVec.{u} n} {F : TypeVec.{u} n → Type v} [MvFunctor F] (R : (α.prod α).Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x y : F α) : LiftR' R x y ↔ ∃ (u : F (TypeVec.Subtype_ R)), map (TypeVec.comp TypeVec.prod.fst (TypeVec.subtypeVal R)) u = x ∧ map (TypeVec.comp TypeVec.prod.snd (TypeVec.subtypeVal R)) u = y

theorem MvFunctor.LiftP_PredLast_iff {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u_1} [MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : Type u} (P : β → Prop) (x : F (α ::: β)) : LiftP' (α.PredLast' P) x ↔ LiftP (α.PredLast P) x

theorem MvFunctor.LiftR_RelLast_iff {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u_1} [MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : Type u} (rr : β → β → Prop) (x y : F (α ::: β)) : LiftR' (α.RelLast' rr) x y ↔ LiftR (α.RelLast rr) x y

def MvFunctor.ofEquiv {n : ℕ} {F : TypeVec.{u} n → Type u_1} {F' : TypeVec.{u} n → Type u_2} [MvFunctor F'] (eqv : (α : TypeVec.{u} n) → F α ≃ F' α) : MvFunctor F

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