This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Dubuc-Penon compact types

module foundation.dubuc-penon-compact-types where
Imports 
open import foundation.disjunction
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.propositions
open import foundation-core.subtypes

Idea

A type is said to be Dubuc-Penon compact if for every proposition P and every subtype Q of X such that the disjunction P ∨ Q x holds for all x, then either P is true or Q contains every element of X.

Definition

is-dubuc-penon-compact-Prop :
  {l : Level} (l1 l2 : Level) → UU l → Prop (l ⊔ lsuc l1 ⊔ lsuc l2)
is-dubuc-penon-compact-Prop l1 l2 X =
  ∀'
    ( Prop l1)
    ( λ P →
      ∀'
        ( subtype l2 X)
        ( λ Q → (∀' X (λ x → P ∨ Q x)) ⇒ (P ∨ (∀' X Q))))

is-dubuc-penon-compact :
  {l : Level} (l1 l2 : Level) → UU l → UU (l ⊔ lsuc l1 ⊔ lsuc l2)
is-dubuc-penon-compact l1 l2 X = type-Prop (is-dubuc-penon-compact-Prop l1 l2 X)