------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe of proposition functors, along with some properties
------------------------------------------------------------------------

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

module Relation.Nullary.Universe where

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary hiding (_⇒_)
import Relation.Binary.Construct.Always as Always
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  as Trivial
open import Data.Sum     as Sum  hiding (map)
open import Data.Sum.Relation.Binary.Pointwise
open import Data.Product as Prod hiding (map)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function
import Function.Equality as FunS
open import Data.Empty
open import Effect.Applicative
open import Effect.Monad
open import Level

infix  5 ¬¬_
infixr 4 _⇒_
infixr 3 _∧_
infixr 2 _∨_
infix  1 ⟨_⟩_≈_

-- The universe.

data PropF p : Set (suc p) where
  Id   : PropF p
  K    : (P : Set p)  PropF p
  _∨_  : (F₁ F₂ : PropF p)  PropF p
  _∧_  : (F₁ F₂ : PropF p)  PropF p
  _⇒_  : (P₁ : Set p) (F₂ : PropF p)  PropF p
  ¬¬_  : (F : PropF p)  PropF p

-- Equalities for universe inhabitants.

mutual

  setoid :  {p}  PropF p  Set p  Setoid p p
  setoid Id        P = PropEq.setoid P
  setoid (K P)     _ = PropEq.setoid P
  setoid (F₁  F₂) P = (setoid F₁ P) ⊎ₛ (setoid F₂ P)
  setoid (F₁  F₂) P = (setoid F₁ P) ×ₛ (setoid F₂ P)
  setoid (P₁  F₂) P = FunS.≡-setoid P₁
                         (Trivial.indexedSetoid (setoid F₂ P))
  setoid (¬¬ F)    P = Always.setoid (¬ ¬  F  P) _

  ⟦_⟧ :  {p}  PropF p  (Set p  Set p)
   F  P = Setoid.Carrier (setoid F P)

⟨_⟩_≈_ :  {p} (F : PropF p) {P : Set p}  Rel ( F  P) p
⟨_⟩_≈_ F = Setoid._≈_ (setoid F _)

-- ⟦ F ⟧ is functorial.

map :  {p} (F : PropF p) {P Q}  (P  Q)   F  P   F  Q
map Id        f  p = f p
map (K P)     f  p = p
map (F₁  F₂) f FP = Sum.map  (map F₁ f) (map F₂ f) FP
map (F₁  F₂) f FP = Prod.map (map F₁ f) (map F₂ f) FP
map (P₁  F₂) f FP = map F₂ f  FP
map (¬¬ F)    f FP = ¬¬-map (map F f) FP

map-id :  {p} (F : PropF p) {P}    F  P  F  map F id  id
map-id Id        x        = refl
map-id (K P)     x        = refl
map-id (F₁  F₂) (inj₁ x) = inj₁ (map-id F₁ x)
map-id (F₁  F₂) (inj₂ y) = inj₂ (map-id F₂ y)
map-id (F₁  F₂) (x , y)  = (map-id F₁ x , map-id F₂ y)
map-id (P₁  F₂) f        = λ x  map-id F₂ (f x)
map-id (¬¬ F)    ¬¬x      = _

map-∘ :  {p} (F : PropF p) {P Q R} (f : Q  R) (g : P  Q) 
          F  P  F  map F f  map F g  map F (f  g)
map-∘ Id        f g x        = refl
map-∘ (K P)     f g x        = refl
map-∘ (F₁  F₂) f g (inj₁ x) = inj₁ (map-∘ F₁ f g x)
map-∘ (F₁  F₂) f g (inj₂ y) = inj₂ (map-∘ F₂ f g y)
map-∘ (F₁  F₂) f g x        = (map-∘ F₁ f g (proj₁ x) ,
                                map-∘ F₂ f g (proj₂ x))
map-∘ (P₁  F₂) f g h        = λ x  map-∘ F₂ f g (h x)
map-∘ (¬¬ F)    f g x        = _

-- A variant of sequence can be implemented for ⟦ F ⟧.

sequence :  {p AF}  RawApplicative AF 
           (AF (Lift p )  ) 
           ({A B : Set p}  (A  AF B)  AF (A  B)) 
            F {P}   F  (AF P)  AF ( F  P)
sequence {AF = AF} A extract-⊥ sequence-⇒ = helper
  where
  open RawApplicative A

  helper :  F {P}   F  (AF P)  AF ( F  P)
  helper Id        x        = x
  helper (K P)     x        = pure x
  helper (F₁  F₂) (inj₁ x) = inj₁ <$> helper F₁ x
  helper (F₁  F₂) (inj₂ y) = inj₂ <$> helper F₂ y
  helper (F₁  F₂) (x , y)  = _,_  <$> helper F₁ x  helper F₂ y
  helper (P₁  F₂) f        = sequence-⇒ (helper F₂  f)
  helper (¬¬ F)    x        =
    pure  ¬FP  x  fp  extract-⊥ (lift  ¬FP <$> helper F fp)))

-- Some lemmas about double negation.

private
  open module M {p} = RawMonad (¬¬-Monad {p = p})

¬¬-pull :  {p} (F : PropF p) {P} 
           F  (¬ ¬ P)  ¬ ¬  F  P
¬¬-pull = sequence rawIApplicative
                    f  f lower)
                    f g  g  x  ⊥-elim (f x  y  g  _  y)))))

¬¬-remove :  {p} (F : PropF p) {P} 
            ¬ ¬  F  (¬ ¬ P)  ¬ ¬  F  P
¬¬-remove F = negated-stable  ¬¬-pull (¬¬ F)