open import 1Lab.Prelude
open import Data.Dec
open import Data.Sum

module StringLab.Equiv where

private variable
  ℓ ℓ' : Level
  A B C D : Type ℓ

Results about equivalences🔗

This module collects some basic facts about equivalences that I proved in the course of development of the StringLab.

If $B$ is equivalent to $C\text{,}$ then $A\times B$ is equivalent to $A\times C\text{.}$

×-apr : (A → B ≃ C) → (A × B) ≃ (A × C)
×-apr e = Σ-ap id≃ e

×-apl : (C → A ≃ B) → (A × C) ≃ (B × C)
×-apl e = ×-swap ∙e ×-apr e ∙e ×-swap

If $A$ is empty, then the disjoint union $A+B$ is equivalent to $B\text{.}$

⊎-emptyl : ¬ A → (A ⊎ B) ≃ B
⊎-emptyl ¬a = ⊎-apl (is-empty→≃ ¬a id) ∙e ⊎-zerol

⊎-emptyr : ¬ B → (A ⊎ B) ≃ A
⊎-emptyr ¬b = ⊎-apr (is-empty→≃ ¬b id) ∙e ⊎-zeror

If $A$ is contractible, then $B$ is equivalent to $A\times B\text{.}$

lens-introl : is-contr A → B ≃ (A × B)
lens-introl (contr a p) =
  Iso→Equiv $
    (a ,_) ,
    iso snd
      (λ ab → p (ab .fst) ,ₚ refl)
      (λ b → refl)

Singleton types are contractible.

singleton-is-contr : ∀ {A : Type ℓ} (x : A) → is-contr (Σ[ a ∈ A ] a ≡ x)
singleton-is-contr {A = A} x .centre = x , refl
singleton-is-contr {A = A} x .paths (y , p) =
  transp (λ i → Path (Σ[ a ∈ A ] a ≡ x) (x , refl) (p (~ i) , λ j → p (~ i ∨ j))) i0 refl

One of the 4 De Morgan laws are not constructively valid unless $A$ and $B$ are decidable. Moreover, if $A$ and $B$ are general types, then we have a more refined form of De Morgan that distinguishes between one type being non-empty, and both types being nonempty!

Dec→demorgan≃
  : ⦃ _ : H-Level A  ⦄  ⦃ _ : H-Level B  ⦄
  → ⦃ _ : Dec A ⦄ ⦃ _ : Dec B ⦄
  → (¬ (A × B)) ≃ ((¬ A × B) ⊎ (A × ¬ B) ⊎ (¬ A × ¬ B))
Dec→demorgan≃ {A = A} {B = B} with holds? A | holds? B
... | yes a | yes b =
  is-empty→≃ (λ ¬ab → ¬ab (a , b)) λ where
    (inl (¬a , b)) → ¬a a
    (inr (inl (a , ¬b))) → ¬b b
    (inr (inr (¬a , ¬b))) → ¬b b
... | no ¬a | yes b =
  ¬ (A × B)                             ≃⟨ prop-ext! (λ _ → ¬a , b) (λ _ → ¬a ∘ fst) ⟩≃
  (¬ A × B)                             ≃˘⟨ ⊎-emptyr (¬a ∘ fst) ⟩≃˘
  (¬ A × B) ⊎ (A × ¬ B)                 ≃˘⟨ ⊎-apr (⊎-emptyr λ (_ , ¬b) → ¬b b) ⟩≃˘
  ((¬ A × B) ⊎ (A × ¬ B) ⊎ (¬ A × ¬ B)) ≃∎
... | yes a | no ¬b =
  ¬ (A × B)                             ≃⟨ prop-ext! (λ _ → a , ¬b) (λ _ → ¬b ∘ snd) ⟩≃
  (A × ¬ B)                             ≃˘⟨ ⊎-emptyr (λ (¬a , _) → ¬a a) ⟩≃˘
  (A × ¬ B) ⊎ (¬ A × ¬ B)               ≃˘⟨ ⊎-emptyl (¬b ∘ snd) ⟩≃˘
  ((¬ A × B) ⊎ (A × ¬ B) ⊎ (¬ A × ¬ B)) ≃∎
... | no ¬a | no ¬b =
  ¬ (A × B)                             ≃⟨ prop-ext! (λ _ → ¬a , ¬b) (λ _ → ¬a ∘ fst) ⟩≃
  (¬ A × ¬ B)                           ≃˘⟨ ⊎-emptyl (¬a ∘ fst) ⟩≃˘
  (A × ¬ B) ⊎ (¬ A × ¬ B)               ≃˘⟨ ⊎-emptyl (¬b ∘ snd) ⟩≃˘
  ((¬ A × B) ⊎ (A × ¬ B) ⊎ (¬ A × ¬ B)) ≃∎