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

ink

class MvFunctor {n : ℕ} (F : TypeVec n → Type u_2) : Type (max(u_1+1)u_2)

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

  map : {α β : TypeVec n} → TypeVec.Arrow α β → F α → F β

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

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

predicate lifting over multivariate functors

Equations

• MvFunctor.LiftP P x = ∃ u, MvFunctor.map (fun i => Subtype.val) u = x

ink

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

relational lifting over multivariate functors

Equations

• MvFunctor.LiftR R x y = ∃ u, MvFunctor.map (fun i t => t.val.fst) u = x ∧ MvFunctor.map (fun i t => t.val.snd) u = y

ink

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

• MvFunctor.supp x i = { y | ⦃P : (i : Fin2 n) → α i → Prop⦄ → MvFunctor.LiftP P x → P i y }

ink

theorem MvFunctor.of_mem_supp {n : ℕ} {F : TypeVec n → Type v} [inst : 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 i → P i y

ink

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

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

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

• map preserves compositions

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

laws for MvFunctor

ink

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

adapt MvFunctor.LiftP to accept predicates as arrows

Equations

• MvFunctor.LiftP' P = MvFunctor.LiftP fun i x => TypeVec.ofRepeat (P i x)

ink

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

adapt MvFunctor.LiftR to accept relations as arrows

Equations

• MvFunctor.LiftR' R = MvFunctor.LiftR fun i x y => TypeVec.ofRepeat (R i (TypeVec.prod.mk i x y))

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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