Do not leave `Admitted` theorems in the code.  Either comment out the statement and remove the partial proof, or remove it entirely.  If you need it in another theorem, you can do something like
```coq
(** Note: This is provable, but since we haven't proven it yet, we assume it as a hypothesis. *)
Hypothesis pullback_subuniverse : ...
```