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

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

module Logical-equivalence where

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

private
  variable
    a b p      : Level
    @0 A B C D : Type a
    @0 P Q     : A  Type p

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

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

infix 0 _⇔_

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

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

-- _⇔_ is an equivalence relation.

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

inverse : A  B  B  A
inverse A⇔B ._⇔_.to   = let record { from = from } = A⇔B in from
inverse A⇔B ._⇔_.from = let record { to   = to   } = A⇔B in to

infixr 9 _∘_

_∘_ : B  C  A  B  A  C
(f  g) ._⇔_.to =
  let record { to = f-to } = f
      record { to = g-to } = g
  in f-to  g-to
(f  g) ._⇔_.from =
  let record { from = f-from } = f
      record { from = g-from } = g
  in g-from  f-from

-- "Equational" reasoning combinators.

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

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

step-⇔ : (@0 A : Type a)  B  C  A  B  A  C
step-⇔ _ = _∘_

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

finally-⇔ : (@0 A : Type a) (@0 B : Type b)  A  B  A  B
finally-⇔ _ _ A⇔B = A⇔B

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

------------------------------------------------------------------------
-- Preservation lemmas

-- Note that all of the type arguments of these lemmas are erased.

-- _⊎_ preserves logical equivalences.

infixr 2 _×-cong_

_×-cong_ : A  C  B  D  A × B  C × D
A⇔C ×-cong B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = Σ-map to₁   to₂
    ; from = Σ-map from₁ from₂
    }

-- ∃ preserves logical equivalences.

∃-cong : (∀ x  P x  Q x)   P   Q
∃-cong P⇔Q = record
  { to   = λ (x , y)  x , let record { to   = to   } = P⇔Q x in to   y
  ; from = λ (x , y)  x , let record { from = from } = P⇔Q x in from y
  }

-- _⊎_ preserves logical equivalences.

infixr 1 _⊎-cong_

_⊎-cong_ : A  C  B  D  A  B  C  D
A⇔C ⊎-cong B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = ⊎-map to₁   to₂
    ; from = ⊎-map from₁ from₂
    }

-- The non-dependent function space preserves logical equivalences.

→-cong : A  C  B  D  (A  B)  (C  D)
→-cong A⇔C B⇔D =
  let record { to = to₁; from = from₁ } = A⇔C
      record { to = to₂; from = from₂ } = B⇔D
  in
  record
    { to   = (to₂   ⊚_)  (_⊚ from₁)
    ; from = (from₂ ⊚_)  (_⊚ to₁)
    }

-- Π preserves logical equivalences in its second argument.

∀-cong :
  ((x : A)  P x  Q x) 
  ((x : A)  P x)  ((x : A)  Q x)
∀-cong P⇔Q = record
  { to   = λ f x  let record { to   = to   } = P⇔Q x in to   (f x)
  ; from = λ f x  let record { from = from } = P⇔Q x in from (f x)
  }

-- The implicit variant of Π preserves logical equivalences in its
-- second argument.

implicit-∀-cong :
  ({x : A}  P x  Q x) 
  ({x : A}  P x)  ({x : A}  Q x)
implicit-∀-cong P⇔Q = record
  { to   = λ f  let record { to   = to   } = P⇔Q in to   f
  ; from = λ f  let record { from = from } = P⇔Q in from f
  }

-- ↑ preserves logical equivalences.

↑-cong : B  C   a B   a C
↑-cong B⇔C =
  let record { to = to; from = from } = B⇔C in
  record
    { to   = λ (lift x)  lift (to   x)
    ; from = λ (lift x)  lift (from x)
    }

-- _⇔_ preserves logical equivalences.

⇔-cong : A  B  C  D  (A  C)  (B  D)
⇔-cong {A = A} {B = B} {C = C} {D = D} A⇔B C⇔D = record
  { to   = λ A⇔C 
             B  ⇔⟨ inverse A⇔B 
             A  ⇔⟨ A⇔C 
             C  ⇔⟨ C⇔D ⟩□
             D  
  ; from = λ B⇔D 
             A  ⇔⟨ A⇔B 
             B  ⇔⟨ B⇔D 
             D  ⇔⟨ inverse C⇔D ⟩□
             C  
  }