First-Order Homotopical Logic