[logic-ml] models for univalence