-- The Agda standard library
-- Properties of the `Reflects` construct

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

module Relation.Nullary.Reflects where

open import Agda.Builtin.Equality
open import Data.Bool.Base
open import Data.Empty
open import Level
open import Relation.Nullary

    p : Level
    P : Set p

-- `Reflects P b` is equivalent to `if b then P else ¬ P`.

-- These lemmas are intended to be used mostly when `b` is a value, so
-- that the `if` expressions have already been evaluated away.
-- In this case, `of` works like the relevant constructor (`ofⁿ` or
-- `ofʸ`), and `invert` strips off the constructor to just give either
-- the proof of `P` or the proof of `¬ P`.

of :  {b}  if b then P else ¬ P  Reflects P b
of {b = false} ¬p = ofⁿ ¬p
of {b = true }  p = ofʸ p

invert :  {b}  Reflects P b  if b then P else ¬ P
invert (ofʸ  p) = p
invert (ofⁿ ¬p) = ¬p

-- Other lemmas

fromEquivalence :  {b}  (T b  P)  (P  T b)  Reflects P b
fromEquivalence {b = true}  sound complete = ofʸ (sound _)
fromEquivalence {b = false} sound complete = ofⁿ complete

-- `Reflects` is deterministic.
det :  {b b′}  Reflects P b  Reflects P b′  b  b′
det (ofʸ  p) (ofʸ  p′) = refl
det (ofʸ  p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p)
det (ofⁿ ¬p) (ofʸ  p′) = ⊥-elim (¬p p′)
det (ofⁿ ¬p) (ofⁿ ¬p′) = refl