Function prop::path_semantics::ty_eqq_imply

source · [−]

pub fn ty_eqq_imply<X: DProp, Y: DProp, A: Prop, B: Prop>(
    (xa, pord_xa): Ty<X, A>, 
    (yb, pord_yb): Ty<Y, B>, 
    eqq_xy: EqQ<X, Y>
) -> Ty<Imply<X, Y>, Imply<A, B>>

Expand description

(x : a) ⋀ (y : b) ⋀ eqq(x, y) => ((x => y) : (a => b)).