Function prop::univalence::ty_h0

source · [−]
pub fn ty_h0<X: LProp, A: HProp<Z>>(ty_x_a: Ty<X, A>) -> Ty<A::H0, A>
Expand description

(x : a) => (a::h0 : a).