Timings for Trunc.v
(* -*- mode: coq; mode: visual-line -*- *)
(** * Truncatedness *)
Require Import
Basics.Overture
Basics.Contractible
Basics.Equivalences
Basics.Tactics
Basics.Nat.
Local Set Universe Minimization ToSet.
Local Open Scope trunc_scope.
Local Open Scope path_scope.
Generalizable Variables A B m n f.
(** Notation for truncation-levels. *)
(* Increase a truncation index by a natural number. *)
Fixpoint trunc_index_inc@{} (k : trunc_index) (n : nat)
: trunc_index
:= match n with
| O => k
| S m => (trunc_index_inc k m).+1
end.
(* This is a variation that inserts the successor operations in the other order. This is sometimes convenient. *)
Fixpoint trunc_index_inc'@{} (k : trunc_index) (n : nat)
: trunc_index
:= match n with
| O => k
| S m => (trunc_index_inc' k.+1 m)
end.
Definition trunc_index_inc'_succ@{} (n : nat) (k : trunc_index)
: trunc_index_inc' k.+1 n = (trunc_index_inc' k n).+1.
revert k; simple_induction n n IHn; intro k.
Definition trunc_index_inc_agree@{} (k : trunc_index) (n : nat)
: trunc_index_inc k n = trunc_index_inc' k n.
simple_induction n n IHn.
symmetry; apply trunc_index_inc'_succ.
Definition nat_to_trunc_index@{} (n : nat) : trunc_index
:= (trunc_index_inc minus_two n).+2.
Coercion nat_to_trunc_index : nat >-> trunc_index.
Definition trunc_index_inc'_0n (n : nat)
: trunc_index_inc' 0%nat n = n.
refine (trunc_index_inc'_succ _ _ @ _).
Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index
:= match v with
| Decimal.Pos d => Some (nat_to_trunc_index (Nat.of_uint d))
| Decimal.Neg d => match Nat.of_uint d with
| 2%nat => Some minus_two
| 1%nat => Some (minus_two.+1)
| 0%nat => Some (minus_two.+2)
| _ => None
end
end.
Definition num_int_to_trunc_index@{} (v : Numeral.int) : option trunc_index :=
match v with
| Numeral.IntDec v => int_to_trunc_index v
| Numeral.IntHex _ => None
end.
Fixpoint trunc_index_to_little_uint@{} n acc :=
match n with
| minus_two => acc
| minus_two.+1 => acc
| minus_two.+2 => acc
| trunc_S n => trunc_index_to_little_uint n (Decimal.Little.succ acc)
end.
Definition trunc_index_to_int@{} n :=
match n with
| minus_two => Decimal.Neg (Nat.to_uint 2)
| minus_two.+1 => Decimal.Neg (Nat.to_uint 1)
| n => Decimal.Pos (Decimal.rev (trunc_index_to_little_uint n Decimal.zero))
end.
Definition trunc_index_to_num_int@{} n :=
Numeral.IntDec (trunc_index_to_int n).
Number Notation trunc_index num_int_to_trunc_index trunc_index_to_num_int
: trunc_scope.
(** ** Arithmetic on truncation-levels. *)
Fixpoint trunc_index_add@{} (m n : trunc_index) : trunc_index
:= match m with
| -2 => n
| m'.+1 => (trunc_index_add m' n).+1
end.
Notation "m +2+ n" := (trunc_index_add m n) : trunc_scope.
Definition trunc_index_add_minus_two@{} m
: m +2+ -2 = m.
simple_induction m m IHm.
Definition trunc_index_add_succ@{} m n
: m +2+ n.+1 = (m +2+ n).+1.
revert m; simple_induction n n IHn; intro m; simple_induction m m IHm.
Definition trunc_index_add_comm@{} m n
: m +2+ n = n +2+ m.
simple_induction n n IHn.
apply trunc_index_add_minus_two.
exact (trunc_index_add_succ _ _ @ ap trunc_S IHn).
Fixpoint trunc_index_leq@{} (m n : trunc_index) : Type0
:= match m, n with
| -2, _ => Unit
| m'.+1, -2 => Empty
| m'.+1, n'.+1 => trunc_index_leq m' n'
end.
Existing Class trunc_index_leq.
Notation "m <= n" := (trunc_index_leq m n) : trunc_scope.
Global Instance trunc_index_leq_minus_two_n@{} n : -2 <= n := tt.
Global Instance trunc_index_leq_succ@{} n : n <= n.+1.
by induction n as [|n IHn] using trunc_index_ind.
Definition trunc_index_pred@{} : trunc_index -> trunc_index.
Notation "n '.-1'" := (trunc_index_pred n) : trunc_scope.
Notation "n '.-2'" := (n.-1.-1) : trunc_scope.
Definition trunc_index_succ_pred@{} (n : nat)
: (n.-1).+1 = n.
simple_induction n n IHn.
unfold nat_to_trunc_index in *; cbn in *.
Definition trunc_index_leq_minus_two@{} {n}
: n <= -2 -> n = -2.
Definition trunc_index_leq_succ'@{} n m
: n <= m -> n <= m.+1.
induction n as [|n IHn] using trunc_index_ind.
induction m as [|m IHm] using trunc_index_ind.
Global Instance trunc_index_leq_refl@{}
: Reflexive trunc_index_leq.
by induction n as [|n IHn] using trunc_index_ind.
Global Instance trunc_index_leq_transitive@{}
: Transitive trunc_index_leq.
induction b as [|b IHb] using trunc_index_ind.
by destruct (trunc_index_leq_minus_two p).
induction a as [|a IHa] using trunc_index_ind;
induction c as [|c IHc] using trunc_index_ind.
Definition trunc_index_leq_add@{} n m
: n <= m +2+ n.
simple_induction m m IHm.
rapply trunc_index_leq_transitive.
Definition trunc_index_leq_add'@{} n m
: n <= n +2+ m.
rewrite trunc_index_add_comm.
apply trunc_index_leq_add.
Fixpoint trunc_index_min@{} (n m : trunc_index)
: trunc_index.
exact (trunc_index_min n m).+1.
Definition trunc_index_min_minus_two@{} n
: trunc_index_min n (-2) = -2.
Definition trunc_index_min_swap@{} n m
: trunc_index_min n m = trunc_index_min m n.
simple_induction n n IHn; intro m.
apply trunc_index_min_minus_two.
simple_induction m m IHm.
Definition trunc_index_min_path@{} n m
: (trunc_index_min n m = n) + (trunc_index_min n m = m).
revert m; simple_induction n n IHn; intro m.
simple_induction m m IHm.
Definition trunc_index_min_leq_left@{} (n m : trunc_index)
: trunc_index_min n m <= n.
refine (trunc_index_ind _ _ _); [ | intros n IHn ].
all: refine (trunc_index_ind _ _ _); [ | intros m IHm ].
Definition trunc_index_min_leq_right@{} (n m : trunc_index)
: trunc_index_min n m <= m.
refine (trunc_index_ind _ _ _); [ | intros n IHn ].
all: refine (trunc_index_ind _ _ _); [ | intros m IHm ].
(** ** Truncatedness proper. *)
(** A contractible space is (-2)-truncated, by definition. This function is the identity, so there is never any need to actually use it, but it exists to be found in searches. *)
Definition contr_istrunc_minus_two `{H : IsTrunc (-2) A} : Contr A
:= H.
(** Truncation levels are cumulative. *)
Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
: forall x y : A, IsTrunc n (x = y) | 1000.
simple_induction n n IH; simpl; intros A H x y.
Global Instance istrunc_succ {n : trunc_index} {A : Type} `{IsTrunc n A}
: IsTrunc n.+1 A | 1000.
(** 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. *)
Definition istrunc_leq {m n} (Hmn : m <= n) `{IsTrunc m A}
: IsTrunc n A.
generalize dependent A; generalize dependent m.
simple_induction n n' IH;
intros [ | m'] Hmn A ? .
apply @istrunc_succ, (IH (-2)); auto.
intros x y; apply (IH m'); auto with typeclass_instances.
(** 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. *)
Definition istrunc_contr {n} {A} `{Contr A} : IsTrunc n.+1 A
:= (@istrunc_leq (-2) n.+1 tt _ _).
Definition istrunc_hprop {n} {A} `{IsHProp A} : IsTrunc n.+2 A
:= (@istrunc_leq (-1) n.+2 tt _ _).
Definition istrunc_hset {n} {A} `{IsHSet A}
: IsTrunc n.+3 A
:= (@istrunc_leq 0 n.+3 tt _ _).
(** Consider the preceding definitions as instances for typeclass search, but only if the requisite hypothesis is already a known assumption; otherwise they result in long or interminable searches. *)
#[export] Hint Immediate istrunc_contr : typeclass_instances.
#[export] Hint Immediate istrunc_hprop : typeclass_instances.
#[export] Hint Immediate istrunc_hset : typeclass_instances.
(** 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}
: IsTrunc n B.
generalize dependent B; generalize dependent A.
simple_induction n n IH; simpl; intros A ? B f ?.
refine (IH _ _ _ (ap (f^-1))^-1 _).
Definition istrunc_equiv_istrunc A {B} (f : A <~> B) `{IsTrunc n A}
: IsTrunc n B
:= istrunc_isequiv_istrunc A f.
(** ** Truncated morphisms *)
Class IsTruncMap (n : trunc_index) {X Y : Type} (f : X -> Y)
:= istruncmap_fiber : forall y:Y, IsTrunc n (hfiber f y).
Global Existing Instance istruncmap_fiber.
Notation IsEmbedding := (IsTruncMap (-1)).
(** ** Universes of truncated types *)
(** It is convenient for some purposes to consider the universe of all n-truncated types (within a given universe of types). In particular, this allows us to state the important fact that each such universe is itself (n+1)-truncated. *)
Record TruncType (n : trunc_index) := {
trunctype_type : Type ;
trunctype_istrunc : IsTrunc n trunctype_type
}.
Arguments Build_TruncType _ _ {_}.
Arguments trunctype_type {_} _.
Arguments trunctype_istrunc [_] _.
Coercion trunctype_type : TruncType >-> Sortclass.
Global Existing Instance trunctype_istrunc.
Notation "n -Type" := (TruncType n) : type_scope.
Notation HProp := (-1)-Type.
Notation Build_HProp := (Build_TruncType (-1)).
Notation Build_HSet := (Build_TruncType 0).
(** This is (as of October 2014) the only [Canonical Structure] in the library. It would be nice to do without it, in the interests of minimizing the number of fancy Coq features that the reader needs to know about. *)
Canonical Structure default_TruncType := fun n T P => (@Build_TruncType n T P).
(** ** Facts about hprops *)
(** An inhabited proposition is contractible. This is not an [Instance] because it causes infinite loops. *)
Lemma contr_inhabited_hprop (A : Type) `{H : IsHProp A} (x : A)
: Contr A.
(** 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.
intros H; apply istrunc_S; intros x y.
(** Any two points in an hprop are connected by a path. *)
Theorem path_ishprop `{H : IsHProp A}
: forall x y : A, x = y.
(** Conversely, this property characterizes hprops. *)
Theorem hprop_allpath (A : Type)
: (forall (x y : A), x = y) -> IsHProp A.
intros H; apply istrunc_S; intros x y.
nrapply contr_paths_contr.
exact (Build_Contr _ x (H x)).
(** Two propositions are equivalent as soon as there are maps in both directions. *)
Definition isequiv_iff_hprop `{IsHProp A} `{IsHProp B}
(f : A -> B) (g : B -> A)
: IsEquiv f.
apply (isequiv_adjointify f g);
intros ?; apply path_ishprop.
Definition equiv_iff_hprop_uncurried `{IsHProp A} `{IsHProp B}
: (A <-> B) -> (A <~> B).
apply (equiv_adjointify (fst fg) (snd fg));
intros ?; apply path_ishprop.
Definition equiv_iff_hprop `{IsHProp A} `{IsHProp B}
: (A -> B) -> (B -> A) -> (A <~> B)
:= fun f g => equiv_iff_hprop_uncurried (f, g).
Corollary iff_contr_hprop (A : Type) `{IsHProp A}
: Contr A <-> A.
rapply contr_inhabited_hprop.
(** ** Truncatedness: any dependent product of n-types is an n-type *)
Definition contr_forall `{Funext} `{P : A -> Type} `{forall a, Contr (P a)}
: Contr (forall a, P a).
apply (Build_Contr _ (fun a => center (P a))).
Global Instance istrunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)}
: IsTrunc n (forall a, P a) | 100.
simple_induction n n IH; simpl; intros P ?.
(* case [n = -2], i.e. contractibility *)
intros f g; apply (istrunc_isequiv_istrunc@{u1 u1} _ (apD10@{_ _ u1} ^-1)).
(** Truncatedness is an hprop. *)
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A) | 0.
revert A; simple_induction n n IH; cbn; intro A.
nrapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold (-2) A)^-1%equiv).
pose (Build_Contr _ a1 c1); apply path2_contr.
rapply (istrunc_equiv_istrunc _ (equiv_istrunc_unfold n.+1 A)^-1%equiv).
(* This case follows from [istrunc_forall]. *)
(** By [trunc_hprop], it follows that [IsTrunc n A] is also [m]-truncated for any [m >= -1]. *)
(** Similarly, a map being truncated is also a proposition. *)
Global Instance ishprop_istruncmap `{Funext} (n : trunc_index) {X Y : Type} (f : X -> Y)
: IsHProp (IsTruncMap n f).
apply hprop_allpath; intros s t.
apply path_forall; intros x.
(** 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.
exact (equiv_iff_hprop_uncurried (iff_contr_hprop A)).
(** If you are looking for a theorem about truncation, you may want to read the note "Finding Theorems" in "STYLE.md". *)