∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    FreeSimplexQuiver.homRel
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.succ)))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i)))