Function prop::univalence::h0_ext

source · [−]
pub fn h0_ext<A: HProp<Z>, B: HProp<Z>, X: LProp>(
    ty_xa: Ty<X, A>, 
    ty_xb: Ty<X, B>
) -> Q<A, B>
Expand description

(x : a) ⋀ (x : b) => (a ~~ b) when a and b are homotopy level 0.