Documentation

Mathlib.Data.TypeVec

Tuples of types, and their categorical structure. #

Features #

Also, support functions for operating with n-tuples of types, such as:

Since e.g. append1 α.drop α.last is propositionally equal to α but not definitionally equal to it, we need support functions and lemmas to mediate between constructions.

def TypeVec (n : ) :
Type (u_1 + 1)

n-tuples of types, as a category

Equations
Instances For
    Equations
    def TypeVec.Arrow {n : } (α : TypeVec.{u_1} n) (β : TypeVec.{u_2} n) :
    Type (max u_1 u_2)

    arrow in the category of TypeVec

    Equations
    • α.Arrow β = ((i : Fin2 n) → α iβ i)
    Instances For
      theorem TypeVec.Arrow.ext_iff {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {f : α.Arrow β} {g : α.Arrow β} :
      f = g ∀ (i : Fin2 n), f i = g i
      theorem TypeVec.Arrow.ext {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : α.Arrow β) (g : α.Arrow β) :
      (∀ (i : Fin2 n), f i = g i)f = g

      Extensionality for arrows

      instance TypeVec.Arrow.inhabited {n : } (α : TypeVec.{u_1} n) (β : TypeVec.{u_2} n) [(i : Fin2 n) → Inhabited (β i)] :
      Inhabited (α.Arrow β)
      Equations
      def TypeVec.id {n : } {α : TypeVec.{u_1} n} :
      α.Arrow α

      identity of arrow composition

      Equations
      Instances For
        def TypeVec.comp {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_3} n} (g : β.Arrow γ) (f : α.Arrow β) :
        α.Arrow γ

        arrow composition in the category of TypeVec

        Equations
        Instances For

          arrow composition in the category of TypeVec

          Equations
          Instances For
            @[simp]
            theorem TypeVec.id_comp {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : α.Arrow β) :
            TypeVec.comp TypeVec.id f = f
            @[simp]
            theorem TypeVec.comp_id {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : α.Arrow β) :
            TypeVec.comp f TypeVec.id = f
            theorem TypeVec.comp_assoc {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} {γ : TypeVec.{u_3} n} {δ : TypeVec.{u_4} n} (h : γ.Arrow δ) (g : β.Arrow γ) (f : α.Arrow β) :
            def TypeVec.append1 {n : } (α : TypeVec.{u_1} n) (β : Type u_1) :

            Support for extending a TypeVec by one element.

            Equations
            • (α ::: β) i.fs = α i
            • (α ::: β) Fin2.fz = β
            Instances For

              Support for extending a TypeVec by one element.

              Equations
              Instances For
                def TypeVec.drop {n : } (α : TypeVec.{u} (n + 1)) :

                retain only a n-length prefix of the argument

                Equations
                • α.drop i = α i.fs
                Instances For
                  def TypeVec.last {n : } (α : TypeVec.{u} (n + 1)) :

                  take the last value of a (n+1)-length vector

                  Equations
                  • α.last = α Fin2.fz
                  Instances For
                    instance TypeVec.last.inhabited {n : } (α : TypeVec.{u_1} (n + 1)) [Inhabited (α Fin2.fz)] :
                    Inhabited α.last
                    Equations
                    theorem TypeVec.drop_append1 {n : } {α : TypeVec.{u_1} n} {β : Type u_1} {i : Fin2 n} :
                    (α ::: β).drop i = α i
                    @[simp]
                    theorem TypeVec.drop_append1' {n : } {α : TypeVec.{u_1} n} {β : Type u_1} :
                    (α ::: β).drop = α
                    theorem TypeVec.last_append1 {n : } {α : TypeVec.{u_1} n} {β : Type u_1} :
                    (α ::: β).last = β
                    @[simp]
                    theorem TypeVec.append1_drop_last {n : } (α : TypeVec.{u_1} (n + 1)) :
                    α.drop ::: α.last = α
                    def TypeVec.append1Cases {n : } {C : TypeVec.{u_1} (n + 1)Sort u} (H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)) (γ : TypeVec.{u_1} (n + 1)) :
                    C γ

                    cases on (n+1)-length vectors

                    Equations
                    Instances For
                      @[simp]
                      theorem TypeVec.append1_cases_append1 {n : } {C : TypeVec.{u_1} (n + 1)Sort u} (H : (α : TypeVec.{u_1} n) → (β : Type u_1) → C (α ::: β)) (α : TypeVec.{u_1} n) (β : Type u_1) :
                      TypeVec.append1Cases H (α ::: β) = H α β
                      def TypeVec.splitFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.lastα'.last) :
                      α.Arrow α'

                      append an arrow and a function for arbitrary source and target type vectors

                      Equations
                      Instances For
                        def TypeVec.appendFun {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : ββ') :
                        (α ::: β).Arrow (α' ::: β')

                        append an arrow and a function as well as their respective source and target types / typevecs

                        Equations
                        Instances For

                          append an arrow and a function as well as their respective source and target types / typevecs

                          Equations
                          Instances For
                            def TypeVec.dropFun {n : } {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} (f : α.Arrow β) :
                            α.drop.Arrow β.drop

                            split off the prefix of an arrow

                            Equations
                            Instances For
                              def TypeVec.lastFun {n : } {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} (f : α.Arrow β) :
                              α.lastβ.last

                              split off the last function of an arrow

                              Equations
                              Instances For
                                def TypeVec.nilFun {α : TypeVec.{u_1} 0} {β : TypeVec.{u_2} 0} :
                                α.Arrow β

                                arrow in the category of 0-length vectors

                                Equations
                                Instances For
                                  theorem TypeVec.eq_of_drop_last_eq {n : } {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} {f : α.Arrow β} {g : α.Arrow β} (h₀ : TypeVec.dropFun f = TypeVec.dropFun g) (h₁ : TypeVec.lastFun f = TypeVec.lastFun g) :
                                  f = g
                                  @[simp]
                                  theorem TypeVec.dropFun_splitFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.lastα'.last) :
                                  def TypeVec.Arrow.mp {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (h : α = β) :
                                  α.Arrow β

                                  turn an equality into an arrow

                                  Equations
                                  Instances For
                                    def TypeVec.Arrow.mpr {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (h : α = β) :
                                    β.Arrow α

                                    turn an equality into an arrow, with reverse direction

                                    Equations
                                    Instances For
                                      def TypeVec.toAppend1DropLast {n : } {α : TypeVec.{u_1} (n + 1)} :
                                      α.Arrow (α.drop ::: α.last)

                                      decompose a vector into its prefix appended with its last element

                                      Equations
                                      Instances For
                                        def TypeVec.fromAppend1DropLast {n : } {α : TypeVec.{u_1} (n + 1)} :
                                        (α.drop ::: α.last).Arrow α

                                        stitch two bits of a vector back together

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem TypeVec.lastFun_splitFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.drop.Arrow α'.drop) (g : α.lastα'.last) :
                                          @[simp]
                                          theorem TypeVec.dropFun_appendFun {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : ββ') :
                                          @[simp]
                                          theorem TypeVec.lastFun_appendFun {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : ββ') :
                                          theorem TypeVec.split_dropFun_lastFun {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.Arrow α') :
                                          theorem TypeVec.splitFun_inj {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} {f : α.drop.Arrow α'.drop} {f' : α.drop.Arrow α'.drop} {g : α.lastα'.last} {g' : α.lastα'.last} (H : TypeVec.splitFun f g = TypeVec.splitFun f' g') :
                                          f = f' g = g'
                                          theorem TypeVec.appendFun_inj {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} {f : α.Arrow α'} {f' : α.Arrow α'} {g : ββ'} {g' : ββ'} :
                                          (f ::: g) = (f' ::: g')f = f' g = g'
                                          theorem TypeVec.splitFun_comp {n : } {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : α₀.drop.Arrow α₁.drop) (f₁ : α₁.drop.Arrow α₂.drop) (g₀ : α₀.lastα₁.last) (g₁ : α₁.lastα₂.last) :
                                          TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ g₀) = TypeVec.comp (TypeVec.splitFun f₁ g₁) (TypeVec.splitFun f₀ g₀)
                                          theorem TypeVec.appendFun_comp_splitFun {n : } {α : TypeVec.{u_1} n} {γ : TypeVec.{u_2} n} {β : Type u_1} {δ : Type u_2} {ε : TypeVec.{u_3} (n + 1)} (f₀ : ε.drop.Arrow α) (f₁ : α.Arrow γ) (g₀ : ε.lastβ) (g₁ : βδ) :
                                          TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ g₀)
                                          theorem TypeVec.appendFun_comp {n : } {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀β₁) (g₁ : β₁β₂) :
                                          (TypeVec.comp f₁ f₀ ::: g₁ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)
                                          theorem TypeVec.appendFun_comp' {n : } {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀β₁) (g₁ : β₁β₂) :
                                          TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀) = (TypeVec.comp f₁ f₀ ::: g₁ g₀)
                                          theorem TypeVec.nilFun_comp {α₀ : TypeVec.{u_1} 0} (f₀ : α₀.Arrow Fin2.elim0) :
                                          TypeVec.comp TypeVec.nilFun f₀ = f₀
                                          theorem TypeVec.appendFun_comp_id {n : } {α : TypeVec.{u} n} {β₀ : Type u} {β₁ : Type u} {β₂ : Type u} (g₀ : β₀β₁) (g₁ : β₁β₂) :
                                          (TypeVec.id ::: g₁ g₀) = TypeVec.comp (TypeVec.id ::: g₁) (TypeVec.id ::: g₀)
                                          @[simp]
                                          theorem TypeVec.dropFun_comp {n : } {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) :
                                          @[simp]
                                          theorem TypeVec.lastFun_comp {n : } {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) :
                                          theorem TypeVec.appendFun_aux {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : (α ::: β).Arrow (α' ::: β')) :
                                          theorem TypeVec.appendFun_id_id {n : } {α : TypeVec.{u_1} n} {β : Type u_1} :
                                          (TypeVec.id ::: id) = TypeVec.id
                                          def TypeVec.casesNil {β : TypeVec.{u_2} 0Sort u_1} (f : β Fin2.elim0) (v : TypeVec.{u_2} 0) :
                                          β v

                                          cases distinction for 0-length type vector

                                          Equations
                                          Instances For
                                            def TypeVec.casesCons (n : ) {β : TypeVec.{u_2} (n + 1)Sort u_1} (f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)) (v : TypeVec.{u_2} (n + 1)) :
                                            β v

                                            cases distinction for (n+1)-length type vector

                                            Equations
                                            Instances For
                                              theorem TypeVec.casesNil_append1 {β : TypeVec.{u_2} 0Sort u_1} (f : β Fin2.elim0) :
                                              TypeVec.casesNil f Fin2.elim0 = f
                                              theorem TypeVec.casesCons_append1 (n : ) {β : TypeVec.{u_2} (n + 1)Sort u_1} (f : (t : Type u_2) → (v : TypeVec.{u_2} n) → β (v ::: t)) (v : TypeVec.{u_2} n) (α : Type u_2) :
                                              TypeVec.casesCons n f (v ::: α) = f α v
                                              def TypeVec.typevecCasesNil₃ {β : (v : TypeVec.{u_2} 0) → (v' : TypeVec.{u_3} 0) → v.Arrow v'Sort u_1} (f : β Fin2.elim0 Fin2.elim0 TypeVec.nilFun) (v : TypeVec.{u_2} 0) (v' : TypeVec.{u_3} 0) (fs : v.Arrow v') :
                                              β v v' fs

                                              cases distinction for an arrow in the category of 0-length type vectors

                                              Equations
                                              Instances For
                                                def TypeVec.typevecCasesCons₃ (n : ) {β : (v : TypeVec.{u_2} (n + 1)) → (v' : TypeVec.{u_3} (n + 1)) → v.Arrow v'Sort u_1} (F : (t : Type u_2) → (t' : Type u_3) → (f : tt') → (v : TypeVec.{u_2} n) → (v' : TypeVec.{u_3} n) → (fs : v.Arrow v') → β (v ::: t) (v' ::: t') (fs ::: f)) (v : TypeVec.{u_2} (n + 1)) (v' : TypeVec.{u_3} (n + 1)) (fs : v.Arrow v') :
                                                β v v' fs

                                                cases distinction for an arrow in the category of (n+1)-length type vectors

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def TypeVec.typevecCasesNil₂ {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0Sort u_1} (f : β TypeVec.nilFun) (f : TypeVec.Arrow Fin2.elim0 Fin2.elim0) :
                                                  β f

                                                  specialized cases distinction for an arrow in the category of 0-length type vectors

                                                  Equations
                                                  Instances For
                                                    def TypeVec.typevecCasesCons₂ (n : ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n) {β : (v ::: t).Arrow (v' ::: t')Sort u_3} (F : (f : tt') → (fs : v.Arrow v') → β (fs ::: f)) (fs : (v ::: t).Arrow (v' ::: t')) :
                                                    β fs

                                                    specialized cases distinction for an arrow in the category of (n+1)-length type vectors

                                                    Equations
                                                    Instances For
                                                      theorem TypeVec.typevecCasesNil₂_appendFun {β : TypeVec.Arrow Fin2.elim0 Fin2.elim0Sort u_1} (f : β TypeVec.nilFun) :
                                                      TypeVec.typevecCasesNil₂ f TypeVec.nilFun = f
                                                      theorem TypeVec.typevecCasesCons₂_appendFun (n : ) (t : Type u_1) (t' : Type u_2) (v : TypeVec.{u_1} n) (v' : TypeVec.{u_2} n) {β : (v ::: t).Arrow (v' ::: t')Sort u_3} (F : (f : tt') → (fs : v.Arrow v') → β (fs ::: f)) (f : tt') (fs : v.Arrow v') :
                                                      TypeVec.typevecCasesCons₂ n t t' v v' F (fs ::: f) = F f fs
                                                      def TypeVec.PredLast {n : } (α : TypeVec.{u_1} n) {β : Type u_1} (p : βProp) ⦃i : Fin2 (n + 1) :
                                                      (α ::: β) iProp

                                                      PredLast α p x predicates p of the last element of x : α.append1 β.

                                                      Equations
                                                      • α.PredLast p = fun (x : (α ::: β) i.fs) => True
                                                      • α.PredLast p = p
                                                      Instances For
                                                        def TypeVec.RelLast {n : } (α : TypeVec.{u} n) {β : Type u} {γ : Type u} (r : βγProp) ⦃i : Fin2 (n + 1) :
                                                        (α ::: β) i(α ::: γ) iProp

                                                        RelLast α r x y says that p the last elements of x y : α.append1 β are related by r and all the other elements are equal.

                                                        Equations
                                                        • α.RelLast r = Eq
                                                        • α.RelLast r = r
                                                        Instances For
                                                          def TypeVec.repeat (n : ) :

                                                          repeat n t is a n-length type vector that contains n occurrences of t

                                                          Equations
                                                          Instances For

                                                            prod α β is the pointwise product of the components of α and β

                                                            Equations
                                                            • x_3.prod x_4 = Fin2.elim0
                                                            • α.prod β = α.drop.prod β.drop ::: (α.last × β.last)
                                                            Instances For

                                                              prod α β is the pointwise product of the components of α and β

                                                              Equations
                                                              Instances For
                                                                def TypeVec.const {β : Type u_1} (x : β) {n : } (α : TypeVec.{u_2} n) :
                                                                α.Arrow (TypeVec.repeat n β)

                                                                const x α is an arrow that ignores its source and constructs a TypeVec that contains nothing but x

                                                                Equations
                                                                Instances For
                                                                  def TypeVec.repeatEq {n : } (α : TypeVec.{u_1} n) :
                                                                  (α.prod α).Arrow (TypeVec.repeat n Prop)

                                                                  vector of equality on a product of vectors

                                                                  Equations
                                                                  Instances For
                                                                    theorem TypeVec.const_append1 {β : Type u_1} {γ : Type u_2} (x : γ) {n : } (α : TypeVec.{u_1} n) :
                                                                    TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun (x_1 : β) => x)
                                                                    theorem TypeVec.eq_nilFun {α : TypeVec.{u_1} 0} {β : TypeVec.{u_2} 0} (f : α.Arrow β) :
                                                                    f = TypeVec.nilFun
                                                                    theorem TypeVec.id_eq_nilFun {α : TypeVec.{u_1} 0} :
                                                                    TypeVec.id = TypeVec.nilFun
                                                                    theorem TypeVec.const_nil {β : Type u_1} (x : β) (α : TypeVec.{u_2} 0) :
                                                                    TypeVec.const x α = TypeVec.nilFun
                                                                    theorem TypeVec.repeat_eq_append1 {β : Type u_1} {n : } (α : TypeVec.{u_1} n) :
                                                                    (α ::: β).repeatEq = TypeVec.splitFun α.repeatEq (Function.uncurry Eq)
                                                                    theorem TypeVec.repeat_eq_nil (α : TypeVec.{u_1} 0) :
                                                                    α.repeatEq = TypeVec.nilFun
                                                                    def TypeVec.PredLast' {n : } (α : TypeVec.{u_1} n) {β : Type u_1} (p : βProp) :
                                                                    (α ::: β).Arrow (TypeVec.repeat (n + 1) Prop)

                                                                    predicate on a type vector to constrain only the last object

                                                                    Equations
                                                                    Instances For
                                                                      def TypeVec.RelLast' {n : } (α : TypeVec.{u_1} n) {β : Type u_1} (p : ββProp) :
                                                                      ((α ::: β).prod (α ::: β)).Arrow (TypeVec.repeat (n + 1) Prop)

                                                                      predicate on the product of two type vectors to constrain only their last object

                                                                      Equations
                                                                      Instances For
                                                                        def TypeVec.Curry {n : } (F : TypeVec.{u} (n + 1)Type u_1) (α : Type u) (β : TypeVec.{u} n) :
                                                                        Type u_1

                                                                        given F : TypeVec.{u} (n+1) → Type u, curry F : Type u → TypeVec.{u} → Type u, i.e. its first argument can be fed in separately from the rest of the vector of arguments

                                                                        Equations
                                                                        Instances For
                                                                          instance TypeVec.Curry.inhabited {n : } (F : TypeVec.{u} (n + 1)Type u_1) (α : Type u) (β : TypeVec.{u} n) [I : Inhabited (F (β ::: α))] :
                                                                          Equations
                                                                          def TypeVec.dropRepeat (α : Type u_1) {n : } :
                                                                          (TypeVec.repeat n.succ α).drop.Arrow (TypeVec.repeat n α)

                                                                          arrow to remove one element of a repeat vector

                                                                          Equations
                                                                          Instances For
                                                                            def TypeVec.ofRepeat {α : Type u_1} {n : } {i : Fin2 n} :
                                                                            TypeVec.repeat n α iα

                                                                            projection for a repeat vector

                                                                            Equations
                                                                            • TypeVec.ofRepeat = fun (a : α) => a
                                                                            • TypeVec.ofRepeat = TypeVec.ofRepeat
                                                                            Instances For
                                                                              theorem TypeVec.const_iff_true {n : } {α : TypeVec.{u_1} n} {i : Fin2 n} {x : α i} {p : Prop} :
                                                                              def TypeVec.prod.fst {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} :
                                                                              (α.prod β).Arrow α

                                                                              left projection of a prod vector

                                                                              Equations
                                                                              Instances For
                                                                                def TypeVec.prod.snd {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} :
                                                                                (α.prod β).Arrow β

                                                                                right projection of a prod vector

                                                                                Equations
                                                                                Instances For
                                                                                  def TypeVec.prod.diag {n : } {α : TypeVec.{u} n} :
                                                                                  α.Arrow (α.prod α)

                                                                                  introduce a product where both components are the same

                                                                                  Equations
                                                                                  Instances For
                                                                                    def TypeVec.prod.mk {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} (i : Fin2 n) :
                                                                                    α iβ iα.prod β i

                                                                                    constructor for prod

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[simp]
                                                                                      theorem TypeVec.prod_fst_mk {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i) :
                                                                                      @[simp]
                                                                                      theorem TypeVec.prod_snd_mk {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} (i : Fin2 n) (a : α i) (b : β i) :
                                                                                      def TypeVec.prod.map {n : } {α : TypeVec.{u} n} {α' : TypeVec.{u} n} {β : TypeVec.{u} n} {β' : TypeVec.{u} n} :
                                                                                      α.Arrow βα'.Arrow β'(α.prod α').Arrow (β.prod β')

                                                                                      prod is functorial

                                                                                      Equations
                                                                                      Instances For
                                                                                        theorem TypeVec.fst_prod_mk {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} {β' : TypeVec.{u_1} n} (f : α.Arrow β) (g : α'.Arrow β') :
                                                                                        TypeVec.comp TypeVec.prod.fst (TypeVec.prod.map f g) = TypeVec.comp f TypeVec.prod.fst
                                                                                        theorem TypeVec.snd_prod_mk {n : } {α : TypeVec.{u_1} n} {α' : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} {β' : TypeVec.{u_1} n} (f : α.Arrow β) (g : α'.Arrow β') :
                                                                                        TypeVec.comp TypeVec.prod.snd (TypeVec.prod.map f g) = TypeVec.comp g TypeVec.prod.snd
                                                                                        theorem TypeVec.fst_diag {n : } {α : TypeVec.{u_1} n} :
                                                                                        TypeVec.comp TypeVec.prod.fst TypeVec.prod.diag = TypeVec.id
                                                                                        theorem TypeVec.snd_diag {n : } {α : TypeVec.{u_1} n} :
                                                                                        TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id
                                                                                        theorem TypeVec.repeatEq_iff_eq {n : } {α : TypeVec.{u_1} n} {i : Fin2 n} {x : α i} {y : α i} :
                                                                                        TypeVec.ofRepeat (α.repeatEq i (TypeVec.prod.mk i x y)) x = y
                                                                                        def TypeVec.Subtype_ {n : } {α : TypeVec.{u} n} :
                                                                                        α.Arrow (TypeVec.repeat n Prop)TypeVec.{u} n

                                                                                        given a predicate vector p over vector α, Subtype_ p is the type of vectors that contain an α that satisfies p

                                                                                        Equations
                                                                                        Instances For
                                                                                          def TypeVec.subtypeVal {n : } {α : TypeVec.{u} n} (p : α.Arrow (TypeVec.repeat n Prop)) :
                                                                                          (TypeVec.Subtype_ p).Arrow α

                                                                                          projection on Subtype_

                                                                                          Equations
                                                                                          Instances For
                                                                                            def TypeVec.toSubtype {n : } {α : TypeVec.{u} n} (p : α.Arrow (TypeVec.repeat n Prop)) :
                                                                                            TypeVec.Arrow (fun (i : Fin2 n) => { x : α i // TypeVec.ofRepeat (p i x) }) (TypeVec.Subtype_ p)

                                                                                            arrow that rearranges the type of Subtype_ to turn a subtype of vector into a vector of subtypes

                                                                                            Equations
                                                                                            Instances For
                                                                                              def TypeVec.ofSubtype {n : } {α : TypeVec.{u} n} (p : α.Arrow (TypeVec.repeat n Prop)) :
                                                                                              (TypeVec.Subtype_ p).Arrow fun (i : Fin2 n) => { x : α i // TypeVec.ofRepeat (p i x) }

                                                                                              arrow that rearranges the type of Subtype_ to turn a vector of subtypes into a subtype of vector

                                                                                              Equations
                                                                                              Instances For
                                                                                                def TypeVec.toSubtype' {n : } {α : TypeVec.{u} n} (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) :
                                                                                                TypeVec.Arrow (fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) }) (TypeVec.Subtype_ p)

                                                                                                similar to toSubtype adapted to relations (i.e. predicate on product)

                                                                                                Equations
                                                                                                Instances For
                                                                                                  def TypeVec.ofSubtype' {n : } {α : TypeVec.{u} n} (p : (α.prod α).Arrow (TypeVec.repeat n Prop)) :
                                                                                                  (TypeVec.Subtype_ p).Arrow fun (i : Fin2 n) => { x : α i × α i // TypeVec.ofRepeat (p i (TypeVec.prod.mk i x.1 x.2)) }

                                                                                                  similar to of_subtype adapted to relations (i.e. predicate on product)

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def TypeVec.diagSub {n : } {α : TypeVec.{u} n} :
                                                                                                    α.Arrow (TypeVec.Subtype_ α.repeatEq)

                                                                                                    similar to diag but the target vector is a Subtype_ guaranteeing the equality of the components

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      theorem TypeVec.subtypeVal_nil {α : TypeVec.{u} 0} (ps : α.Arrow (TypeVec.repeat 0 Prop)) :
                                                                                                      TypeVec.subtypeVal ps = TypeVec.nilFun
                                                                                                      theorem TypeVec.diag_sub_val {n : } {α : TypeVec.{u} n} :
                                                                                                      TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
                                                                                                      theorem TypeVec.prod_id {n : } {α : TypeVec.{u} n} {β : TypeVec.{u} n} :
                                                                                                      TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
                                                                                                      theorem TypeVec.append_prod_appendFun {n : } {α : TypeVec.{u} n} {α' : TypeVec.{u} n} {β : TypeVec.{u} n} {β' : TypeVec.{u} n} {φ : Type u} {φ' : Type u} {ψ : Type u} {ψ' : Type u} {f₀ : α.Arrow α'} {g₀ : β.Arrow β'} {f₁ : φφ'} {g₁ : ψψ'} :
                                                                                                      (TypeVec.prod.map f₀ g₀ ::: Prod.map f₁ g₁) = TypeVec.prod.map (f₀ ::: f₁) (g₀ ::: g₁)
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_diag {n : } {α : TypeVec.{u_1} (n + 1)} :
                                                                                                      TypeVec.dropFun TypeVec.prod.diag = TypeVec.prod.diag
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.lastFun_subtypeVal {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_toSubtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.lastFun_toSubtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.lastFun_of_subtype {n : } {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)) :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_RelLast' {n : } {α : TypeVec.{u_1} n} {β : Type u_1} (R : ββProp) :
                                                                                                      TypeVec.dropFun (α.RelLast' R) = α.repeatEq
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_prod {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_1} (n + 1)} {β' : TypeVec.{u_1} (n + 1)} (f : α.Arrow β) (f' : α'.Arrow β') :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.lastFun_prod {n : } {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_1} (n + 1)} {β' : TypeVec.{u_1} (n + 1)} (f : α.Arrow β) (f' : α'.Arrow β') :
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_from_append1_drop_last {n : } {α : TypeVec.{u_1} (n + 1)} :
                                                                                                      TypeVec.dropFun TypeVec.fromAppend1DropLast = TypeVec.id
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.lastFun_from_append1_drop_last {n : } {α : TypeVec.{u_1} (n + 1)} :
                                                                                                      TypeVec.lastFun TypeVec.fromAppend1DropLast = id
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.dropFun_id {n : } {α : TypeVec.{u_1} (n + 1)} :
                                                                                                      TypeVec.dropFun TypeVec.id = TypeVec.id
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.prod_map_id {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} :
                                                                                                      TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.subtypeVal_diagSub {n : } {α : TypeVec.{u_1} n} :
                                                                                                      TypeVec.comp (TypeVec.subtypeVal α.repeatEq) TypeVec.diagSub = TypeVec.prod.diag
                                                                                                      @[simp]
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.subtypeVal_toSubtype {n : } {α : TypeVec.{u_1} n} (p : α.Arrow (TypeVec.repeat n Prop)) :
                                                                                                      TypeVec.comp (TypeVec.subtypeVal p) (TypeVec.toSubtype p) = fun (x : Fin2 n) => Subtype.val
                                                                                                      @[simp]
                                                                                                      theorem TypeVec.toSubtype'_of_subtype' {n : } {α : TypeVec.{u_1} n} (r : (α.prod α).Arrow (TypeVec.repeat n Prop)) :
                                                                                                      theorem TypeVec.subtypeVal_toSubtype' {n : } {α : TypeVec.{u_1} n} (r : (α.prod α).Arrow (TypeVec.repeat n Prop)) :
                                                                                                      TypeVec.comp (TypeVec.subtypeVal r) (TypeVec.toSubtype' r) = fun (i : Fin2 n) (x : { x : α i × α i // TypeVec.ofRepeat (r i (TypeVec.prod.mk i x.1 x.2)) }) => TypeVec.prod.mk i (↑x).1 (↑x).2