{motive : LightDiagram → Sort u_1} →
  (t : LightDiagram) →
    ((diagram : CategoryTheory.Functor ℕᵒᵖ FintypeCat) →
        (cone : CategoryTheory.Limits.Cone (diagram.comp FintypeCat.toProfinite)) →
          (isLimit : CategoryTheory.Limits.IsLimit cone) →
            motive { diagram := diagram, cone := cone, isLimit := isLimit }) →
      motive t