Function prop::path_semantics::xy_norm

pub fn xy_norm<A: LProp, B: LProp, C: LProp, D: LProp>(
    p1: PSemNaive<A, B, C, D>,
    p2: PSemNaiveNorm<A, B, C, D>,
    f_eq_a_b: Imply<Q<A::SetLevel<(A::N, <LN<Zero, A, B, C, D> as LProp>::N)>, B::SetLevel<(B::N, <LN<One, A, B, C, D> as LProp>::N)>>, And<Q<A, B>, Q<LN<Zero, A, B, C, D>, LN<One, A, B, C, D>>>>,
    f_a_c: Imply<Imply<A::SetLevel<(A::N, <LN<Zero, A, B, C, D> as LProp>::N)>, C::SetLevel<(C::N, <LN<Two, A, B, C, D> as LProp>::N)>>, And<Imply<A, C>, Imply<LN<Zero, A, B, C, D>, LN<Two, A, B, C, D>>>>,
    f_b_d: Imply<Imply<B::SetLevel<(B::N, <LN<One, A, B, C, D> as LProp>::N)>, D::SetLevel<(D::N, <LN<Three, A, B, C, D> as LProp>::N)>>, And<Imply<B, D>, Imply<LN<One, A, B, C, D>, LN<Three, A, B, C, D>>>>,
    f_eq_c_d: Imply<And<Q<C, D>, Q<LN<Two, A, B, C, D>, LN<Three, A, B, C, D>>>, Q<C::SetLevel<(C::N, <LN<Two, A, B, C, D> as LProp>::N)>, D::SetLevel<(D::N, <LN<Three, A, B, C, D> as LProp>::N)>>>
) -> PSemNaive<A::SetLevel<(A::N, <LN<Zero, A, B, C, D> as LProp>::N)>, B::SetLevel<(B::N, <LN<One, A, B, C, D> as LProp>::N)>, C::SetLevel<(C::N, <LN<Two, A, B, C, D> as LProp>::N)>, D::SetLevel<(D::N, <LN<Three, A, B, C, D> as LProp>::N)>>where
    (A::N, B::N): SortMin<A, B> + SortMax<A, B>,
    (C::N, D::N): SortMin<C, D> + SortMax<C, D>,
    (<Min<A, B> as LProp>::N, <Min<C, D> as LProp>::N): SortMin<Min<A, B>, Min<C, D>> + SortMax<Min<A, B>, Min<C, D>>,
    (<Max<A, B> as LProp>::N, <Max<C, D> as LProp>::N): SortMin<Max<A, B>, Max<C, D>> + SortMax<Max<A, B>, Max<C, D>>,
    (<MaxMin<A, B, C, D> as LProp>::N, <MinMax<A, B, C, D> as LProp>::N): SortMin<MaxMin<A, B, C, D>, MinMax<A, B, C, D>> + SortMax<MaxMin<A, B, C, D>, MinMax<A, B, C, D>>,
    <MinMin<A, B, C, D> as LProp>::N: Lt<<Maxi<A, B, C, D> as LProp>::N>,
    <Mixi<A, B, C, D> as LProp>::N: Lt<<MaxMax<A, B, C, D> as LProp>::N>,

Constructs a 2D naive core axiom from two naive core axioms, where one is normalised of the other.