Skip to content
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.

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

Try to make entire library Cumulative #1710

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 1 commit
Commits
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
Prev Previous commit
Mild progress on cumulative inductives
  • Loading branch information
jdchristensen committed Feb 16, 2024
commit 4666c4bbff87c7761b865cbb2cc6bd378ee955fe
2 changes: 1 addition & 1 deletion theories/Algebra/Universal/Homomorphism.v
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Section is_homomorphism.
Qed.
End is_homomorphism.

(* We make this NonCumulative so that the proof of [homomorphism_id] goes through smoothly. *)
(* We make this NonCumulative so that the proof of [homomorphism_id] goes through smoothly. TODO: remove this. *)
NonCumulative Record Homomorphism {σ} {A B : Algebra σ} : Type := Build_Homomorphism
{ def_homomorphism : forall (s : Sort σ), A s -> B s
; is_homomorphism : IsHomomorphism def_homomorphism }.
Expand Down
1 change: 1 addition & 0 deletions theories/HIT/quotient.v
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,8 @@
intros. eapply concat;[apply transport_const|].
apply path_forall. intro z. apply path_hprop; simpl.
apply @equiv_iff_hprop; eauto.
(** Some universe annotations needed above for typeclass instance istrunc_trunctype. *)
Defined.

Check failure on line 88 in theories/HIT/quotient.v

View workflow job for this annotation

GitHub Actions / opam-build (latest, ubuntu-latest)

Illegal application:

Check failure on line 88 in theories/HIT/quotient.v

View workflow job for this annotation

GitHub Actions / opam-build (supported, ubuntu-latest)

Illegal application:

Check failure on line 88 in theories/HIT/quotient.v

View workflow job for this annotation

GitHub Actions / opam-build (8.17, ubuntu-latest)

Illegal application:

Check failure on line 88 in theories/HIT/quotient.v

View workflow job for this annotation

GitHub Actions / opam-build (dev, ubuntu-latest)

Illegal application:

Context {Hrefl : Reflexive R}.

Expand Down
3 changes: 2 additions & 1 deletion theories/Modalities/Accessible.v
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ Coercion lgenerator : LocalGenerators >-> Funclass.

(** We put this definition in a module so that no one outside of this file will use it accidentally. It will be redefined in [Localization] to refer to the localization reflective subuniverse, which is judgmentally the same but will also pick up typeclass inference for [In]. *)
Module Import IsLocal_Internal.
Definition IsLocal f X :=
(* TODO: reorder these universe variables; make it land in v. Currently done this way for backwards compatibility, to keep diff small. *)
Definition IsLocal@{u v a | u <= v, a <= v} (f : LocalGenerators@{a}) (X : Type@{u}) :=
(forall (i : lgen_indices f), ooExtendableAlong (f i) (fun _ => X)).
End IsLocal_Internal.

Expand Down
4 changes: 2 additions & 2 deletions theories/Modalities/Localization.v
Original file line number Diff line number Diff line change
Expand Up @@ -337,7 +337,7 @@ Section Localization.

End Localization.

Definition Loc@{a i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}.
Definition Loc@{a i | a <= i} (f : LocalGenerators@{a}) : ReflectiveSubuniverse@{i}.
Proof.
snrefine (Build_ReflectiveSubuniverse
(Build_Subuniverse (IsLocal f) _ _)
Expand Down Expand Up @@ -422,7 +422,7 @@ Proof.
Defined.

(** Conversely, if a subuniverse is accessible, then the corresponding localization subuniverse is equivalent to it, and moreover exists at every universe level and satisfies its computation rules judgmentally. This is called [lift_accrsu] but in fact it works equally well to *lower* the universe level, as long as both levels are no smaller than the size [a] of the generators. *)
Definition lift_accrsu@{a i j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
Definition lift_accrsu@{a i j | a <= i, a <= j} (O : Subuniverse@{i}) `{IsAccRSU@{a i} O}
: ReflectiveSubuniverse@{j}
:= Loc@{a j} (acc_lgen O).

Expand Down
9 changes: 5 additions & 4 deletions theories/TruncType.v
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,9 @@ Section TruncType.
: (A <~> B) <~> (A = B :> TruncType n)
:= equiv_path_trunctype' _ _ oE equiv_path_universe _ _.

Definition path_trunctype@{a b} {n : trunc_index} {A B : TruncType n}
Definition path_trunctype {n : trunc_index} {A B : TruncType n}
: A <~> B -> (A = B :> TruncType n)
:= equiv_path_trunctype@{a b} A B.
:= equiv_path_trunctype A B.

Global Instance isequiv_path_trunctype {n : trunc_index} {A B : TruncType n}
: IsEquiv (@path_trunctype n A B) := _.
Expand Down Expand Up @@ -99,7 +99,7 @@ Section TruncType.
Proof.
apply istrunc_S.
intros A B.
refine (istrunc_equiv_istrunc _ (equiv_path_trunctype@{i j} A B)).
refine (istrunc_equiv_istrunc _ (equiv_path_trunctype A B)).
case n as [ | n'].
- apply contr_equiv_contr_contr. (* The reason is different in this case. *)
- apply istrunc_equiv.
Expand All @@ -110,7 +110,8 @@ Section TruncType.
Global Instance istrunc_sig_istrunc : forall n, IsTrunc n.+1 { A : Type & IsTrunc n A } | 0.
Proof.
intro n.
apply (istrunc_equiv_istrunc _ issig_trunctype^-1).
nrefine (istrunc_equiv_istrunc _ issig_trunctype^-1).
exact istrunc_trunctype. (* To get universe variables to match, we do this as a separate step. *)
Defined.

(** ** Some standard inhabitants *)
Expand Down
Loading