------------------------------------------------------------------------
-- Logical equivalences
------------------------------------------------------------------------

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

module Logical-equivalence where

open import Prelude as P hiding (id) renaming (_∘_ to _⊚_)

------------------------------------------------------------------------
-- Logical equivalence

-- A ⇔ B means that A and B are logically equivalent.

infix 0 _⇔_

record _⇔_ {f t} (From : Set f) (To : Set t) : Set (f  t) where
  field
    to   : From  To
    from : To  From

------------------------------------------------------------------------
-- Equivalence relation

-- _⇔_ is an equivalence relation.

id :  {a} {A : Set a}  A  A
id = record
  { to   = P.id
  ; from = P.id
  }

inverse :  {a b} {A : Set a} {B : Set b}  A  B  B  A
inverse A⇔B = record
  { to               = from
  ; from             = to
  } where open _⇔_ A⇔B

infixr 9 _∘_

_∘_ :  {a b c} {A : Set a} {B : Set b} {C : Set c} 
      B  C  A  B  A  C
f  g = record
  { to   = to   f  to   g
  ; from = from g  from f
  } where open _⇔_

-- "Equational" reasoning combinators.

infix  -1 finally-⇔
infixr -2 step-⇔

-- For an explanation of why step-⇔ is defined in this way, see
-- Equality.step-≡.

step-⇔ :  {a b c} (A : Set a) {B : Set b} {C : Set c} 
         B  C  A  B  A  C
step-⇔ _ = _∘_

syntax step-⇔ A B⇔C A⇔B = A ⇔⟨ A⇔B  B⇔C

finally-⇔ :  {a b} (A : Set a) (B : Set b)  A  B  A  B
finally-⇔ _ _ A⇔B = A⇔B

syntax finally-⇔ A B A⇔B = A ⇔⟨ A⇔B ⟩□ B 

------------------------------------------------------------------------
-- A lemma

-- Dec preserves logical equivalences.

Dec-preserves : {A B : Set}  A  B  Dec A  Dec B
Dec-preserves A⇔B = record
  { to   = lemma A⇔B
  ; from = lemma (inverse A⇔B)
  }
  where
  lemma : {A B : Set}  A  B  Dec A  Dec B
  lemma A⇔B = ⊎-map to  ¬A  ¬A  from)
    where open _⇔_ A⇔B