Trait prop::univalence::HLev

pub trait HLev: Nat {
    type Out<A: Prop, B: Prop>: HomotopyEquivalence<A, B, N = Self>;
}

Implemented by homotopy levels.

Required Associated Types

type Out<A: Prop, B: Prop>: HomotopyEquivalence<A, B, N = Self>

The output type.

Implementors

impl HLev for Z

type Out<A: Prop, B: Prop> = True

impl<X: HLev> HLev for S<X>

type Out<A: Prop, B: Prop> = ((Rc<dyn Fn(Qubit<X, A>) -> Qubit<X, B>>, Rc<dyn Fn(Qubit<X, B>) -> Qubit<X, A>>), <X as HLev>::Out<A, B>)