------------------------------------------------------------------------ -- 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 @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 □ }