From 9749e00d49fc6223288552512c84664ef9985c0b Mon Sep 17 00:00:00 2001 From: Yann Leray Date: Fri, 23 Jan 2026 16:20:52 +0100 Subject: [PATCH] Adapt to rocq-prover/rocq#21531 (stricter Type in Type) --- examples/cat/cat.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/examples/cat/cat.v b/examples/cat/cat.v index 3fbfa1c2..7d9a7615 100644 --- a/examples/cat/cat.v +++ b/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.