∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (X : C × C),
  CategoryTheory.IsFiltered (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag C))