Figure out the correct definition of higher homotopy levels

[bvssvni]

Currently, the definition of is_groupoid_n is the following:

/// Defines an n-groupoid relation from `x` to `a` and `b`.
pub fn is_groupoid_n(n: u32, x: u64, a: u64, b: u64) -> u64 {
    let cond = and(imply(a, x), imply(b, x));
    let mut a = a;
    let mut b = b;
    for _ in 0..n {
        a = qubit(a);
        b = qubit(b);
    }
    imply(cond, imply(eq(a, b), eq(qubit(a), qubit(b))))
}

https://github.com/advancedresearch/pocket_prover/blob/master/src/lib.rs#L659-L669

This lifts equality of qubits at the last level in general.

It is sufficient to prove homotopy equivalence, e.g.:

use pocket_prover::*;

fn main() {
    println!("{}", measure(1000, || prove!(&mut |a, b, x| {
        imply(
            and!(
                is_hom_lev_n(7, x, a, b),
                imply(a, x),
                hom_eq(6, a, b),
            ),
            hom_eq(7, a, b)
        )
    })))
}

However, a more strict definition is also possible that is limited to homotopy equivalence:

pub fn is_groupoid_n(n: u32, x: u64, a: u64, b: u64) -> u64 {
    imply(and(imply(a, x), imply(b, x)), imply(hom_eq(n + 1, a, b), hom_eq(n + 2, a, b)))
}