Function prop::univalence::h2

source · [−]

pub fn h2<X: LProp, Y: LProp, X2: LProp, Y2: LProp, N: Nat, A: HProp<S<S<N>>>>(
    ty_x: Ty<X, A>, 
    ty_y: Ty<Y, A>, 
    ty_x2_q_xy: Ty<X2, Q<X, Y>>, 
    ty_y2_q_xy: Ty<Y2, Q<X, Y>>
) -> Q<H2<A, N>, Q<X2, Y2>>

Expand description

Get the type of the path between paths.