[logic-ml] injective types in univalent mathematics