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

From HoTT Require Import Basics Types.
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)
  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)
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)
  -
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) 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) 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 a0 : A, Decidable (P a0)
r: forall a0 : A, merely (P a0)
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 a0 : A, Decidable (P a0)
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 a0 : A, Decidable (P a0)
r: ~ {x : A & ~ P x}
a: A
P a
    apply (stable_decidable (P a)).
A: Type
c: IsSigmaCompact A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
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)
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)
  -
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) 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) 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)
  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)
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)
  -
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 a0 : A, Decidable (P a0)
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) 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) 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 a0 : A, (merely o P) a0}
dP: forall a0 : A, Decidable (P a0)
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 a0 : A, Decidable (P a0)
{x : A & P x -> forall a0 : A, P a0}
  induction (c P _) as [l|r].
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
l: {a0 : A & ~ P a0}
{x : A & P x -> forall a0 : A, P a0}
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
r: forall a0 : A, P a0
{x : A & P x -> forall a0 : A, P a0}
  -
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
l: {a0 : A & ~ P a0}
{x : A & P x -> forall a0 : A, P a0} exists l.1.
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
l: {a0 : A & ~ P a0}
P l.1 -> forall a0 : A, P a0
    intro h; contradiction (l.2 h).
  -
A: Type
c: IsCompact A
a: A
P: A -> Type
dP: forall a0 : A, Decidable (P a0)
r: forall a0 : A, P a0
{x : A & P x -> forall a0 : A, P a0} 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)
  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)
  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)
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)
  -
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) 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) 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 a0 : A, Decidable (P a0)
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
    destruct (decidable_iscompact c) as [l|r].
A: Type
c: IsCompact A
l: A
~ A + IsSearchable A
A: Type
c: IsCompact A
r: ~ A
~ A + IsSearchable A
    +
A: Type
c: IsCompact A
l: A
~ A + IsSearchable A exact (inr (issearchable_iscompact_inhabited c l)).
    +
A: Type
c: IsCompact A
r: ~ A
~ A + IsSearchable A 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 a0 : HProp, Decidable (P a0)
t: P Unit_hp
p: P False_hp
a: HProp
P a
    rapply stable_decidable.
H: Univalence
P: HProp -> HProp
dP: forall a0 : HProp, Decidable (P a0)
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
  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
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
s: IsSearchable A
~ B + IsSearchable B
  -
H: Univalence
A, B: Type
c: IsCompact A
f: A -> B
surj: IsConnMap (Tr (-1)) f
n: ~ A
~ B + IsSearchable B 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 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 P0 : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P0 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 P0 : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P0 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 P0 : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P0 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 P0 : (nat -> A) -> Type,
(forall f : nat -> A, Decidable (P0 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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u : nat -> A, P0 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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u : nat -> A, P0 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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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 (P0 : (nat -> A) -> Type)
(dP0 : forall f : nat -> A, Decidable (P0 f)),
is_modulus_of_uniform_continuity n P0 ->
pred_uniformsearch_witness n P0 dP0 -> forall u0 : nat -> A, P0 u0
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.