(** * Properties of compact and searchable types *)

From HoTT Require Import Basics Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Truncations.Core Truncations.Connectedness.
Require Import Spaces.Nat.Core.
Require Import Misc.UStructures.
Require Import Spaces.NatSeq.Core Spaces.NatSeq.UStructure.
Require Import Homotopy.Suspension.
Require Import Pointed.Core.
Require Import Universes.TruncType.
Require Import Idempotents.

Local Open Scope nat_scope.
Local Open Scope pointed_scope.

(** ** Basic definitions of compact types *)

(** 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)
  := forall P : A -> Type, (forall a : A, Decidable (P a)) ->
                              {a : A & ~ P a} + (forall a : A, P a).

(** Any compact type is decidable. *)
Definition decidable_iscompact {A : Type} (c : IsCompact A) : Decidable A.
A: Type
c: IsCompact A
Decidable A
Proof.
A: Type
c: IsCompact A
Decidable A
  destruct (c (fun (_ : A) => Empty) _) as [c1|c2].
A: Type
c: IsCompact A
c1: {_ : A & ~ Empty}
Decidable A
A: Type
c: IsCompact A
c2: A -> Empty
Decidable A
  -
A: Type
c: IsCompact A
c1: {_ : A & ~ Empty}
Decidable A exact (inl c1.1).
  -
A: Type
c: IsCompact A
c2: A -> Empty
Decidable A exact (inr c2).
Defined.

(** Compactness is equivalent to assuming the same for [HProp]-valued decidable predicates. *)
Definition IsCompactProps (A : Type)
  := forall P : A -> HProp, (forall a : A, Decidable (P a)) ->
                              {a : A & ~ P a} + (forall a : A, P a).

Definition iscompact_iscompactprops {A} (c : IsCompactProps A) : IsCompact A.
A: Type
c: IsCompactProps A
IsCompact A
Proof.
A: Type
c: IsCompactProps A
IsCompact A
  intros P dP.
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
({a : A & ~ P a} + (forall a : A, P a))%type
  destruct (c (merely o P) _) as [l|r].
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {a : A & ~ merely (P a)}
({a : A & ~ P a} + (forall a : A, P a))%type
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, merely (P a)
({a : A & ~ P a} + (forall a : A, P a))%type
  -
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {a : A & ~ merely (P a)}
({a : A & ~ P a} + (forall a : A, P a))%type exact (inl (l.1; fun p => l.2 (tr p))).
  -
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, merely (P a)
({a : A & ~ P a} + (forall a : A, P a))%type right.
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, merely (P a)
forall a : A, P a
    intro a.
A: Type
c: IsCompactProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, merely (P a)
a: A
P a
    apply merely_inhabited_iff_inhabited_stable, r.
Defined.

