Library HoTT.Misc.CompactTypes

Properties of compact and searchable types


From HoTT Require Import Basics Types.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Spaces.Nat.Core Finite.Fin.
Require Import Misc.UStructures BoundedSearch.
Require Import Spaces.NatSeq.Core Spaces.NatSeq.UStructure.
Require Import Homotopy.Suspension.
Require Import Pointed.Core.
Require Import Universes.TruncType Universes.HProp.
Require Import ExcludedMiddle Projective.

Local Open Scope nat_scope.
Local Open Scope pointed_scope.

Basic definitions of compact types

A type A is Sigma-compact if for every decidable family over A, the Σ-type is decidable. We generally drop the "Sigma" from the name in prose.
Definition IsSigmaCompact (A : Type)
  := ∀ P : A → Type, (∀ a : A, Decidable (P a)) → Decidable (sig P).

It is enough to consider HProp-valued families.
Definition IsSigmaCompactProps (A : Type)
  := ∀ P : A → HProp,
      (∀ a : A, Decidable (P a)) → Decidable (sig P).

Definition issigmacompactprops_issigmacompact {A : Type}
  (h : IsSigmaCompact A)
  : IsSigmaCompactProps A
  := h.

Definition issigmacompact_issigmacompactprops {A : Type}
  (h : IsSigmaCompactProps A)
  : IsSigmaCompact A.
Proof.
  intros P hP.
  refine (decidable_iff _ (h (merely o P) _)).
  apply iff_functor_sigma; intro a.
  exact merely_inhabited_iff_inhabited_stable.
Defined.

A weaker definition: a type is ∃-compact if for any decidable family, the propositional truncation of the Σ-type is decidable.
Definition IsHExistsCompact (A : Type)
  := ∀ P : A → Type,
      (∀ a : A, Decidable (P a)) → Decidable (hexists P).

Definition ishprop_ishexistscompact `{Funext} (A : Type)
  : IsHProp (IsHExistsCompact A) := _.

Sigma-compactness implies exists-compactness.
Definition ishexistscompact_issigmacompact {A} (c : IsSigmaCompact A)
  : IsHExistsCompact A.
Proof.
  intros P dP.
  destruct (c P dP) as [l|r].
  - left; exact (tr l).
  - right; intros u; by strip_truncations.
Defined.

An even weaker definition: a type is Π-compact if for any decidable family, the dependent function type is decidable.
Definition IsPiCompact (A : Type)
  := ∀ (P : A → Type) (dP : ∀ a : A, Decidable (P a)),
      Decidable (∀ a : A, P a).

It is enough to consider HProp-valued families.
Definition IsPiCompactProps (A : Type)
  := ∀ P : A → HProp,
      (∀ a, Decidable (P a)) → Decidable (∀ a, P a).

Definition ishprop_ispicompactprops `{Funext} (A : Type)
  : IsHProp (IsPiCompactProps A) := _.

Definition ispicompactprops_ispicompact {A} (h : IsPiCompact A)
  : IsPiCompactProps A := h.

Definition ispicompact_ispicompactprops {A} (h : IsPiCompactProps A)
  : IsPiCompact A.
Proof.
  intros P dP.
  refine (decidable_iff _ (h (merely o P) _)); split.
  2: exact (fun f a ⇒ tr (f a)).
  intros f a.
  apply merely_inhabited_iff_inhabited_stable; exact (f a).
Defined.

exists-compactness implies Pi-compactness.
Definition ispicompact_ishexistscompact {A} (c : IsHExistsCompact A)
  : IsPiCompact A.
Proof.
  intros P dP.
  destruct (c (not o P) _) as [l|r].
  - right; intro f; strip_truncations.
    exact (l.2 (f l.1)).
  - left; intro a.
    apply (stable_decidable (P a)).
    exact (fun u ⇒ r (tr (a; u))).
Defined.

Therefore, compactness implies Pi-compactness.
Definition ispicompact_issigmacompact {A} (c : IsSigmaCompact A)
  : IsPiCompact A
  := (ispicompact_ishexistscompact (ishexistscompact_issigmacompact c)).

