pub fn hom_to_univ<A: Prop, B: Prop>(hom: Hom<A, B>) -> Univ<A, B>
((a => b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b)).
((a => b) => (a ~~ b)) => ((a == b) ~~ (a ~~ b))
