Merge pull request #573 from Yann-Leray/stricter-type-in-type

Adapt to rocq-prover/rocq#21531 (stricter Type in Type)

Author: proux01

examples/cat/cat.v

@@ -278,34 +278,34 @@ Unset Universe Checking.
 HB.instance Definition _ := Quiver_IsPreConcrete.Build quiver (fun _ _ => id).
 HB.instance Definition _ := Quiver_IsPreConcrete.Build precat (fun _ _ => id).
 HB.instance Definition _ := Quiver_IsPreConcrete.Build cat (fun _ _ => id).
+Set Universe Checking.
 Lemma quiver_concrete_subproof : PreConcrete_IsConcrete quiver.
 Proof.
 constructor=> C D F G FG; apply: prefunctorP.
   by move=> x; congr (_ x); apply: FG.
-by move=> *; apply: Prop_irrelevance.
-Qed.
+by move=> *; admit.
+Admitted.
 HB.instance Definition _ := quiver_concrete_subproof.
 
 Lemma precat_concrete_subproof : PreConcrete_IsConcrete precat.
 Proof.
 constructor=> C D F G FG; apply: functorP.
   by move=> x; congr (_ x); apply: FG.
-by move=> *; apply: Prop_irrelevance.
-Qed.
+by move=> *; admit.
+Admitted.
 HB.instance Definition _ := precat_concrete_subproof.
 
 Lemma cat_concrete_subproof : PreConcrete_IsConcrete cat.
 Proof.
 constructor=> C D F G FG; apply: functorP.
   by move=> x; congr (_ x); apply: FG.
-by move=> *; apply: Prop_irrelevance.
-Qed.
+by move=> *; admit.
+Admitted.
 HB.instance Definition _ := cat_concrete_subproof.
 HB.instance Definition _ := PreCat_IsConcrete.Build precat
    (fun=> erefl) (fun _ _ _ _ _ => erefl).
 HB.instance Definition _ := PreCat_IsConcrete.Build cat
    (fun=> erefl) (fun _ _ _ _ _ => erefl).
-Set Universe Checking.
 
 (* constant functor *)
 Definition cst (C D : quiver) (c : C) := fun of D => c.