Compact types are closed under retracts.
Definition issigmacompact_retract {A R : Type} {f : A → R} {g : R → A}
  (s : f o g == idmap) (c : IsSigmaCompact A)
  : IsSigmaCompact R.
Proof.
  intros P dP; destruct (c (P o f) _) as [u|v].
  1: left; exact (f u.1; u.2).
  right; intros [r pr].
  apply v.
  ∃ (g r).
  exact ((s r)^ # pr).
Defined.

Definition issigmacompact_equiv {A B : Type} (f : A → B) `{!IsEquiv f}
  (c : IsSigmaCompact B)
  : IsSigmaCompact A
  := issigmacompact_retract (eissect f) c.

Any compact type is decidable.
Definition decidable_issigmacompact {A : Type} (c : IsSigmaCompact A)
  : Decidable A.
Proof.
  destruct (c (fun (_ : A) ⇒ Unit) _) as [c1|c2].
  - exact (inl c1.1).
  - right; intro a.
    exact (c2 (a; pt)).
Defined.

Any ∃-compact type has decidable propositional truncation.
Definition decidable_tr_ishexistscompact {A : Type} (c : IsHExistsCompact A)
  : Decidable (Tr (-1) A).
Proof.
  refine (decidable_equiv' (hexists (fun _ ⇒ Unit)) _ (c _ _)).
  apply Trunc_functor_equiv.
  rapply equiv_sigma_contr.
Defined.

The negation of any Π-compact type is decidable.
Definition decidable_not_ispicompact {A} (h : IsPiCompact A)
  : Decidable (¬A)
  := h (const False_hp) _.

Equivalent definitions

A type A is compact if for every decidable predicate P on A we can either find an element of A making P false or we can show that P a always holds.
Definition IsCompact (A : Type)
  := ∀ P : A → Type, (∀ a : A, Decidable (P a)) →
                              {a : A & ¬ P a} + (∀ a : A, P a).

Compactness is equivalent to assuming the same for HProp-valued decidable predicates.
Definition IsCompactProps (A : Type)
  := ∀ P : A → HProp, (∀ a : A, Decidable (P a)) →
                              {a : A & ¬ P a} + (∀ a : A, P a).

Definition iscompact_iscompactprops {A} (c : IsCompactProps A) : IsCompact A.
Proof.
  intros P dP.
  destruct (c (merely o P) _) as [l|r].
  - exact (inl (l.1; fun p ⇒ l.2 (tr p))).
  - right.
    intro a.
    apply merely_inhabited_iff_inhabited_stable, r.
Defined.

Since decidable types are stable, it's also equivalent to negate P in the definition. We use this as an intermediate notion to show that IsCompact and IsSigmaCompact are logically equivalent.
Definition IsCompact' (A : Type)
  := ∀ P : A → Type, (∀ a : A, Decidable (P a)) →
                              {a : A & P a} + (∀ a : A, ¬ P a).

Definition iff_iscompact_iscompact' (A : Type)
  : IsCompact A ↔ IsCompact' A.
Proof.
  split;
    napply (functor_forall (fun P ⇒ not o P)); intro P;
    rapply functor_forall; intro dP;
    apply functor_sum.
  2,3: exact idmap.
  1: apply (functor_sigma idmap).
  2: apply (functor_forall idmap).
  all: intro a; by apply stable_decidable.
Defined.

Definition iff_iscompact'_issigmacompact (A : Type)
  : IsCompact' A ↔ IsSigmaCompact A.
Proof.
  apply iff_functor_forall; intro P.
  apply iff_functor_forall; intro dP.
  apply iff_equiv.
  apply (equiv_functor_sum' equiv_idmap).
  napply equiv_sig_ind.
Defined.

Definition iff_iscompact_issigmacompact (A : Type)
  : IsCompact A ↔ IsSigmaCompact A
  := iff_compose (iff_iscompact_iscompact' A) (iff_iscompact'_issigmacompact A).

This wrapper for equiv_sig_ind will get used twice in the next proof, so we factor it out.
Definition pi_not_equiv_not_sigma {A} (P : A → Type)
  : (∀ a, ~(P a)) <~> ~(sig P)
  := equiv_sig_ind _.

Being Π-compact is equivalent to the statement that for any decidable family, the negation of the Σ-type is decidable.
Definition iff_ispicompact_decidable_not_sigma (A : Type)
  : IsPiCompact A ↔
    ∀ P : A → Type,
      (∀ a, Decidable (P a)) → Decidable (~(sig P)).
Proof.
  split.
  1,2: intros c P dP.
  1: exact (decidable_equiv' _ (pi_not_equiv_not_sigma _) (c _ _)).
  refine (decidable_iff _ (c (not o P) _)).
  refine (iff_compose (pi_not_equiv_not_sigma _)^-1%equiv _).
  apply iff_functor_forall; intro a.
  rapply iff_stable.
Defined.

Basic definitions of searchable types

A type is searchable if for every decidable predicate we can find a "universal witness" for whether the predicate is always true or not.
Definition IsSearchable (A : Type)
  := ∀ (P : A → Type) (dP : ∀ a : A, Decidable (P a)),
      {x : A & P x → ∀ a : A, P a}.

Definition IsSearchableProps (A : Type)
  := ∀ (P : A → HProp) (dP : ∀ a : A, Decidable (P a)),
      {x : A & P x → ∀ a : A, P a}.

Definition issearchable_issearchableprops {A : Type} (s : IsSearchableProps A)
  : IsSearchable A.
Proof.
  intros P dP.
  specialize (s (merely o P) _).
  ∃ s.1.
  intros h a.
  apply merely_inhabited_iff_inhabited_stable, s.2, tr, h.
Defined.

A type is searchable if and only if it is compact and inhabited.

Definition issearchable_issigmacompact_inhabited {A : Type}
  (c : IsSigmaCompact A)
  : A → IsSearchable A.
Proof.
  intros a P dP.
  destruct (c (fun x ⇒ ¬ (P x)) _) as [l|r].
  - ∃ l.1.
    intro h; contradiction (l.2 h).
  - ∃ a; intros _ x.
    rapply stable_decidable.
    exact (fun u ⇒ r (x; u)).
Defined.

Definition issigmacompact_issearchable {A : Type} (s : IsSearchable A)
  : IsSigmaCompact A.
Proof.
  intros P dP.
  destruct (s (fun x ⇒ ¬ (P x)) _) as [w hw].
  destruct (dP w) as [x|y].
  - exact (inl (w; x)).
  - exact (inr (fun u ⇒ hw y u.1 u.2)).
Defined.

Definition inhabited_issearchable {A : Type} (s : IsSearchable A) : A
  := (s (fun a ⇒ Unit) _).1.

Definition issearchable_iff (A : Type) : IsSearchable A ↔ A × (IsSigmaCompact A)
  := (fun s ⇒ (inhabited_issearchable s, issigmacompact_issearchable s),
        fun c ⇒ issearchable_issigmacompact_inhabited (snd c) (fst c)).

Since compactness implies decidability, a type is compact if and only if it is either empty or searchable.
Definition issigmacompact_iff_not_or_issearchable (A : Type)
  : IsSigmaCompact A ↔ (¬ A) + IsSearchable A.
Proof.
  constructor.
  - intro c.
    destruct (decidable_issigmacompact c) as [l|r].
    + exact (inr (issearchable_issigmacompact_inhabited c l)).
    + exact (inl r).
  - intros [l|r].
    + exact (fun P dP ⇒ inr (l o pr1)).
    + exact (issigmacompact_issearchable r).
Defined.

Examples of searchable and compact types, and closure properties

Contractible types are compact.
Definition issigmacompact_contr {A} (c : Contr A) : IsSigmaCompact A.
Proof.
  intros P dP.
  rapply (decidable_equiv _ (equiv_contr_sigma _)^-1).
Defined.

Contractible types are searchable.
Definition issearchable_contr {A} (c : Contr A) : IsSearchable A.
Proof.
  intros P dP.
  ∃ (center A).
  intros p a.
  by induction (contr a).
Defined.

Bool is searchable.
Definition issearchable_Bool : IsSearchable Bool.
Proof.
  intros P dP.
  induction (dP false) as [p | np]; [∃ true | ∃ false].
  all: by intros p' [].
Defined.

Bool is compact.
Definition issigmacompact_bool : IsSigmaCompact Bool
  := issigmacompact_issearchable issearchable_Bool.

The empty type is trivially compact.
Definition issigmacompact_empty : IsSigmaCompact Empty
  := fun P dP ⇒ inr pr1.

Any decidable proposition is compact.
Definition issigmacompact_decidable_hprop {A : HProp} (dA : Decidable A)
  : IsSigmaCompact A.
Proof.
  destruct (equiv_decidable_hprop A) as [e1|e2].
  - apply (issigmacompact_equiv e1).
    rapply issigmacompact_contr.
  - apply (issigmacompact_equiv e2).
    apply issigmacompact_empty.
Defined.

Assuming univalence, the type of propositions is searchable.
Definition issearchable_hprop `{Univalence} : IsSearchable HProp.
Proof.
  apply issearchable_issearchableprops.
  intros P dP.
  destruct (dP Unit_hp) as [t|f].
  - ∃ False_hp; intros p a.
    rapply stable_decidable.
    by apply (not_not_constant_family_hprop P).
  - exact (Unit_hp; fun h ⇒ Empty_rec (f h)).
Defined.

Assuming the set truncation map has a section, a type is compact if and only if its set truncation is compact.
Definition issigmacompact_iff_issigmacompact_set_trunc `{Univalence} {A : Type}
  (f : (Tr 0 A) → A) (s : tr o f == idmap)
  : IsSigmaCompact A ↔ IsSigmaCompact (Tr 0 A).
Proof.
  constructor.
  1: exact (issigmacompact_retract s).
  intro cpt; rapply issigmacompact_issigmacompactprops.
  intros P dP.
  destruct (cpt (Trunc_rec P)) as [l|r].
  - intro a; strip_truncations.
    exact (dP a).
  - left; ∃ (f l.1).
    exact ((ap (Trunc_rec P) (s l.1))^ # l.2).
  - right; refine (fun a ⇒ r (tr a.1; a.2)).
Defined.

Assuming univalence, if the domain of a surjective map is searchable, then so is its codomain.

Definition issearchableprops_image `{Univalence} (A B : Type)
  (s : IsSearchableProps A)
  (f : A → B) (surj : IsSurjection f)
  : IsSearchableProps B.
Proof.
  intros P dP.
  specialize (s (P o f) _).
  exact (f s.1; fun t ⇒ conn_map_elim _ f _ (s.2 t)).
Defined.

Definition issearchable_image `{Univalence} (A B : Type)
  (s : IsSearchable A)
  (f : A → B) (surj : IsSurjection f)
  : IsSearchable B
  := issearchable_issearchableprops (issearchableprops_image A B s f surj).

Consequently, the same is true for compact types.
Definition issigmacompact_image `{Univalence} {A B : Type}
  (c : IsSigmaCompact A)
  (f : A → B) (surj : IsSurjection f)
  : IsSigmaCompact B.
Proof.
  apply issigmacompact_iff_not_or_issearchable.
  destruct (fst (issigmacompact_iff_not_or_issearchable A) c) as [n|s].
  - left; by rapply conn_map_elim.
  - right; by rapply issearchable_image.
Defined.

Assuming univalence, every pointed, connected type is searchable.
Definition issearchable_isconnected_ptype `{Univalence} (A : pType)
  (c : IsConnected 0 A)
  : IsSearchable A
  := issearchable_image Unit A (issearchable_contr _) (fun _ ⇒ pt) _.

Assuming univalence, the suspension of any type is searchable.
Definition issearchable_suspension `{Univalence} (A : Type)
  : IsSearchable (Susp A).
Proof.
  snrefine (issearchable_image Bool (Susp A) issearchable_Bool _ _).
  - exact (Bool_rec _ North South).
  - snapply Susp_ind; cbn.
    1,2: rapply contr_inhabited_hprop; apply tr.
    1: exact (true; idpath).
    1: exact (false; idpath).
    intro x; by apply path_ishprop.
Defined.

For any family of compact types over a compact type, the corresponding dependent sum type is compact.
Definition issigmacompact_sigma {A : Type} {P : A → Type}
  (cA : IsSigmaCompact A) (cP : ∀ (a : A), IsSigmaCompact (P a))
  : IsSigmaCompact (sig P).
Proof.
  intros Q dQ.
  apply (decidable_equiv _ (equiv_sigma_assoc P Q)).
  apply cA; intro a.
  by apply cP; intro p.
Defined.

Definition issigmacompact_sum {A B : Type}
  (cA : IsSigmaCompact A) (cB : IsSigmaCompact B)
  : IsSigmaCompact (A + B).
Proof.
  apply (issigmacompact_equiv (sig_of_sum A B)).
  apply issigmacompact_sigma.
  - exact issigmacompact_bool.
  - by destruct a.
Defined.

Inductively, any type of the form Fin n is compact.
Definition issigmacompact_fin (n : nat)
  : IsSigmaCompact (Fin n).
Proof.
  induction n.
  - exact (fun P dP ⇒ inr proj1).
  - apply (issigmacompact_sum IHn).
    rapply issigmacompact_contr.
Defined.

A decidable subtype of a compact type is compact.
Definition issigmacompact_detachable_subtype {A : Type} {P : A → HProp}
  (cA : IsSigmaCompact A) (dP : ∀ (a : A), Decidable (P a))
  : IsSigmaCompact (sig P).
Proof.
  apply (issigmacompact_sigma cA); cbn beta.
  intro a.
  rapply issigmacompact_decidable_hprop.
Defined.

Constructive taboos

In the next two results, we assume some form of choice and LEM. This is redundant since LEM follows from AC(0,-1) by the Diaconescu-Goodman-Myhill theorem, which is not currently part of the library.
Assuming univalence and AC(oo,-1), every type is merely compact. Note that "all types are compact" would be equivalent to all types being decidable, and thus inconsistent with univalence.
Definition merely_issigmacompact_choice `{Univalence} `{ExcludedMiddle}
  {ac : ∀ X, IsHSet X → HasChoice X} (A : Type)
  : merely (IsSigmaCompactProps A).
Proof.
  rapply ac; intro P.
  rapply ac; intro d.
  apply trunc_decidable_decidable_trunc.
  rapply LEM.
Defined.

Similarly, assuming univalence and AC(n,-1), every n-type is merely compact.
Definition merely_issigmacompact_trchoice `{Univalence} `{ExcludedMiddle}
  (n : nat) {ac : ∀ X, IsHSet X → HasTrChoice n X}
  (A : Type) `{IsTrunc n A}
  : merely (IsSigmaCompactProps A).
Proof.
  rapply ac.
  - intro; napply istrunc_forall.
    shelve.
  - intro P.
    rapply ac.
    + Unshelve.
      all: intro; apply istrunc_sum; exact _.
    + intro d.
      apply trunc_decidable_decidable_trunc.
      rapply LEM.
Defined.

The statement "every type is ∃-compact" is logically equivalent to LEM.
Definition iff_lem_ishexistscompact_all
  : ExcludedMiddle_type ↔ ∀ A, IsHExistsCompact A.
Proof.
  split.
  1: intros lem A P dP; rapply lem.
  intros c P hP.
  refine (decidable_equiv' _ _ (decidable_tr_ishexistscompact (c P))).
  symmetry; rapply equiv_tr.
Defined.

Weak LEM says that all negations are decidable.
Definition WLEM := ∀ A, Decidable (¬A).

The statement "every type is Π-compact" is logically equivalent to weak LEM.
Definition iff_wlem_ispicompact_all
  : WLEM ↔ ∀ A, IsPiCompact A.
Proof.
  split.
  2: exact (fun c A ⇒ decidable_not_ispicompact (c A)).
  intros wlem A P dP.
  destruct (wlem (∀ a, P a)) as [l|r].
  1: right; exact l.
  left; exact (stable_forall _ _ r).
Defined.

The limited principle of omniscience says that nat is exists-compact.
Definition LPO := IsHExistsCompact nat.

The limited principle of omniscience is equivalent to nat being compact.
Definition issigmacompact_nat_lpo (lpo : LPO)
  : IsSigmaCompact nat.
Proof.
  intros P dP.
  destruct (lpo P dP) as [l|r].
  1: left; exact (minimal_n _ _ l).
  right; exact (r o tr).
Defined.

The weak limited principle of omniscience says that for any decidable family on nat, the negation of the total type is decidable.
Definition WLPO
  := ∀ (P : nat → Type) (dP : ∀ n : nat, Decidable (P n)), Decidable (¬ sig P).

Instance ishprop_wlpo `{Funext} : IsHProp WLPO := _.

The weak limited principle of omniscience is logically equivalent to nat being Π-compact.
Definition iff_wlpo_ispicompact_nat : WLPO ↔ IsPiCompact nat
  := symmetric_iff _ _ (iff_ispicompact_decidable_not_sigma nat).

Section Uniform_Search.

Searchability of nat → A

Following https://www.cs.bham.ac.uk/~mhe/TypeTopology/TypeTopology.UniformSearch.html, we prove that if A is searchable then nat → A is uniformly searchable.
A type with a uniform structure is uniformly searchable if it is searchable over uniformly continuous predicates. Here the uniform structure on Type is the trivial one trivial_us involving the identity types at each level.
  Definition uniformly_searchable (A : Type) {usA : UStructure A}
    := ∀ (P : A → Type) (dP : ∀ a : A, Decidable (P a)),
        uniformly_continuous P → ∃ w0 : A, (P w0 → ∀ u : A, P u).

  Context {A : Type} (issearchable_A : IsSearchable A).

The witness function for uniformly continuous predicates on nat → A. The first argument n : nat will be the modulus of uniform continuity, but we do not use the property in this definition.
  Definition uniformsearch_witness (n : nat) (P : (nat → A) → Type)
    (dP : ∀ (f : nat → A), Decidable (P f))
    : nat → A.
  Proof.
    induction n in P, dP.
    - exact (fun _ ⇒ inhabited_issearchable issearchable_A).
    - pose (g Q dQ := Q (IHn Q dQ)).
      pose (wA := (issearchable_A (fun x ⇒ g (P o (seq_cons x)) _) _).1).
      exact (seq_cons wA (IHn (P o (seq_cons wA)) _)).
  Defined.

We often need to apply P to uniformsearch_witness n P dP, and this saves repeating P.
  Local Definition pred_uniformsearch_witness (n : nat) (P : (nat → A) → Type)
    (dP : ∀ (f : nat → A), Decidable (P f))
    := P (uniformsearch_witness n P dP).

The desired property of the witness function.
  Definition uniformsearch_witness_spec {n : nat} (P : (nat → A) → Type)
    (dP : ∀ f : (nat → A), Decidable (P f))
    (is_mod : is_modulus_of_uniform_continuity n P)
    (h : pred_uniformsearch_witness n P dP)
    : ∀ u : nat → A, P u.
  Proof.
    induction n in P, dP, is_mod, h.
    - intro u.
      refine (transport idmap _ h).
      (* For n = 0, is_mod u1 u2 says that P u1 = P u2. *)
      apply is_mod, sequence_type_us_zero.
    - intro u.
      refine (transport idmap _ _).
      1: exact (uniformly_continuous_extensionality P (m:=0)
                  (uniformly_continuous_has_modulus is_mod)
                  (seq_cons_head_tail u)).
      rapply (IHn (P o (seq_cons (u 0)))).
      1: apply cons_decreases_modulus, is_mod.
      (* The universality of uniformsearch_witness says that it is enough to check this statement with u 0 replaced with wA above, and that is exactly what h proves, by the inductive step. *)
      exact ((issearchable_A
                 (fun y ⇒ pred_uniformsearch_witness n (P o (seq_cons y)) _) _).2
                h (u 0)).
  Defined.

  Definition has_uniformly_searchable_seq_issearchable
    : uniformly_searchable (nat → A).
  Proof.
    intros P dP contP.
    ∃ (uniformsearch_witness (contP 0).1 P dP).
    apply uniformsearch_witness_spec; exact (contP 0).2.
  Defined.

End Uniform_Search.