Skip to content

Commit

Permalink
WIP: Make IsTrunc an inductive type
Browse files Browse the repository at this point in the history
  • Loading branch information
jdchristensen committed Jan 10, 2024
1 parent 191c10e commit 1dc29c3
Show file tree
Hide file tree
Showing 25 changed files with 156 additions and 145 deletions.
17 changes: 3 additions & 14 deletions theories/Basics/Contractible.v
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Definition path_contr `{Contr A} (x y : A) : x = y
(** Any space of paths in a contractible space is contractible. *)
Global Instance contr_paths_contr `{Contr A} (x y : A) : Contr (x = y) | 10000.
Proof.
exists (path_contr x y).
apply (Build_Contr _ (path_contr x y)).
intro r; destruct r; apply concat_Vp.
Defined.

Expand All @@ -37,7 +37,7 @@ Arguments path_basedpaths {X x y} p : simpl nomatch.

Global Instance contr_basedpaths {X : Type} (x : X) : Contr {y : X & x = y} | 100.
Proof.
exists (x;1).
apply (Build_Contr _ (x;1)).
intros [y p]; apply path_basedpaths.
Defined.

Expand Down Expand Up @@ -105,17 +105,6 @@ Definition contr_retract {X Y : Type} `{Contr X}
Definition contr_change_center {A : Type} (a : A) `{Contr A}
: Contr A.
Proof.
exists a.
apply (Build_Contr _ a).
intros; apply path_contr.
Defined.

