```------------------------------------------------------------------------
-- A universe of proposition functors, along with some properties
------------------------------------------------------------------------

module Relation.Nullary.Universe where

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.Simple
import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)
open import Relation.Binary.Sum
open import Relation.Binary.Product.Pointwise
open import Relation.Binary.FunctionLifting
import Data.Sum     as Sum;  open Sum  hiding (map)
import Data.Product as Prod; open Prod hiding (map)
open import Data.Function
open import Data.Empty
open import Category.Applicative

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

-- The universe.

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

⟦_⟧ : PropF → (Set → Set)
⟦ Id ⟧      = λ x → x
⟦ K P ⟧     = λ _ → P
⟦ F₁ ∨ F₂ ⟧ = λ x → ⟦ F₁ ⟧ x ⊎ ⟦ F₂ ⟧ x
⟦ F₁ ∧ F₂ ⟧ = λ x → ⟦ F₁ ⟧ x × ⟦ F₂ ⟧ x
⟦ P₁ ⇒ F₂ ⟧ = λ x → P₁       → ⟦ F₂ ⟧ x
⟦ ¬¬ F ⟧    = λ x → ¬ ¬ ⟦ F ⟧ x

-- Equalities for universe inhabitants.

Eq : (F : PropF) {P : Set} → Rel (⟦ F ⟧ P)
Eq Id        = _≡_
Eq (K P)     = _≡_
Eq (F₁ ∨ F₂) = Eq F₁ ⊎-Rel Eq F₂
Eq (F₁ ∧ F₂) = Eq F₁ ×-Rel Eq F₂
Eq (P₁ ⇒ F₂) = ≡↝ (λ _ → Eq F₂)
Eq (¬¬ F)    = Always

⟨_⟩_≈_ : (F : PropF) {P : Set} → Rel (⟦ F ⟧ P)
⟨_⟩_≈_ = Eq

isEquivalence : ∀ F {P} → IsEquivalence (Eq F {P})
isEquivalence Id        = PropEq.isEquivalence
isEquivalence (K P)     = PropEq.isEquivalence
isEquivalence (F₁ ∨ F₂) = isEquivalence F₁ ⊎-isEquivalence
isEquivalence F₂
isEquivalence (F₁ ∧ F₂) = isEquivalence F₁ ×-isEquivalence
isEquivalence F₂
isEquivalence (P₁ ⇒ F₂) = LiftEquiv≡ (λ _ → isEquivalence F₂)
isEquivalence (¬¬ F)    = Always-isEquivalence

-- ⟦ F ⟧ is functorial.

map : ∀ F {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 : ∀ F {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) = ₁∼₁ (map-id F₁ x)
map-id (F₁ ∨ F₂) (inj₂ y) = ₂∼₂ (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-∘ : ∀ F {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) = ₁∼₁ (map-∘ F₁ f g x)
map-∘ (F₁ ∨ F₂) f g (inj₂ y) = ₂∼₂ (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 : ∀ {AF} → RawApplicative AF →
(AF ⊥ → ⊥) →
({A B : Set} → (A → AF B) → AF (A → B)) →
∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
sequence {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-⊥ (¬FP <\$> helper F fp)))

-- Some lemmas about double negation.