{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Nullary.Reflects where
open import Agda.Builtin.Equality
open import Data.Bool.Base
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
open import Level using (Level)
open import Function.Base using (_$_; _∘_; const; id)
open import Relation.Nullary.Negation.Core
using (¬_; contradiction-irr; contradiction; _¬-⊎_)
open import Relation.Nullary.Recomputable as Recomputable using (Recomputable)
private
variable
a : Level
A B : Set a
data Reflects (A : Set a) : Bool → Set a where
ofʸ : ( a : A) → Reflects A true
ofⁿ : (¬a : ¬ A) → Reflects A false
of : ∀ {b} → if b then A else ¬ A → Reflects A b
of {b = false} ¬a = ofⁿ ¬a
of {b = true } a = ofʸ a
invert : ∀ {b} → Reflects A b → if b then A else ¬ A
invert (ofʸ a) = a
invert (ofⁿ ¬a) = ¬a
recompute : ∀ {b} → Reflects A b → Recomputable A
recompute (ofʸ a) _ = a
recompute (ofⁿ ¬a) a = contradiction-irr a ¬a
recompute-constant : ∀ {b} (r : Reflects A b) (p q : A) →
recompute r p ≡ recompute r q
recompute-constant = Recomputable.recompute-constant ∘ recompute
infixr 1 _⊎-reflects_
infixr 2 _×-reflects_ _→-reflects_
T-reflects : ∀ b → Reflects (T b) b
T-reflects true = of _
T-reflects false = of id
¬-reflects : ∀ {b} → Reflects A b → Reflects (¬ A) (not b)
¬-reflects (ofʸ a) = of (_$ a)
¬-reflects (ofⁿ ¬a) = of ¬a
_×-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
Reflects (A × B) (a ∧ b)
ofʸ a ×-reflects ofʸ b = of (a , b)
ofʸ a ×-reflects ofⁿ ¬b = of (¬b ∘ proj₂)
ofⁿ ¬a ×-reflects _ = of (¬a ∘ proj₁)
_⊎-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
Reflects (A ⊎ B) (a ∨ b)
ofʸ a ⊎-reflects _ = of (inj₁ a)
ofⁿ ¬a ⊎-reflects ofʸ b = of (inj₂ b)
ofⁿ ¬a ⊎-reflects ofⁿ ¬b = of (¬a ¬-⊎ ¬b)
_→-reflects_ : ∀ {a b} → Reflects A a → Reflects B b →
Reflects (A → B) (not a ∨ b)
ofʸ a →-reflects ofʸ b = of (const b)
ofʸ a →-reflects ofⁿ ¬b = of (¬b ∘ (_$ a))
ofⁿ ¬a →-reflects _ = of (λ a → contradiction a ¬a)
fromEquivalence : ∀ {b} → (T b → A) → (A → T b) → Reflects A b
fromEquivalence {b = true} sound complete = of (sound _)
fromEquivalence {b = false} sound complete = of complete
det : ∀ {b b′} → Reflects A b → Reflects A b′ → b ≡ b′
det (ofʸ a) (ofʸ _) = refl
det (ofʸ a) (ofⁿ ¬a) = contradiction a ¬a
det (ofⁿ ¬a) (ofʸ a) = contradiction a ¬a
det (ofⁿ ¬a) (ofⁿ _) = refl
T-reflects-elim : ∀ {a b} → Reflects (T a) b → b ≡ a
T-reflects-elim {a} r = det r (T-reflects a)