----------------------------------------------------------------------------------------------------
-- 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.Nat
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))

{- 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)