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 : TypeVec nType 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

Instances

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

    Equations
    • One or more equations did not get rendered due to their size.
    def MvFunctor.LiftP {n : } {F : TypeVec nType v} [inst : MvFunctor F] {α : TypeVec n} (P : (i : Fin2 n) → α iProp) (x : F α) :

    predicate lifting over multivariate functors

    Equations
    def MvFunctor.LiftR {n : } {F : TypeVec nType v} [inst : MvFunctor F] {α : TypeVec n} (R : {i : Fin2 n} → α iα iProp) (x : F α) (y : F α) :

    relational lifting over multivariate functors

    Equations
    def MvFunctor.supp {n : } {F : TypeVec nType 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
    theorem MvFunctor.of_mem_supp {n : } {F : TypeVec nType v} [inst : MvFunctor F] {α : TypeVec n} {x : F α} {P : i : Fin2 n⦄ → α iProp} (h : MvFunctor.LiftP P x) (i : Fin2 n) (y : α i) :
    y MvFunctor.supp x iP i y
    class LawfulMvFunctor {n : } (F : TypeVec nType u_2) [inst : MvFunctor F] :

    laws for MvFunctor

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

      adapt MvFunctor.LiftP to accept predicates as arrows

      Equations
      def MvFunctor.LiftR' {n : } {α : TypeVec n} {F : TypeVec nType 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
      @[simp]
      theorem MvFunctor.id_map {n : } {α : TypeVec n} {F : TypeVec nType v} [inst : MvFunctor F] [inst : LawfulMvFunctor F] (x : F α) :
      MvFunctor.map TypeVec.id x = x
      @[simp]
      theorem MvFunctor.id_map' {n : } {α : TypeVec n} {F : TypeVec nType v} [inst : MvFunctor F] [inst : LawfulMvFunctor F] (x : F α) :
      MvFunctor.map (fun _i a => a) x = x
      theorem MvFunctor.map_map {n : } {α : TypeVec n} {β : TypeVec n} {γ : TypeVec n} {F : TypeVec nType v} [inst : MvFunctor F] [inst : LawfulMvFunctor F] (g : TypeVec.Arrow α β) (h : TypeVec.Arrow β γ) (x : F α) :
      theorem MvFunctor.exists_iff_exists_of_mono {n : } {α : TypeVec n} {β : TypeVec n} (F : TypeVec nType 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
      theorem MvFunctor.LiftP_def {n : } {α : TypeVec n} {F : TypeVec nType v} [inst : MvFunctor F] (P : TypeVec.Arrow α (TypeVec.repeat n Prop)) [inst : LawfulMvFunctor F] (x : F α) :
      theorem MvFunctor.LiftR_def {n : } {α : TypeVec n} {F : TypeVec nType 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
      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 (α ::: β)) :
      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 (α ::: β)) :