before breaking everything by changing the def of is_left_adjoint
finished isaprop_is_left_adjoint
finished is_equivalence is proposition