Commit 2024-05-30 18:01 ec2ce4cc
View on Github →feat(CategoryTheory): constructor for functors from the category ℕ (#13223)
In this file, we provide a constructor Functor.ofSequence for functors ℕ ⥤ C, which takes as an input a sequence of morphisms f : X n ⟶ X (n + 1) for all n : ℕ.