Markovian types

Content created by Fredrik Bakke.

Created on 2025-01-07.
Last modified on 2025-08-14.

module logic.markovian-types where

Imports

open import foundation.booleans
open import foundation.decidable-subtypes
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.negation
open import foundation.universal-quantification
open import foundation.universe-levels

open import foundation-core.propositions

Idea

A type A is Markovian^¶ if, for every decidable subtype 𝒫 of A, if 𝒫 is not full then there is an element of A that is not in 𝒫.

Definitions

The predicate of being Markovian

We phrase the condition using the type of booleans so that the predicate is small.

is-markovian : {l : Level} → UU l → UU l
is-markovian A =
  (𝒫 : A → bool) →
  ¬ ((x : A) → is-true (𝒫 x)) →
  exists A (λ x → is-false-Prop (𝒫 x))

is-prop-is-markovian : {l : Level} (A : UU l) → is-prop (is-markovian A)
is-prop-is-markovian A =
  is-prop-Π (λ 𝒫 → is-prop-function-type (is-prop-exists A (is-false-Prop ∘ 𝒫)))

The predicate of being Markovian at a universe level

module _
  {l1 : Level} (l2 : Level) (A : UU l1)
  where

  is-markovian-prop-Level : Prop (l1 ⊔ lsuc l2)
  is-markovian-prop-Level =
    Π-Prop
      ( decidable-subtype l2 A)
      ( λ P →
        ¬' (∀' A (subtype-decidable-subtype P)) ⇒
        ∃ A (¬'_ ∘ subtype-decidable-subtype P))

  is-markovian-Level : UU (l1 ⊔ lsuc l2)
  is-markovian-Level =
      (P : decidable-subtype l2 A) →
      ¬ ((x : A) → is-in-decidable-subtype P x) →
      exists A (¬'_ ∘ subtype-decidable-subtype P)

  is-prop-is-markovian-Level : is-prop is-markovian-Level
  is-prop-is-markovian-Level = is-prop-type-Prop is-markovian-prop-Level