Skip to content

Changes for Rocq PR#21164 #2318

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jdchristensen merged 4 commits into from
Oct 21, 2025
+11 −14
Merged

Changes for Rocq PR#21164 #2318

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
415ecb8
Meet: use apply instead of rapply for Rocq PR#21164
jdchristensen Oct 20, 2025
f831e6e
istrunc_truncation: use only one universe variable
jdchristensen Oct 20, 2025
cbbb2e8
if_not_hprop_then_equiv_Empty: remove unneeded HProp assumption
jdchristensen Oct 20, 2025
b2dfaef
HoTTBookExercises: make build with Rocq PR#21164
jdchristensen Oct 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion contrib/HoTTBookExercises.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1109,7 +1109,7 @@ Defined.
Definition Book_3_10_LEM@{j} := forall A : HProp@{j}, A + ~ A.

Definition Book_3_10_Lift@{i j | i < j} (A : HProp@{i}) : HProp@{j}
:= Build_HProp A.
:= @Build_HProp A (trunctype_istrunc A).

Definition Book_3_10_impred@{i j k | i < j, j < k} `{Univalence}
(LEM : Book_3_10_LEM@{j})
Expand Down
4 changes: 2 additions & 2 deletions theories/Algebra/Rings/Matrix.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -667,7 +667,7 @@ Class IsUpperTriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix@{i} R n n) : Ty
Instance ishprop_isuppertriangular@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
: IsHProp (IsUpperTriangular M).
Proof.
apply istrunc_truncation@{i i}.
apply istrunc_truncation@{i}.
Defined.

(** A matrix is lower triangular if all the entries above the diagonal are zero. We define it as the transpose being upper triangular. *)
Expand All @@ -678,7 +678,7 @@ Instance ishprop_islowertriangular@{i} {R : Ring@{i}} {n : nat}
(M : Matrix R n n)
: IsHProp (IsLowerTriangular M).
Proof.
apply istrunc_truncation@{i i}.
apply istrunc_truncation@{i}.
Defined.

(** The transpose of a matrix is lower triangular if and only if the matrix is upper triangular. *)
Expand Down
2 changes: 1 addition & 1 deletion theories/Modalities/Meet.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,7 @@ Section LexMeet.
apply mapinO_compose.
2:rapply mapinO_isequiv.
apply IHn.
- rapply mapinO_diagonal.
- apply mapinO_diagonal.
pose (O_eq_Tr n.+1).
rapply (mapinO_O_leq _ (Sep (Tr n.+1))).
- apply plusconnmap_diagonal; assumption.
Expand Down
6 changes: 3 additions & 3 deletions theories/Truncations/Core.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,9 @@ Module Export Trunc.
tr : A -> Trunc n A.
Arguments tr {n A} a.

(** Without explicit universe parameters, this instance is insufficiently polymorphic. *)
#[export] Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
: IsTrunc@{j} n (Trunc@{i} n A).
(** Because [IsTrunc] is cumulative, we can use only one universe variable here. *)
#[export] Instance istrunc_truncation@{i} (n : trunc_index) (A : Type@{i})
: IsTrunc@{i} n (Trunc@{i} n A).
Comment on lines +31 to +33
Copy link
Collaborator Author

@jdchristensen jdchristensen Oct 20, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We decided to make IsTrunc (really, IsTrunc_internal) cumulative, but this extra flexibility makes it harder for Rocq to choose universe variables optimally. E.g. with the original version of istrunc_truncation, there is not a unique choice of j, since anything smaller than the desired j will work. With this change, there is no longer the flexibility to choose j, making it easier for Rocq, but then Rocq can fail to find a solution in other situations. It's a bit of a dilemma, and we might end up making different design decisions once we have algebraic universes.

Admitted.

Definition Trunc_ind {n A}
Expand Down
2 changes: 1 addition & 1 deletion theories/Universes/DProp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ Proof.
- intros P; unfold dprop_to_bool.
destruct (dec P); symmetry; apply path_dprop, path_universe_uncurried.
+ apply if_hprop_then_equiv_Unit; [ exact _ | assumption ].
+ apply if_not_hprop_then_equiv_Empty; [ exact _ | assumption ].
+ apply if_not_hprop_then_equiv_Empty; assumption.
Defined.

Definition equiv_dprop_to_bool `{Univalence}
Expand Down
9 changes: 3 additions & 6 deletions theories/Universes/HProp.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -128,12 +128,9 @@ Proof.
- exact (fun _ => p).
Defined.

(** If an hprop is not inhabited, then it is equivalent to [Empty]. *)
Lemma if_not_hprop_then_equiv_Empty (hprop : Type) `{IsHProp hprop} : ~hprop -> hprop <~> Empty.
Proof.
intro np.
exact (Build_Equiv _ _ np _).
Defined.
(** If an hprop is not inhabited, then it is equivalent to [Empty]. Note that we'd don't need the assumption that the type is an hprop here. *)
Definition if_not_hprop_then_equiv_Empty (hprop : Type) : ~hprop -> hprop <~> Empty
:= equiv_to_empty.

(** Thus, a decidable hprop is either equivalent to [Unit] or [Empty]. *)
Definition equiv_decidable_hprop (hprop : Type)
Expand Down
Loading