Function prop::path_semantics::creation_hom

source · [−]

pub fn creation_hom<X: Prop, Y: Prop, A: Prop, B: Prop>(
    nx: Not<X>, 
    ty_y_b: Ty<Y, B>, 
    hom_xy: Hom<X, Y>, 
    pord: POrdProof<X, A>
) -> Imply<A, B>

Expand description

Creation theorem using homotopy map.