Slow type-checking: replace `admitted` by proof

[benediktahrens]

File https://github.com/UniMath/TypeTheory/blob/9242475372d001026004536caed15fc9f2922d75/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v contains admitted statements:

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 44 in 9242475

  use weqimplimpl; apply admit_slow_proof.

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 90 in 9242475

  - intros X Y. apply admit_slow_proof. (* refine (pr2 (idweq _)). *)

• TypeTheory/TypeTheory/ALV2/DiscCompCatDef_DiscCompCat_catiso.v

  Line 91 in 9242475

  - admit. (* refine (pr2 DiscCompCat_DiscCompCatDef_weq). *)

Fragments or complete proofs are there, but do not type-check in a reasonable amount of time, or at all.

The admitted statements should be proved.

For some background, see also #202 (comment)