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

{-# OPTIONS --cubical-compatible --safe #-}

module Logical-equivalence where

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

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

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

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

infix  _⇔_

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  _∘_

_∘_ : 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-⇔ : (@ A : Type a) → B ⇔ C → A ⇔ B → A ⇔ C
step-⇔ _ = _∘_

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

finally-⇔ : (@ A : Type a) (@ 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  _×-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  _⊎-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  □
  }