Type Definition prop::univalence::Hom

source · 
pub type Hom<A, B> = Imply<Imply<A, B>, Q<A, B>>;
Expand description

A homotopy path between paths A and B.