Function prop::univalence::h1_lim_ext

source · [−]

pub fn h1_lim_ext<A: HProp<S<N>>, B: HProp<S<N>>, X: LProp, N: Nat>(
    ty_xa: Ty<X, A>, 
    ty_xb: Ty<X, B>, 
    q_xx_x: Eq<Q<X, X>, X>
) -> Q<A, B>

Expand description

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