(** If a type is contractible, then so is its type of contractions. *)
Global Instance contr_contr `{Funext} (A : Type) `{contrA : Contr A}
: Contr (Contr A) | 100.
Proof.
exists contrA; intros [a2 c2].
destruct (contr a2).
apply (ap (Build_Contr _ (center A))).
apply path_forall; intros x.
apply path2_contr.
Defined.
4 changes: 3 additions & 1 deletion theories/Basics/Decidable.v
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,7 @@ Defined.
Global Instance hset_pathcoll (A : Type) `{PathCollapsible A}
: IsHSet A | 1000.
Proof.
apply istrunc_S.
intros x y.
assert (h : forall p:x=y, p = (collapse (idpath x))^ @ collapse p).
{ intros []; symmetry; by apply concat_Vp. }
Expand Down Expand Up @@ -195,7 +196,8 @@ Global Instance ishprop_decpaths `{Funext} (A : Type)
Proof.
apply hprop_inhabited_contr; intros d.
assert (IsHSet A) by exact _.
exists d; intros d'.
apply (Build_Contr _ d).
intros d'.
apply path_forall; intros x; apply path_forall; intros y.
generalize (d x y); clear d; intros d.
generalize (d' x y); clear d'; intros d'.
Expand Down
2 changes: 1 addition & 1 deletion theories/Basics/Equivalences.v
Original file line number Diff line number Diff line change
Expand Up @@ -214,7 +214,7 @@ Definition moveL_equiv_V' `(f : A <~> B) (x : B) (y : A) (p : f y = x)
Lemma contr_equiv A {B} (f : A -> B) `{IsEquiv A B f} `{Contr A}
: Contr B.
Proof.
exists (f (center A)).
apply (Build_Contr _ (f (center A))).
intro y.
apply moveR_equiv_M.
apply contr.
Expand Down
91 changes: 44 additions & 47 deletions theories/Basics/Overture.v
Original file line number Diff line number Diff line change
Expand Up @@ -499,12 +499,7 @@ In order to achieve moderate coverage and speedy resolution, we currently follow
(** A space [A] is contractible if there is a point [x : A] and a (pointwise) homotopy connecting the identity on [A] to the constant map at [x]. Thus an element of [contr A] is a pair whose first component is a point [x] and the second component is a pointwise retraction of [A] to [x]. *)

(** We use the [Contr_internal] record so as not to pollute typeclass search; we only do truncation typeclass search on the [IsTrunc] datatype, usually. We will define a notation [Contr] which is equivalent to [Contr_internal], but picked up by typeclass search. However, we must make [Contr_internal] a class so that we pick up typeclasses on [center] and [contr]. However, the only typeclass rule we register is the one that turns it into a [Contr]/[IsTrunc]. Unfortunately, this means that declaring an instance like [Instance contr_foo : Contr foo := { center := bar }.] will fail with mismatched instances/contexts. Instead, we must iota expand such definitions to get around Coq's deficiencies, and write [Instance contr_foo : Contr foo := let x := {| center := bar |} in x.] *)
Class Contr_internal (A : Type) := Build_Contr {
center : A ;
contr : (forall y : A, center = y)
}.

Arguments center A {_}.
(** TODO: update comment. *)

(** *** Truncation levels *)

Expand Down Expand Up @@ -541,58 +536,60 @@ Local Open Scope trunc_scope.
(** Further notation for truncation levels is introducted in Trunc.v. *)

(** n-truncatedness is defined by recursion on [n]. We could simply define [IsTrunc] as a fixpoint and an [Existing Class], but we want to also declare [IsTrunc] to be [simpl nomatch], so that when we say [simpl] or [cbn], [IsTrunc n.+1 A] doesn't get unfolded to [forall x y:A, IsTrunc n (x = y)]. But we also want to be able to use this equality, e.g. by proving [IsTrunc n.+1 A] starting with [intros x y], and if [IsTrunc] is a fixpoint declared as [simpl nomatch] then that doesn't work, because [intros] uses [hnf] to expose a [forall] and [hnf] respects [simpl nomatch] on fixpoints. But we can make it work if we define the fixpoint separately as [IsTrunc_internal] and then take the class [IsTrunc] to be a definitional wrapper around it, since [hnf] is willing to unfold non-fixpoints even if they are defined as [simpl never]. This behavior of [hnf] is arguably questionable (see https://github.com/coq/coq/issues/11619), but it is useful for us here. *)
(** TODO: update comment. *)

Fixpoint IsTrunc_internal (n : trunc_index) (A : Type@{u}) : Type@{u} :=
match n with
| minus_two => Contr_internal A
| n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
end.
Cumulative Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).

Arguments IsTrunc_internal n A : simpl nomatch.

Class IsTrunc (n : trunc_index) (A : Type) : Type :=
Trunc_is_trunc : IsTrunc_internal n A.
Existing Class IsTrunc_internal.

(** We use the principle that we should always be doing typeclass resolution on truncation of non-equality types. We try to change the hypotheses and goals so that they never mention something like [IsTrunc n (_ = _)] and instead say [IsTrunc (S n) _]. If you're evil enough that some of your paths [a = b] are n-truncated, but others are not, then you'll have to either reason manually or add some (local) hints with higher priority than the hint below, or generalize your equality type so that it's not a path anymore. *)
Notation IsTrunc n A := (IsTrunc_internal A n).

#[global] Typeclasses Opaque IsTrunc. (* don't auto-unfold [IsTrunc] in typeclass search *)
Scheme IsTrunc_internal_ind := Induction for IsTrunc_internal Sort Type.
Scheme IsTrunc_internal_rec := Minimality for IsTrunc_internal Sort Type.
Definition IsTrunc_internal_rect := IsTrunc_internal_ind.

Arguments IsTrunc : simpl never. (* don't auto-unfold [IsTrunc] with [simpl] *)
Definition IsTrunc_unfolded (n : trunc_index) (A : Type)
:= match n with
| minus_two => { center : A & forall y, center = y }
| n.+1 => forall x y : A, IsTrunc n (x = y)
end.

Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A)
: IsTrunc n (x = y)
:= H x y. (* but do fold [IsTrunc] *)
Definition istrunc_unfold (n : trunc_index) (A : Type)
: IsTrunc n A -> IsTrunc_unfolded n A.
Proof.
intros [center contr|k istrunc].
- exact (center; contr).
- exact istrunc.
Defined.

Existing Class IsTrunc_internal.
Definition isequiv_istrunc_unfold (n : trunc_index) (A : Type)
: IsEquiv (istrunc_unfold n A).
Proof.
simple refine (Build_IsEquiv _ _ (istrunc_unfold n A) _ _ _ _).
- destruct n.
+ intros [center contr]; exact (Build_Contr _ center contr).
+ intros H. exact (istrunc_S _ H).
- destruct n; reflexivity.
- intros [center contr|k istrunc]; reflexivity.
- intros [center contr|k istrunc]; reflexivity.
Defined.

#[export]
Hint Extern 0 (IsTrunc_internal _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
Definition equiv_istrunc_unfold (n : trunc_index) (A : Type)
:= Build_Equiv _ _ _ (isequiv_istrunc_unfold n A).

#[export]
Hint Extern 0 (IsTrunc _ _) => progress change IsTrunc_internal with IsTrunc in * : typeclass_instances. (* Also fold [IsTrunc_internal] *)
(** A version of [istrunc_unfold] for successors. *)
Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A)
: IsTrunc n (x = y)
:= istrunc_unfold n.+1 A H x y.

(** Picking up the [forall x y, IsTrunc n (x = y)] instances in the hypotheses is much tricker. We could do something evil where we declare an empty typeclass like [IsTruncSimplification] and use the typeclass as a proxy for allowing typeclass machinery to factor nested [forall]s into the [IsTrunc] via backward reasoning on the type of the hypothesis... but, that's rather complicated, so we instead explicitly list out a few common cases. It should be clear how to extend the pattern. *)
#[export]
Hint Extern 10 =>
progress match goal with
| [ H : forall x y : ?T, IsTrunc ?n (x = y) |- _ ]
=> change (IsTrunc n.+1 T) in H
| [ H : forall (a : ?A) (x y : @?T a), IsTrunc ?n (x = y) |- _ ]
=> change (forall a : A, IsTrunc n.+1 (T a)) in H; cbv beta in H
| [ H : forall (a : ?A) (b : @?B a) (x y : @?T a b), IsTrunc ?n (x = y) |- _ ]
=> change (forall (a : A) (b : B a), IsTrunc n.+1 (T a b)) in H; cbv beta in H
| [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (x y : @?T a b c), IsTrunc ?n (x = y) |- _ ]
=> change (forall (a : A) (b : B a) (c : C a b), IsTrunc n.+1 (T a b c)) in H; cbv beta in H
| [ H : forall (a : ?A) (b : @?B a) (c : @?C a b) (d : @?D a b c) (x y : @?T a b c d), IsTrunc ?n (x = y) |- _ ]
=> change (forall (a : A) (b : B a) (c : C a b) (d : D a b c), IsTrunc n.+1 (T a b c d)) in H; cbv beta in H
end : core.

Notation Contr := (IsTrunc minus_two).
Notation IsHProp := (IsTrunc minus_two.+1).
Notation IsHSet := (IsTrunc minus_two.+2).
Notation Contr A := (IsTrunc minus_two A).
Notation IsHProp A := (IsTrunc minus_two.+1 A).
Notation IsHSet A := (IsTrunc minus_two.+2 A).

#[export]
Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
Definition center (A : Type) {H : Contr A} : A := pr1 (istrunc_unfold _ _ H).
Definition contr {A : Type} {H : Contr A} (y : A) : center A = y := pr2 (istrunc_unfold _ _ H) y.

(** *** Truncated relations *)

Expand Down
6 changes: 0 additions & 6 deletions theories/Basics/Tactics.v
Original file line number Diff line number Diff line change
Expand Up @@ -733,12 +733,6 @@ Ltac issig :=

(** We show how the tactic works in a couple of examples. *)

Definition issig_contr (A : Type)
: {x : A & forall y, x = y} <~> Contr A.
Proof.
issig.
Defined.

Definition issig_equiv (A B : Type)
: {f : A -> B & IsEquiv f} <~> Equiv A B.
Proof.
Expand Down
85 changes: 54 additions & 31 deletions theories/Basics/Trunc.v
Original file line number Diff line number Diff line change
Expand Up @@ -279,13 +279,20 @@ Definition contr_istrunc_minus_two `{H : IsTrunc (-2) A} : Contr A
:= H.

(** Truncation levels are cumulative. *)
Global Instance istrunc_succ `{IsTrunc n A}
: IsTrunc n.+1 A | 1000.
Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
: forall x y : A, IsTrunc n (x = y) | 1000.
Proof.
generalize dependent A.
simple_induction n n IH; simpl; intros A H x y.
- apply contr_paths_contr.
- apply IH, H.
- apply istrunc_S. rapply IH.
Defined.

Global Instance istrunc_succ {n : trunc_index} {A : Type} `{IsTrunc n A}
: IsTrunc n.+1 A | 1000.
Proof.
apply istrunc_S.
apply istrunc_paths'.
Defined.

(** This could be an [Instance] (with very high priority, so it doesn't get applied trivially). However, we haven't given typeclass search any hints allowing it to solve goals like [m <= n], so it would only ever be used trivially. *)
Expand All @@ -298,8 +305,9 @@ Proof.
- (* -2, -2 *) assumption.
- (* S m', -2 *) destruct Hmn.
- (* -2, S n' *) apply @istrunc_succ, (IH (-2)); auto.
- (* S m', S n' *) intros x y; apply (IH m');
auto with typeclass_instances.
- (* S m', S n' *)
apply istrunc_S.
intros x y; apply (IH m'); auto with typeclass_instances.
Defined.

(** In particular, a contractible type, hprop, or hset is truncated at all higher levels. We don't allow these to be used as idmaps, since there would be no point to it. *)
Expand All @@ -321,15 +329,15 @@ Definition istrunc_hset {n} {A} `{IsHSet A}

(** Equivalence preserves truncation (this is, of course, trivial with univalence). This is not an [Instance] because it causes infinite loops. *)
Definition istrunc_isequiv_istrunc A {B} (f : A -> B)
`{IsTrunc n A} `{IsEquiv A B f}
`{H : IsTrunc n A} `{IsEquiv A B f}
: IsTrunc n B.
Proof.
generalize dependent B; generalize dependent A.
simple_induction n n IH; simpl; intros A ? B f ?.
- exact (contr_equiv _ f).
- intros x y.
exact (IH (f^-1 x = f^-1 y) (H (f^-1 x) (f^-1 y))
(x = y) ((ap (f^-1))^-1) _).
- apply istrunc_S.
intros x y.
refine (IH _ _ _ (ap (f^-1))^-1 _).
Defined.

Definition istrunc_equiv_istrunc A {B} (f : A <~> B) `{IsTrunc n A}
Expand Down Expand Up @@ -377,16 +385,16 @@ Canonical Structure default_TruncType := fun n T P => (@Build_TruncType n T P).
Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A)
: Contr A.
Proof.
exists x.
apply (Build_Contr _ x).
intro y.
apply center, H.
rapply center.
Defined.

(** If inhabitation implies contractibility, then we have an h-proposition. We probably won't often have a hypothesis of the form [A -> Contr A], so we make sure we give priority to other instances. *)
Global Instance hprop_inhabited_contr (A : Type)
: (A -> Contr A) -> IsHProp A | 10000.
Proof.
intros H x y.
intros H; apply istrunc_S; intros x y.
pose (C := H x).
apply contr_paths_contr.
Defined.
Expand All @@ -395,15 +403,17 @@ Defined.
Theorem path_ishprop `{H : IsHProp A}
: forall x y : A, x = y.
Proof.
apply H.
intros x y.
rapply center.
Defined.

(** Conversely, this property characterizes hprops. *)
Theorem hprop_allpath (A : Type)
: (forall (x y : A), x = y) -> IsHProp A.
intros H x y.
pose (C := Build_Contr A x (H x)).
apply contr_paths_contr.
Proof.
intros H; apply istrunc_S; intros x y.
nrapply contr_paths_contr.
exact (Build_Contr _ x (H x)).
Defined.

(** Two propositions are equivalent as soon as there are maps in both directions. *)
Expand Down Expand Up @@ -435,29 +445,31 @@ Proof.
- rapply contr_inhabited_hprop.
Defined.

Corollary equiv_contr_hprop (A : Type) `{Funext} `{IsHProp A}
: Contr A <~> A.
Proof.
exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
Defined.

(** Truncatedness is an hprop. *)
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A) | 0.
Proof.
apply hprop_inhabited_contr.
revert A.
simple_induction n n IH; unfold IsTrunc; simpl.
- intros A ?.
exact _.
simple_induction n n IH.
- intros A ContrA.
nrapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold (-2) A)^-1%equiv).
destruct (istrunc_unfold (-2) A ContrA) as [a1 c1].
snrapply (Build_Contr _ (a1; c1)).
intros [a2 c2].
destruct (c1 a2).
apply (ap (exist _ a1)).
funext x.
apply path2_contr.
- intros A AH1.
exists AH1.
nrapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold n.+1 A)^-1%equiv).
cbn.
pose (AH1' := (equiv_istrunc_unfold n.+1 A AH1)).
apply (Build_Contr _ AH1').
intro AH2.
apply path_forall; intro x.
apply path_forall; intro y.
apply @path_contr.
apply IH, AH1.
Qed.
funext x y.
apply path_contr.
Defined.

(** By [trunc_hprop], it follows that [IsTrunc n A] is also [m]-truncated for any [m >= -1]. *)

Expand All @@ -470,4 +482,15 @@ Proof.
apply path_ishprop.
Defined.

(** If a type [A] is [n]-truncated, then [IsTrunc n A] is contractible. *)
Global Instance contr_istrunc `{Funext} (n : trunc_index) (A : Type) `{istruncA : IsTrunc n A}
: Contr (IsTrunc n A) | 100
:= contr_inhabited_hprop _ _.

Corollary equiv_contr_hprop (A : Type) `{Funext} `{IsHProp A}
: Contr A <~> A.
Proof.
exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
Defined.

(** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)
1 change: 1 addition & 0 deletions theories/Categories/Category/Sum.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
(** * The coproduct of categories *)
Require Export Category.Core.
Require Import Types.Empty.

Set Universe Polymorphism.
Set Implicit Arguments.
Expand Down
2 changes: 1 addition & 1 deletion theories/Colimits/Pushout.v
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ Global Instance contr_pushout {A B C : Type} `{Contr A, Contr B, Contr C}
(f : A -> B) (g : A -> C)
: Contr (Pushout f g).
Proof.
exists (pushl (center B)).
apply (Build_Contr _ (pushl (center B))).
srapply Pushout_ind.
- intros b; apply ap, path_contr.
- intros c.
Expand Down
3 changes: 2 additions & 1 deletion theories/HFiber.v
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,8 @@ Global Instance istruncmap_ap {A B} n (f:A -> B) `{!IsTruncMap n.+1 f}
Definition istruncmap_from_ap {A B} n (f:A -> B) `{!forall x y, IsTruncMap n (@ap _ _ f x y)}
: IsTruncMap n.+1 f.
Proof.
intros y [a p] [b q];
intro y; apply istrunc_S.
intros [a p] [b q];
destruct q;
exact (istrunc_equiv_istrunc _ (hfiber_ap p)).
Defined.
Expand Down
2 changes: 1 addition & 1 deletion theories/HIT/Interval.v
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ Defined.

Global Instance contr_interval : Contr interval | 0.
Proof.
exists zero.
apply (Build_Contr _ zero).
refine (interval_ind _ 1 seg _).
refine (transport_paths_r _ _ @ concat_1p _).
Defined.
Loading

0 comments on commit 1dc29c3

Please sign in to comment.