------------------------------------------------------------------------
-- Various properties
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

module Delay-monad.Alternative.Properties where

open import Equality.Propositional
open import Interval using (ext; ⟨ext⟩)
open import Logical-equivalence using (_⇔_)
open import Prelude hiding ()

open import Bijection equality-with-J as Bijection using (_↔_)
open import Embedding equality-with-J as Embedding using (Embedding)
open import Equality.Decision-procedures equality-with-J
import Equality.Groupoid equality-with-J as EG
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Groupoid equality-with-J
open import H-level equality-with-J as H-level
open import H-level.Closure equality-with-J
open import Injection equality-with-J using (Injective)
import Nat equality-with-J as N

open import Delay-monad.Alternative

------------------------------------------------------------------------
-- Lemmas related to h-levels

module _ {a} {A : Set a} where

  -- _↑ is a family of propositions.

  ↑-propositional : (x : Maybe A)  Is-proposition (x )
  ↑-propositional nothing =
                                        $⟨ mono (N.zero≤ 2) ⊤-contractible _ _ 
    Is-proposition (tt  tt)            ↝⟨ H-level.respects-surjection (_↔_.surjection Bijection.≡↔inj₁≡inj₁) 1 ⟩□
    Is-proposition (nothing  nothing)  

  ↑-propositional (just x) = [inhabited⇒+]⇒+ 0 (

    just x  nothing           ↝⟨ ⊎.inj₁≢inj₂  sym 
    ⊥₀                         ↝⟨ ⊥-elim ⟩□
    Is-proposition (just x )  )

  -- LE nothing is a family of contractible types.

  LE-nothing-contractible :
    {x : Maybe A}  Contractible (LE nothing x)
  LE-nothing-contractible {x = x} =
    propositional⇒inhabited⇒contractible
      (_⇔_.from propositional⇔irrelevant λ
         { (inj₁ x↑)        (inj₂ (_ , ¬x↑))  ⊥-elim (¬x↑ (sym x↑))
         ; (inj₂ (_ , ¬x↑)) (inj₁ x↑)         ⊥-elim (¬x↑ (sym x↑))

         ; (inj₁ p)         (inj₁ q)         
                                 $⟨ ↑-propositional _ 
           Is-proposition (x )  ↝⟨  hyp  _⇔_.to propositional⇔irrelevant hyp _ _) 
           sym p  sym q         ↔⟨ Eq.≃-≡ $ from-bijection $ Groupoid.⁻¹-bijection (EG.groupoid _) 
           p  q                 ↔⟨ Bijection.≡↔inj₁≡inj₁ ⟩□
           inj₁ p  inj₁ q       

         ; (inj₂ p) (inj₂ q) 
                                               $⟨ ×-closure 1 (↑-propositional _) (¬-propositional ext) 
           Is-proposition (nothing  × ¬ x )  ↝⟨  hyp  _⇔_.to propositional⇔irrelevant hyp _ _) 
           p  q                               ↔⟨ Bijection.≡↔inj₂≡inj₂ ⟩□
           inj₂ p  inj₂ q                     
         })
      (case x return LE nothing of λ
         { nothing   inj₁ refl
         ; (just x)  inj₂ (refl , ⊎.inj₁≢inj₂  sym)
         })

  -- If A is a set, then LE is a family of propositions.

  LE-propositional :
    Is-set A  {x y : Maybe A}  Is-proposition (LE x y)
  LE-propositional A-set = _⇔_.from propositional⇔irrelevant (irr _ _)
    where
    irr :  x y  Proof-irrelevant (LE x y)
    irr nothing _ = _⇔_.to propositional⇔irrelevant $
                      mono₁ 0 LE-nothing-contractible

    irr (just x) (just y) (inj₁ p) (inj₁ q) = cong inj₁ $
      _⇔_.to set⇔UIP (Maybe-closure 0 A-set) p q

    irr (just _) (just _) (inj₂ (() , _))
    irr (just _) (just _) _ (inj₂ (() , _))
    irr (just _) nothing  (inj₁ ())
    irr (just _) nothing  (inj₂ (() , _))

  -- If A is a set, then Increasing is a family of propositions.

  Increasing-propositional :
    Is-set A  {f :   Maybe A}  Is-proposition (Increasing f)
  Increasing-propositional A-set =
    Π-closure ext 1 λ _ 
    LE-propositional A-set

  -- An equality characterisation lemma which applies when A is a set.

  equality-characterisation :
    Is-set A 
    {x y : Delay A}  proj₁ x  proj₁ y  x  y
  equality-characterisation A-set =
    ignore-propositional-component (Increasing-propositional A-set)

  -- If A has h-level 2 + n, then LE {A = A} x y has h-level 2 + n.

  LE-closure :
     {x y} n  H-level (2 + n) A  H-level (2 + n) (LE x y)
  LE-closure n h =
    ⊎-closure n
      (mono₁ (1 + n) (Maybe-closure n h _ _))
      (mono (N.suc≤suc (N.zero≤ (1 + n)))
         (×-closure 1 (↑-propositional _)
                      (¬-propositional ext)))

  -- If A has h-level 2 + n, then Increasing {A = A} f has h-level
  -- 2 + n.

  Increasing-closure :
     {f} n  H-level (2 + n) A  H-level (2 + n) (Increasing f)
  Increasing-closure n h =
    Π-closure ext (2 + n) λ _ 
    LE-closure n h

  -- If A has h-level 2 + n, then Delay A has h-level 2 + n.

  Delay-closure :
     n  H-level (2 + n) A  H-level (2 + n) (Delay A)
  Delay-closure n h =
    Σ-closure (2 + n)
      (Π-closure ext (2 + n) λ _ 
       Maybe-closure n h)
       _  Increasing-closure n h)

