Mathlib Map

Theorems · Definition · category theory

TypeVec.Arrow

{n : ℕ} → TypeVec.{u} n → TypeVec.{v} n → Type (max u v)

arrow in the category of TypeVec

Defined in
Mathlib.Data.TypeVec
Cited by
144 results in Mathlib
Foundations
Depth 3 from the axioms, rests on 4 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MvFunctor.map · cited by 58MvFunctor.mapTypeVec.comp · cited by 52TypeVec.compTypeVec.id · cited by 46TypeVec.idMvPFunctor.Obj · cited by 43MvPFunctor.ObjTypeVec.appendFun · cited by 42TypeVec.appendFunTypeVec.dropFun · cited by 32TypeVec.dropFunTypeVec.splitFun · cited by 23TypeVec.splitFunTypeVec.Subtype_ · cited by 22TypeVec.Subtype_TypeVec.Arrow.ext · cited by 21Arrow.extTypeVec.lastFun · cited by 19TypeVec.lastFunMvQPF.abs_map · cited by 13MvQPF.abs_mapMvPFunctor.map_eq · cited by 13MvPFunctor.map_eqMvPFunctor.wMk · cited by 13MvPFunctor.wMkTypeVec.subtypeVal · cited by 11TypeVec.subtypeValMvFunctor.map_map · cited by 10MvFunctor.map_mapTypeVec · cited by 185TypeVecFin2 · cited by 145Fin2TypeVec.ArrowCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • TypeVecstatement and proof · cited by 185
  • Fin2proof · cited by 145

Cited by236

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 236.