Function prop::univalence::lift_ty

source · [−]

pub fn lift_ty<X: LProp, Y: LProp, X2: Prop, N: Nat, A: HProp<S<N>>>(
    ty_x: Ty<X, A>, 
    ty_y: Ty<Y, A>, 
    ty_x2_q_xy: Ty<X2, Q<X, Y>>
) -> Ty<X2, A::H>

Expand description

Lift type of path.