Documentation

Mathlib.Control.Functor.Multivariate

Functors between the category of tuples of types, and the category Type #

Features:

class MvFunctor {n : } (F : TypeVec.{u_2} nType 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 β.

Instances

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

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

      predicate lifting over multivariate functors

      Equations
      Instances For
        def MvFunctor.LiftR {n : } {F : TypeVec.{u} nType v} [MvFunctor F] {α : TypeVec.{u} n} (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 : TypeVec.{u} nType 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

          Equations
          Instances For
            theorem MvFunctor.of_mem_supp {n : } {F : TypeVec.{u} nType v} [MvFunctor F] {α : TypeVec.{u} n} {x : F α} {P : i : Fin2 n⦄ → α iProp} (h : MvFunctor.LiftP P x) (i : Fin2 n) (y : α i) :
            y MvFunctor.supp x iP y
            class LawfulMvFunctor {n : } (F : TypeVec.{u_2} nType u_1) [MvFunctor F] :

            laws for MvFunctor

            Instances
              theorem LawfulMvFunctor.id_map {n : } {F : TypeVec.{u_2} nType u_1} [MvFunctor F] [self : LawfulMvFunctor F] {α : TypeVec.{u_2} n} (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 : TypeVec.{u_2} nType u_1} [MvFunctor F] [self : LawfulMvFunctor F] {α : TypeVec.{u_2} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_2} n} (g : α.Arrow β) (h : β.Arrow γ) (x : F α) :

              map preserves compositions

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

              adapt MvFunctor.LiftP to accept predicates as arrows

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

                adapt MvFunctor.LiftR to accept relations as arrows

                Equations
                Instances For
                  @[simp]
                  theorem MvFunctor.id_map {n : } {α : TypeVec.{u} n} {F : TypeVec.{u} nType v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) :
                  MvFunctor.map TypeVec.id x = x
                  @[simp]
                  theorem MvFunctor.id_map' {n : } {α : TypeVec.{u} n} {F : TypeVec.{u} nType v} [MvFunctor F] [LawfulMvFunctor F] (x : F α) :
                  MvFunctor.map (fun (_i : Fin2 n) (a : α _i) => a) x = x
                  theorem MvFunctor.map_map {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} {γ : TypeVec.{u} n} {F : TypeVec.{u} nType v} [MvFunctor F] [LawfulMvFunctor F] (g : α.Arrow β) (h : β.Arrow γ) (x : F α) :
                  theorem MvFunctor.exists_iff_exists_of_mono {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} (F : TypeVec.{u} nType 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 (MvFunctor.map f u)) :
                  (∃ (u : F α), P u) ∃ (u : F β), q u
                  theorem MvFunctor.LiftP_def {n : } {α : TypeVec.{u} n} {F : TypeVec.{u} nType v} [MvFunctor F] (P : α.Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x : F α) :
                  theorem MvFunctor.LiftR_def {n : } {α : TypeVec.{u} n} {F : TypeVec.{u} nType v} [MvFunctor F] (R : (α.prod α).Arrow (TypeVec.repeat n Prop)) [LawfulMvFunctor F] (x : F α) (y : F α) :
                  MvFunctor.LiftR' R x y ∃ (u : F (TypeVec.Subtype_ R)), 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.{u} (n + 1)Type u_1} [MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : 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} [MvFunctor F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {β : 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 : TypeVec.{u} nType u_1} {F' : TypeVec.{u} nType u_2} [MvFunctor F'] (eqv : (α : TypeVec.{u} n) → F α F' α) :

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

                  Equations
                  Instances For