add one lemma to precategories
finished one direction of cone univalence