------------------------------------------------------------------------
-- Various properties relating _↓_, _↑ and the usual ordering of the
-- natural numbers

module _ {a} {A : Set a} where

  -- If f is increasing and f n has a value, then f (suc n) has the
  -- same value.

  ↓-step :  {f} {x : A} {n} 
           Increasing f  f n  x  f (suc n)  x
  ↓-step {f = f} {x} {n} inc fn↓x = step (inc n)
    module  where
    step : LE (f n) (f (suc n))  f (suc n)  x
    step (inj₁ fn≡f1+n) =

      f (suc n)  ≡⟨ sym fn≡f1+n 
      f n        ≡⟨ fn↓x ⟩∎
      just x     

    step (inj₂ (fn↑ , _)) =

      ⊥-elim $ ⊎.inj₁≢inj₂ (
        nothing  ≡⟨ sym fn↑ 
        f n      ≡⟨ fn↓x ⟩∎
        just x   )

  -- If f is increasing and f (suc n) does not have a value, then
  -- f n does not have a value.

  ↑-step :  {f :   Maybe A} {n} 
           Increasing f  f (suc n)   f n 
  ↑-step {f} {n} inc f1+n↑ with inc n
  ... | inj₁ fn≡f1+n   = f n        ≡⟨ fn≡f1+n 
                         f (suc n)  ≡⟨ f1+n↑ ⟩∎
                         nothing    
  ... | inj₂ (fn↑ , _) = fn↑

  -- If f is increasing and f 0 has a value, then f n has the same
  -- value.

  ↓-upwards-closed₀ :  {f} {x : A} 
                      Increasing f  f 0  x   n  f n  x
  ↓-upwards-closed₀ _   f0↓ zero    = f0↓
  ↓-upwards-closed₀ inc f0↓ (suc n) =
    ↓-upwards-closed₀ (inc  suc) (↓-step inc f0↓) n

  -- If f is increasing, then (λ n → f n ↓ x) is upwards closed.

  ↓-upwards-closed :
     {f :   Maybe A} {m n x} 
    Increasing f  m N.≤ n  f m  x  f n  x
  ↓-upwards-closed _   (N.≤-refl′ refl)     = id
  ↓-upwards-closed inc (N.≤-step′ m≤n refl) =
    ↓-step inc  ↓-upwards-closed inc m≤n

  -- If f is increasing, then (λ n → f n ↑) is downwards closed.

  ↑-downwards-closed :  {f :   Maybe A} {m n} 
                       Increasing f  m N.≤ n  f n   f m 
  ↑-downwards-closed inc (N.≤-refl′ refl)     = id
  ↑-downwards-closed inc (N.≤-step′ m≤n refl) =
    ↑-downwards-closed inc m≤n  ↑-step inc

  -- If f is increasing and f m does not have a value, but f n does
  -- have a value, then m < n.

  ↑<↓ :  {f :   Maybe A} {x m n} 
        Increasing f  f m   f n  x  m N.< n
  ↑<↓ {f} {x} {m} {n} inc fm↑ fn↓x with N.≤⊎> n m
  ... | inj₂ m<n = m<n
  ... | inj₁ n≤m =
    ⊥-elim $ ⊎.inj₁≢inj₂
      (nothing  ≡⟨ sym $ ↑-downwards-closed inc n≤m fm↑ 
       f n      ≡⟨ fn↓x ⟩∎
       just x   )