(** Since decidable types are stable, it's also equivalent to negate [P] in the definition. *)
Definition IsCompact' (A : Type)
  := forall P : A -> Type, (forall a : A, Decidable (P a)) ->
                              {a : A & P a} + (forall a : A, ~ P a).

Definition iff_iscompact_iscompact' (A : Type)
  : IsCompact A <-> IsCompact' A.
A: Type
IsCompact A <-> IsCompact' A
Proof.
A: Type
IsCompact A <-> IsCompact' A
  split;
    napply (functor_forall (fun P => not o P)); intro P;
    rapply functor_forall; intro dP;
    apply functor_sum.
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
{a : A & ~~ P a} -> {a : A & P a}
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
(forall a : A, ~ P a) -> forall a : A, ~ P a
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
{a : A & ~ P a} -> {a : A & ~ P a}
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
(forall a : A, ~~ P a) -> forall a : A, P a
  2,3: exact idmap.
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
{a : A & ~~ P a} -> {a : A & P a}
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
(forall a : A, ~~ P a) -> forall a : A, P a
  1: apply (functor_sigma idmap).
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
forall a : A, ~~ P a -> P a
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
(forall a : A, ~~ P a) -> forall a : A, P a
  2: apply (functor_forall idmap).
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
forall a : A, ~~ P a -> P a
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
forall b : A, ~~ P b -> P b
  all: intro a; by apply stable_decidable.
Defined.

(** Another equivalent definition of compactness: If a family over the type is decidable, then the Σ-type is decidable. *)
Definition IsSigmaCompact (A : Type)
  := forall P : A -> Type, (forall a : A, Decidable (P a)) -> Decidable (sig P).

Definition equiv_iscompact'_issigmacompact {A : Type}
  : IsCompact' A <-> IsSigmaCompact A.
A: Type
IsCompact' A <-> IsSigmaCompact A
Proof.
A: Type
IsCompact' A <-> IsSigmaCompact A
  apply iff_functor_forall; intro P.
A: Type
P: A -> Type
((forall a : A, Decidable (P a)) ->
 {a : A & P a} + (forall a : A, ~ P a)) <->
((forall a : A, Decidable (P a)) ->
 Decidable {x : _ & P x})
  apply iff_functor_forall; intro dP.
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
{a : A & P a} + (forall a : A, ~ P a) <->
Decidable {x : _ & P x}
  apply iff_equiv.
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
{a : A & P a} + (forall a : A, ~ P a) <~>
Decidable {x : _ & P x}
  apply (equiv_functor_sum' equiv_idmap).
A: Type
P: A -> Type
dP: forall a : A, Decidable (P a)
(forall a : A, ~ P a) <~> ~ {x : _ & P x}
  napply equiv_sig_ind.
Defined.

(** Again, it is enough to consider [HProp]-valued families. *)
Definition IsSigmaCompactProps (A : Type)
  := forall P : A -> HProp,
      (forall a : A, Decidable (P a)) -> Decidable (sig P).

Definition issigmacompactprops_issigmacompact {A : Type}
  (h : IsSigmaCompact A)
  : IsSigmaCompactProps A
  := fun P hP => h P hP.

Definition issigmacompact_issigmacompactprops {A : Type}
  (h : IsSigmaCompactProps A)
  : IsSigmaCompact A.
A: Type
h: IsSigmaCompactProps A
IsSigmaCompact A
Proof.
A: Type
h: IsSigmaCompactProps A
IsSigmaCompact A
  intros P hP.
A: Type
h: IsSigmaCompactProps A
P: A -> Type
hP: forall a : A, Decidable (P a)
Decidable {x : _ & P x}
  refine (decidable_iff _ (h (merely o P) _)).
A: Type
h: IsSigmaCompactProps A
P: A -> Type
hP: forall a : A, Decidable (P a)
{x : A & merely (P x)} <-> {x : _ & P x}
  apply iff_functor_sigma; intro a.
A: Type
h: IsSigmaCompactProps A
P: A -> Type
hP: forall a : A, Decidable (P a)
a: A
merely (P a) <-> P a
  exact merely_inhabited_iff_inhabited_stable.
Defined.

(** A weaker definition: for any decidable family, the dependent function type is decidable. *)
Definition IsPiCompact (A : Type)
  := forall (P : A -> Type) (dP : forall a : A, Decidable (P a)),
      Decidable (forall a : A, P a).

Definition ispicompact_issigmacompact {A : Type} (c : IsSigmaCompact A)
  : IsPiCompact A.
A: Type
c: IsSigmaCompact A
IsPiCompact A
Proof.
A: Type
c: IsSigmaCompact A
IsPiCompact A
  intros P dP.
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
Decidable (forall a : A, P a)
  destruct (c (not o P) _) as [l|r].
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {x : A & ~ P x}
Decidable (forall a : A, P a)
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: ~ {x : A & ~ P x}
Decidable (forall a : A, P a)
  -
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {x : A & ~ P x}
Decidable (forall a : A, P a) right; exact (fun f => l.2 (f l.1)).
  -
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: ~ {x : A & ~ P x}
Decidable (forall a : A, P a) left.
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: ~ {x : A & ~ P x}
forall a : A, P a
    intro a.
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: ~ {x : A & ~ P x}
a: A
P a
    apply (stable_decidable (P a)).
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: ~ {x : A & ~ P x}
a: A
~~ P a
    exact (fun u => r (a; u)).
Defined.

(** Compact types are closed under retracts. *)
Definition iscompact_retract {A : Type} (R : RetractOf A) (c : IsCompact A)
  : IsCompact (retract_type R).
A: Type
R: RetractOf A
c: IsCompact A
IsCompact (retract_type R)
Proof.
A: Type
R: RetractOf A
c: IsCompact A
IsCompact (retract_type R)
  intros P dP; destruct (c (P o (retract_retr R)) _) as [l|r].
A: Type
R: RetractOf A
c: IsCompact A
P: retract_type R -> Type
dP: forall a : retract_type R, Decidable (P a)
l: {a : A & ~ P (retract_retr R a)}
({a : retract_type R & ~ P a} +
 (forall a : retract_type R, P a))%type
A: Type
R: RetractOf A
c: IsCompact A
P: retract_type R -> Type
dP: forall a : retract_type R, Decidable (P a)
r: forall a : A, P (retract_retr R a)
({a : retract_type R & ~ P a} +
 (forall a : retract_type R, P a))%type
  -
A: Type
R: RetractOf A
c: IsCompact A
P: retract_type R -> Type
dP: forall a : retract_type R, Decidable (P a)
l: {a : A & ~ P (retract_retr R a)}
({a : retract_type R & ~ P a} +
 (forall a : retract_type R, P a))%type exact (inl ((retract_retr R) l.1; l.2)).
  -
A: Type
R: RetractOf A
c: IsCompact A
P: retract_type R -> Type
dP: forall a : retract_type R, Decidable (P a)
r: forall a : A, P (retract_retr R a)
({a : retract_type R & ~ P a} +
 (forall a : retract_type R, P a))%type exact (inr (fun a =>  ((retract_issect R) a) # r ((retract_sect R) a))).
Defined.

Definition iscompact_retract' {A R : Type} {f : A -> R} {g : R -> A}
  (s : f o g == idmap) (c : IsCompact A)
  : IsCompact R
  := iscompact_retract (Build_RetractOf A R f g s) c.

(** Assuming the set truncation map has a section, a type is compact if and only if its set truncation is compact. *)
Definition compact_set_trunc_compact `{Univalence} {A : Type}
  (f : (Tr 0 A) -> A) (s : tr o f == idmap)
  : IsCompact A <-> IsCompact (Tr 0 A).
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
IsCompact A <-> IsCompact (Tr 0 A)
Proof.
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
IsCompact A <-> IsCompact (Tr 0 A)
  constructor.
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
IsCompact A -> IsCompact (Tr 0 A)
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
IsCompact (Tr 0 A) -> IsCompact A
  1: exact (iscompact_retract' s).
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
IsCompact (Tr 0 A) -> IsCompact A
  intro cpt; rapply iscompact_iscompactprops.
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
IsCompactProps A
  intros P dP.
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
({a : A & ~ P a} + (forall a : A, P a))%type
  destruct (cpt (Trunc_rec P)) as [l|r].
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
forall a : Tr 0 A, Decidable (Trunc_rec P a)
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
l: {a : Tr 0 A & ~ Trunc_rec P a}
({a : A & ~ P a} + (forall a : A, P a))%type
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
r: forall a : Tr 0 A, Trunc_rec P a
({a : A & ~ P a} + (forall a : A, P a))%type
  -
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
forall a : Tr 0 A, Decidable (Trunc_rec P a) intro a; strip_truncations.
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
a: A
Decidable (Trunc_rec P (tr a))
    exact (dP a).
  -
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
l: {a : Tr 0 A & ~ Trunc_rec P a}
({a : A & ~ P a} + (forall a : A, P a))%type exact (inl (f l.1; fun x => l.2 (ap (Trunc_rec P) (s l.1) # x))).
  -
H: Univalence
A: Type
f: Tr 0 A -> A
s: tr o f == idmap
cpt: IsCompact (Tr 0 A)
P: A -> HProp
dP: forall a : A, Decidable (P a)
r: forall a : Tr 0 A, Trunc_rec P a
({a : A & ~ P a} + (forall a : A, P a))%type exact (inr (fun a => r (tr a))).
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)
  := forall (P : A -> Type) (dP : forall a : A, Decidable (P a)),
      {x : A & P x -> forall a : A, P a}.

Definition IsSearchableProps (A : Type)
  := forall (P : A -> HProp) (dP : forall a : A, Decidable (P a)),
      {x : A & P x -> forall a : A, P a}.

Definition issearchable_issearchableprops {A : Type} (s : IsSearchableProps A)
  : IsSearchable A.
A: Type
s: IsSearchableProps A
IsSearchable A
Proof.
A: Type
s: IsSearchableProps A
IsSearchable A
  intros P dP.
A: Type
s: IsSearchableProps A
P: A -> Type
dP: forall a : A, Decidable (P a)
{x : A & P x -> forall a : A, P a}
  specialize (s (merely o P) _).
A: Type
P: A -> Type
s: {x : A &
(merely o P) x -> forall a : A, (merely o P) a}
dP: forall a : A, Decidable (P a)
{x : A & P x -> forall a : A, P a}
  exists s.1.
A: Type
P: A -> Type
s: {x : A &
(merely o P) x -> forall a : A, (merely o P) a}
dP: forall a : A, Decidable (P a)
P s.1 -> forall a : A, P a
  intros h a.
A: Type
P: A -> Type
s: {x : A &
(merely o P) x -> forall a : A, (merely o P) a}
dP: forall a : A, Decidable (P a)
h: P s.1
a: A
P 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_iscompact_inhabited {A : Type}
  : IsCompact A -> A -> IsSearchable A.
A: Type
IsCompact A -> A -> IsSearchable A
Proof.
A: Type
IsCompact A -> A -> IsSearchable A
  intros c a P dP.
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
{x : A & P x -> forall a : A, P a}
  induction (c P _) as [l|r].
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {a : A & ~ P a}
{x : A & P x -> forall a : A, P a}
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, P a
{x : A & P x -> forall a : A, P a}
  -
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {a : A & ~ P a}
{x : A & P x -> forall a : A, P a} exists l.1.
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
l: {a : A & ~ P a}
P l.1 -> forall a : A, P a
    intro h; contradiction (l.2 h).
  -
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a : A, Decidable (P a)
r: forall a : A, P a
{x : A & P x -> forall a : A, P a} exact (a; fun _ => r).
Defined.

Definition iscompact_issearchable {A : Type} : IsSearchable A -> IsCompact A.
A: Type
IsSearchable A -> IsCompact A
Proof.
A: Type
IsSearchable A -> IsCompact A
  intros h P dP.
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
({a : A & ~ P a} + (forall a : A, P a))%type
  set (w := (h P dP).1).
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
w:= (h P dP).1: A
({a : A & ~ P a} + (forall a : A, P a))%type
  destruct (dP w) as [x|y].
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
w:= (h P dP).1: A
x: P w
({a : A & ~ P a} + (forall a : A, P a))%type
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
w:= (h P dP).1: A
y: ~ P w
({a : A & ~ P a} + (forall a : A, P a))%type
  -
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
w:= (h P dP).1: A
x: P w
({a : A & ~ P a} + (forall a : A, P a))%type exact (inr ((h P dP).2 x)).
  -
A: Type
h: IsSearchable A
P: A -> Type
dP: forall a : A, Decidable (P a)
w:= (h P dP).1: A
y: ~ P w
({a : A & ~ P a} + (forall a : A, P a))%type exact (inl (w; y)).
Defined.

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

Definition searchable_iff {A : Type} : IsSearchable A <-> A * (IsCompact A)
  := (fun s => (inhabited_issearchable s, iscompact_issearchable s),
        fun c => issearchable_iscompact_inhabited (snd c) (fst c)).

(** ** Examples of searchable and compact types  *)

Definition issearchable_contr {A} (c : Contr A) : IsSearchable A.
A: Type
c: Contr A
IsSearchable A
Proof.
A: Type
c: Contr A
IsSearchable A
  intros P dP.
A: Type
c: Contr A
P: A -> Type
dP: forall a : A, Decidable (P a)
{x : A & P x -> forall a : A, P a}
  exists (center A).
A: Type
c: Contr A
P: A -> Type
dP: forall a : A, Decidable (P a)
P (center A) -> forall a : A, P a
  intros p a.
A: Type
c: Contr A
P: A -> Type
dP: forall a : A, Decidable (P a)
p: P (center A)
a: A
P a
  by induction (contr a).
Defined.

Definition issearchable_Bool : IsSearchable Bool.
IsSearchable Bool
Proof.
IsSearchable Bool
  intros P dP.
P: Bool -> Type
dP: forall a : Bool, Decidable (P a)
{x : Bool & P x -> forall a : Bool, P a}
  induction (dP false) as [p | np]; [exists true | exists false].
P: Bool -> Type
dP: forall a : Bool, Decidable (P a)
p: P false
P true -> forall a : Bool, P a
P: Bool -> Type
dP: forall a : Bool, Decidable (P a)
np: ~ P false
P false -> forall a : Bool, P a
  all: by intros p' [].
Defined.

(** The empty type is trivially compact. *)
Definition iscompact_empty : IsCompact Empty
  := fun P dP => inr (fun a => Empty_rec a).

Definition iscompact_empty' {A : Type} (na : ~A) : IsCompact A
  := fun p dP => inr (fun a => Empty_rec (na a)).

Definition iscompact_iff_not_or_issearchable {A : Type} :
  IsCompact A <-> (~ A) + IsSearchable A.
A: Type
IsCompact A <-> ~ A + IsSearchable A
Proof.
A: Type
IsCompact A <-> ~ A + IsSearchable A
  constructor.
A: Type
IsCompact A -> ~ A + IsSearchable A
A: Type
~ A + IsSearchable A -> IsCompact A
  -
A: Type
IsCompact A -> ~ A + IsSearchable A intro c.
A: Type
c: IsCompact A
(~ A + IsSearchable A)%type
    destruct (decidable_iscompact c) as [l|r].
A: Type
c: IsCompact A
l: A
(~ A + IsSearchable A)%type
A: Type
c: IsCompact A
r: ~ A
(~ A + IsSearchable A)%type
    +
A: Type
c: IsCompact A
l: A
(~ A + IsSearchable A)%type exact (inr (issearchable_iscompact_inhabited c l)).
    +
A: Type
c: IsCompact A
r: ~ A
(~ A + IsSearchable A)%type exact (inl r).
  -
A: Type
~ A + IsSearchable A -> IsCompact A intros [l|r].
A: Type
l: ~ A
IsCompact A
A: Type
r: IsSearchable A
IsCompact A
    +
A: Type
l: ~ A
IsCompact A exact (iscompact_empty' l).
    +
A: Type
r: IsSearchable A
IsCompact A exact (iscompact_issearchable r).
Defined.

(** Assuming univalence, the type of propositions is searchable. *)
Definition issearchable_hprop `{Univalence} : IsSearchable HProp.
H: Univalence
IsSearchable HProp
Proof.
H: Univalence
IsSearchable HProp
  apply issearchable_issearchableprops.
H: Univalence
IsSearchableProps HProp
  intros P dP.
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
{x : HProp & P x -> forall a : HProp, P a}
  destruct (dP Unit_hp) as [t|f].
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
t: P Unit_hp
{x : HProp & P x -> forall a : HProp, P a}
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
f: ~ P Unit_hp
{x : HProp & P x -> forall a : HProp, P a}
  -
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
t: P Unit_hp
{x : HProp & P x -> forall a : HProp, P a} exists False_hp; intros p a.
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
t: P Unit_hp
p: P False_hp
a: HProp
P a
    rapply stable_decidable.
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
t: P Unit_hp
p: P False_hp
a: HProp
~~ P a
    by apply (not_not_constant_family_hprop P).
  -
H: Univalence
P: HProp -> HProp
dP: forall a : HProp, Decidable (P a)
f: ~ P Unit_hp
{x : HProp & P x -> forall a : HProp, P a} exact (Unit_hp; fun h => Empty_rec (f h)).
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.
H: Univalence
A, B: Type
s: IsSearchableProps A
f: A -> B
surj: IsConnMap (Tr (-1)) f
IsSearchableProps B
Proof.
H: Univalence
A, B: Type
s: IsSearchableProps A
f: A -> B
surj: IsConnMap (Tr (-1)) f
IsSearchableProps B
  intros P dP.
H: Univalence
A, B: Type
s: IsSearchableProps A
f: A -> B
surj: IsConnMap (Tr (-1)) f
P: B -> HProp
dP: forall a : B, Decidable (P a)
{x : B & P x -> forall a : B, P a}
  specialize (s (P o f) _).
H: Univalence
A, B: Type
f: A -> B
P: B -> HProp
s: {x : A & (P o f) x -> forall a : A, (P o f) a}
surj: IsConnMap (Tr (-1)) f
dP: forall a : B, Decidable (P a)
{x : B & P x -> forall a : B, P a}
  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).

(** Assuming univalence, every connected pointed 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).
H: Univalence
A: Type
IsSearchable (Susp A)
Proof.
H: Univalence
A: Type
IsSearchable (Susp A)
  snrefine (issearchable_image Bool (Susp A) issearchable_Bool _ _).
H: Univalence
A: Type
Bool -> Susp A
H: Univalence
A: Type
IsConnMap (Tr (-1)) ?f
  -
H: Univalence
A: Type
Bool -> Susp A exact (Bool_rec _ North South).
  -
H: Univalence
A: Type
IsConnMap (Tr (-1)) (Bool_rec (Susp A) North South) snapply Susp_ind; cbn.
H: Univalence
A: Type
IsConnected (Tr (-1))
  (hfiber (Bool_rec (Susp A) North South) North)
H: Univalence
A: Type
IsConnected (Tr (-1))
  (hfiber (Bool_rec (Susp A) North South) South)
H: Univalence
A: Type
forall x : A,
transport
  (fun y : Susp A =>
   IsConnected (Tr (-1))
     (hfiber (Bool_rec (Susp A) North South) y))
  (merid x) ?Goal = ?Goal0
    1,2: rapply contr_inhabited_hprop; apply tr.
H: Univalence
A: Type
hfiber (Bool_rec (Susp A) North South) North
H: Univalence
A: Type
hfiber (Bool_rec (Susp A) North South) South
H: Univalence
A: Type
forall x : A,
transport
  (fun y : Susp A =>
   IsConnected (Tr (-1))
     (hfiber (Bool_rec (Susp A) North South) y))
  (merid x)
  (contr_inhabited_hprop
     (Tr (-1)
        (hfiber (Bool_rec (Susp A) North South) North))
     (tr ?Goal0)) =
contr_inhabited_hprop
  (Tr (-1)
     (hfiber (Bool_rec (Susp A) North South) South))
  (tr ?Goal1)
    1: exact (true; idpath).
H: Univalence
A: Type
hfiber (Bool_rec (Susp A) North South) South
H: Univalence
A: Type
forall x : A,
transport
  (fun y : Susp A =>
   IsConnected (Tr (-1))
     (hfiber (Bool_rec (Susp A) North South) y))
  (merid x)
  (contr_inhabited_hprop
     (Tr (-1)
        (hfiber (Bool_rec (Susp A) North South) North))
     (tr (true; 1))) =
contr_inhabited_hprop
  (Tr (-1)
     (hfiber (Bool_rec (Susp A) North South) South))
  (tr ?Goal0)
    1: exact (false; idpath).
H: Univalence
A: Type
forall x : A,
transport
  (fun y : Susp A =>
   IsConnected (Tr (-1))
     (hfiber (Bool_rec (Susp A) North South) y))
  (merid x)
  (contr_inhabited_hprop
     (Tr (-1)
        (hfiber (Bool_rec (Susp A) North South) North))
     (tr (true; 1))) =
contr_inhabited_hprop
  (Tr (-1)
     (hfiber (Bool_rec (Susp A) North South) South))
  (tr (false; 1))
    intro x; by apply path_ishprop.
Defined.

Definition iscompact_image `{Univalence} (A B : Type)
  (c : IsCompact A)
  (f : A -> B) (surj : IsSurjection f)
  : IsCompact B.
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
IsCompact B
Proof.
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
IsCompact B
  apply iscompact_iff_not_or_issearchable.
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
(~ B + IsSearchable B)%type
  destruct ((fst iscompact_iff_not_or_issearchable) c) as [n|s].
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
n: ~ A
(~ B + IsSearchable B)%type
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
s: IsSearchable A
(~ B + IsSearchable B)%type
  -
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
n: ~ A
(~ B + IsSearchable B)%type left; by rapply conn_map_elim.
  -
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
s: IsSearchable A
(~ B + IsSearchable B)%type right; by rapply issearchable_image.
Defined.

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}
    := forall (P : A -> Type) (dP : forall a : A, Decidable (P a)),
        uniformly_continuous P -> exists w0 : A, (P w0 -> forall 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 : forall (f : nat -> A), Decidable (P f))
    : nat -> A.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
nat -> A
  Proof.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
nat -> A
    induction n in P, dP.
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
nat -> A
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
IHn: forall P : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P f)) ->
nat -> A
nat -> A
    -
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
nat -> A exact (fun _ => inhabited_issearchable issearchable_A).
    -
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
IHn: forall P : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P f)) ->
nat -> A
nat -> A pose (g Q dQ := Q (IHn Q dQ)).
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
IHn: forall P : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P f)) ->
nat -> A
g:= fun (Q : (nat -> A) -> Type)
  (dQ : forall f : nat -> A, Decidable (Q f)) =>
Q (IHn Q dQ): forall Q : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (Q f)) -> Type
nat -> A
      pose (wA := (issearchable_A (fun x => g (P o (seq_cons x)) _) _).1).
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
IHn: forall P : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P f)) ->
nat -> A
g:= fun (Q : (nat -> A) -> Type)
  (dQ : forall f : nat -> A, Decidable (Q f)) =>
Q (IHn Q dQ): forall Q : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (Q f)) -> Type
wA:= (issearchable_A
   (fun x : A =>
    g (P o seq_cons x)
      (fun f : nat -> A => dP (seq_cons x f)))
   (fun a : A =>
    dP
      (seq_cons a
         (IHn
            (fun x0 : nat -> A =>
             P (seq_cons a x0))
            (fun f : nat -> A => dP (seq_cons a f)))))).1: A
nat -> A
      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 : forall (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 : forall f : (nat -> A), Decidable (P f))
    (is_mod : is_modulus_of_uniform_continuity n P)
    (h : pred_uniformsearch_witness n P dP)
    : forall u : nat -> A, P u.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n P
h: pred_uniformsearch_witness n P dP
forall u : nat -> A, P u
  Proof.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n P
h: pred_uniformsearch_witness n P dP
forall u : nat -> A, P u
    induction n in P, dP, is_mod, h.
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity 0 P
h: pred_uniformsearch_witness 0 P dP
forall u : nat -> A, P u
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
forall u : nat -> A, P u
    -
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity 0 P
h: pred_uniformsearch_witness 0 P dP
forall u : nat -> A, P u intro u.
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity 0 P
h: pred_uniformsearch_witness 0 P dP
u: nat -> A
P u
      refine (transport idmap _ h).
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity 0 P
h: pred_uniformsearch_witness 0 P dP
u: nat -> A
pred_uniformsearch_witness 0 P dP = P u
      (* For [n = 0], [is_mod u1 u2] says that [P u1 = P u2]. *)
      apply is_mod, sequence_type_us_zero.
    -
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
forall u : nat -> A, P u intro u.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
P u
      refine (transport idmap _ _).
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
?Goal = P u
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
?Goal
      1: exact (uniformly_continuous_extensionality P (m:=0)
                  (uniformly_continuous_has_modulus is_mod)
                  (seq_cons_head_tail u)).
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
P (seq_cons (u 0) (seq_tail u))
      rapply (IHn (P o (seq_cons (u 0)))).
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
is_modulus_of_uniform_continuity n
  (fun x : nat -> A => P (seq_cons (u 0) x))
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
pred_uniformsearch_witness n
  (fun x : nat -> A => P (seq_cons (u 0) x))
  (fun f : nat -> A => dP (seq_cons (u 0) f))
      1: apply cons_decreases_modulus, is_mod.
A: Type
issearchable_A: IsSearchable A
n: nat
P: (nat -> A) -> Type
dP: forall f : nat -> A, Decidable (P f)
is_mod: is_modulus_of_uniform_continuity n.+1 P
h: pred_uniformsearch_witness n.+1 P dP
IHn: forall (P : (nat -> A) -> Type)
(dP : forall f : nat -> A, Decidable (P f)),
is_modulus_of_uniform_continuity n P ->
pred_uniformsearch_witness n P dP ->
forall u : nat -> A, P u
u: nat -> A
pred_uniformsearch_witness n
  (fun x : nat -> A => P (seq_cons (u 0) x))
  (fun f : nat -> A => dP (seq_cons (u 0) f))
      (* 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).
A: Type
issearchable_A: IsSearchable A
uniformly_searchable (nat -> A)
  Proof.
A: Type
issearchable_A: IsSearchable A
uniformly_searchable (nat -> A)
    intros P dP contP.
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall a : nat -> A, Decidable (P a)
contP: uniformly_continuous P
{w0 : nat -> A & P w0 -> forall u : nat -> A, P u}
    exists (uniformsearch_witness (contP 0).1 P dP).
A: Type
issearchable_A: IsSearchable A
P: (nat -> A) -> Type
dP: forall a : nat -> A, Decidable (P a)
contP: uniformly_continuous P
P (uniformsearch_witness (contP 0).1 P dP) ->
forall u : nat -> A, P u
    apply uniformsearch_witness_spec; exact (contP 0).2.
  Defined.

End Uniform_Search.