----------------------------------------------------------------------------------------------------
-- Some general properties for the development
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module General-Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary
open BinaryRelation
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Iff

{- A *truncated relation* is a set `A` and a relation `A → A → Set`
   that is valued in propositions. -}

isTruncatedRelation : {A : Set} -> (_<_ : A -> A -> Set) -> Set
isTruncatedRelation {A} _<_ = isSet A × isPropValued _<_

{- Extensionality -}

isExtensional : {A : Set} -> (_<_ : A -> A -> Set) -> Set
isExtensional {A} _<_ = (a b : A) → ((c : A) → (c < a ↔ c < b)) → a ≡ b

{- Law of excluded middle -}

LEM : Type₁
LEM = (P : Type) -> isProp P -> Dec P

LEM-¬∀-∃ : ∀ {A : Set} (P : A -> Set) -> LEM -> ¬ ((x : A) -> ¬ P x) -> ∃ A P
LEM-¬∀-∃ {A} P lem P-impossible with lem (∃ A P) ∥_∥.squash
... | yes p = p
... | no ¬a,p = ⊥.elim (P-impossible λ a → λ p → ¬a,p ∣ a , p ∣)

DNE : Type₁
DNE = (P : Type) → isProp P → ¬ (¬ P) → P

LEM-to-DNE : LEM → DNE
LEM-to-DNE lem P pP ¬¬p with (lem P pP)
... | yes p = p
... | no ¬p = ⊥.elim (¬¬p ¬p)

LEM-¬∀-∃¬ : ∀ {A : Type} (P : A → Type) → (∀ a → isProp (P a)) →
            LEM → ¬ (∀ x → P x) → ∃ A (\x → ¬ P x)
LEM-¬∀-∃¬ {A} P pvP lem f = LEM-¬∀-∃ _ lem g
 where
  g : ¬ (∀ x → ¬ (¬ P x))
  g h = f (λ x → LEM-to-DNE lem (P x) (pvP x) (h x))

WLPO : Type
WLPO = (s : ℕ → Bool) → (∀ k → s k ≡ false) ⊎ (¬ (∀ k → s k ≡ false))

{- Wellfoundedness implies that there is no infinite descending sequence. -}

no-infinite-descending-sequence : ∀ {A _<_} → isWellFounded _<_ →
                                  ¬ (Σ[ f ∈ (ℕ -> A) ] (∀ i → f (suc i) < f i))
no-infinite-descending-sequence {A} {_<_} wf (f , inf-desc) =
  WFI.induction wf {P = P} step (f 0) (f , refl , inf-desc)
  where
    P : A -> Set
    P a = ¬ (Σ[ f ∈ (ℕ -> A) ] (f 0 ≡ a) × (∀ i → f (suc i) < f i))
    step : (x : A) → ((y : A) → y < x → P y) → P x
    step x q (f , f0≡x , inf-desc-f) =
      q (f 1) (subst (f 1 <_) f0≡x (inf-desc-f 0))
              (f ∘ suc , refl , λ i → inf-desc-f (suc i))

{- Wellfoundedness implies irreflexivity. -}

wellfounded→irreflexive : ∀ {A _<_} → isWellFounded _<_ → (x : A) → ¬ (x < x)
wellfounded→irreflexive is-wf x x<x = no-infinite-descending-sequence is-wf ((λ n → x) , λ n → x<x)

isIrrefl : ∀ {ℓ ℓ'} {A : Type ℓ} → (A → A → Type ℓ') → Type _
isIrrefl _<_ = ∀ x → ¬ (x < x)

isAntisym : ∀ {ℓ ℓ'} {A : Type ℓ} → (A → A → Type ℓ') → Type _
isAntisym _≤_ = ∀ x y → x ≤ y → y ≤ x → x ≡ y

isTrichotomous : ∀ {ℓ ℓ'} {A : Type ℓ} → (A → A → Type ℓ') → Type _
isTrichotomous _<_ = ∀ x y → (x < y) ⊎ ((y < x) ⊎ (x ≡ y))

isConvex : ∀ {ℓ ℓ'} {A : Type ℓ} → (A → A → Type ℓ') → Type _
isConvex _≤_ = ∀ x y → (x ≤ y) ⊎ (y ≤ x)