Theorems · Definition · category theory
PFunctor.Idx
PFunctor.{uA, uB} → Type (max uA uB)Idx identifies a location inside the application of a polynomial functor. For F : PFunctor,
x : F α and i : F.Idx, i can designate one part of x or is invalid, if i.1 ≠ x.1.
- Defined in
- Mathlib.Data.PFunctor.Univariate.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PFunctor.Bproof · cited by 119
- PFunctor.Aproof · cited by 101
- PFunctorstatement and proof · cited by 75
Cited by17
Results whose statement or proof uses this declaration.
- PFunctor.Approx.Pathproof · cited by 11
- PFunctor.M.IsPath.casesOnstatement · cited by 2
- PFunctor.M.isubtree_consstatement · cited by 2
- PFunctor.Obj.igetstatement and proof · cited by 2
- PFunctor.M.ext_auxstatement · cited by 1
- PFunctor.M.ichildrenstatement and proof · cited by 1
- PFunctor.M.isPath_consstatement · cited by 1
- PFunctor.M.isPath_cons'statement · cited by 1
- PFunctor.M.iselect_consstatement · cited by 1
- PFunctor.M.iselect_eq_defaultproof · cited by 1
- PFunctor.M.nth_of_bisimproof · cited by 1
- PFunctor.M.ichildren_mkstatement and proof · cited by 0