Function prop::univalence::h0_true_q

source · [−]
pub fn h0_true_q<X: LProp>(ty_x: Ty<X, True>) -> Q<X, X>
Expand description

(x : true) => (x ~~ x).