------------------------------------------------------------------------
-- An unused lemma

private

  -- If the embedding g maps nothing to nothing and just to just, then
  -- there is an isomorphism between Increasing f and
  -- Increasing (g ∘ f).

  Increasing-∘ :
     {a b} {A : Set a} {B : Set b} {f :   Maybe A} 
    (g : Embedding (Maybe A) (Maybe B)) 
    Embedding.to g nothing  nothing 
    (∀ {x}  Embedding.to g (just x)  nothing) 
    Increasing f  Increasing (Embedding.to g  f)
  Increasing-∘ {A = A} {B} {f} g g↑ g↓ = record
    { surjection = record
      { logical-equivalence = record
        { to   = to   ∘_
        ; from = from ∘_
        }
      ; right-inverse-of = ⟨ext⟩  (to∘from ∘_)
      }
    ; left-inverse-of = ⟨ext⟩  (from∘to ∘_)
    }
    where
    g′ : Maybe A  Maybe B
    g′ = Embedding.to g

    g-injective : Injective g′
    g-injective = Embedding.injective (Embedding.is-embedding g)

    lemma₁ :  {x}  x   g′ x 
    lemma₁ refl = g↑

    lemma₂ :  x  ¬ x   ¬ g′ x 
    lemma₂ nothing  x↓ _ = x↓ refl
    lemma₂ (just _) _    = g↓

    lemma₃ :  x  g′ x   x 
    lemma₃ nothing  _   = refl
    lemma₃ (just _) g↓↑ = ⊥-elim (lemma₂ _  ()) g↓↑)

    lemma₄ :  x  g′ x  nothing  x  nothing
    lemma₄ nothing  g↑↓ _  = g↑↓ g↑
    lemma₄ (just _) _   ()

    to :  {n}  Increasing-at n f  Increasing-at n (g′  f)
    to = ⊎-map (cong g′) (Σ-map lemma₁ (lemma₂ _))

    from :  {n}  Increasing-at n (g′  f)  Increasing-at n f
    from = ⊎-map g-injective (Σ-map (lemma₃ _) (lemma₄ _))

    to∘from :  {n} (x : Increasing-at n (g′  f))  to (from x)  x
    to∘from (inj₁ p) = cong inj₁ (
      cong g′ (g-injective p)  ≡⟨ _≃_.right-inverse-of (Embedding.equivalence g) _ ⟩∎
      p                        )
    to∘from (inj₂ _) = cong inj₂ $
      _⇔_.to propositional⇔irrelevant
        (×-closure 1 (↑-propositional _) (¬-propositional ext))
        _ _

    from∘to :  {n} (x : Increasing-at n f)  from (to x)  x
    from∘to (inj₁ p) = cong inj₁ (
      g-injective (cong g′ p)  ≡⟨ _≃_.left-inverse-of (Embedding.equivalence g) _ ⟩∎
      p                        )
    from∘to (inj₂ _) = cong inj₂ $
       _⇔_.to propositional⇔irrelevant
         (×-closure 1 (↑-propositional _) (¬-propositional ext))
         _ _