Trait prop::univalence::HomotopyLevel

source · [−]
pub trait HomotopyLevel<N: Nat>: Prop {
    type H0: Prop;
    type H: HomotopyLevel<<N as Dec>::Out>;
    fn h0<Y: LProp>(ty_y: Ty<Y, Self>) -> Q<Self::H0, Y>
    where
        (N, Z): EqNat;

    fn hn<X: LProp, Y: LProp>(
        ty_x: Ty<X, Self>, 
        ty_y: Ty<Y, Self>
    ) -> Q<Self::H, Q<X, Y>>
    where
        Z: Lt<N>;
}
Expand description

Homotopy Level.

For theoretical background, see nLab - homotopy levels.

Associated Types

A type such that it proves homotopy level 0.

A type such that it proves a lower homotopy level.

Required methods

Homotopy level 0.

Higher homotopy level.

Implementors