Dubuc-Penon compact types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-04-09.
Last modified on 2026-05-02.

module foundation.dubuc-penon-compact-types where
Imports 
open import foundation.dependent-products-propositions
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)

Recent changes