Programming Language Foundations in Agda: Connectives

Connectives.agda

module Connectives where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
open Isomorphism._⇔_
open Isomorphism.≃-Reasoning

data _×_ (A B : Set) : Set where
    ⟨_,_⟩ : A → B → A × B

infixr 2 _×_

proj₁ : ∀ {A B : Set} → A × B → A
proj₁ ⟨ a , b ⟩ = a

proj₂ : ∀ {A B : Set} → A × B → B
proj₂ ⟨ a , b ⟩ = b

η-× : ∀ {A B : Set} (a×b : A × B) → ⟨ proj₁ a×b , proj₂ a×b ⟩ ≡ a×b
η-× ⟨ a , b ⟩ = refl

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
    record
        { to       = λ { ⟨ a , b ⟩ → ⟨ b , a ⟩ }
        ; from     = λ { ⟨ b , a ⟩ → ⟨ a , b ⟩ }
        ; from∘to  = λ { ⟨ a , b ⟩ → refl }
        ; to∘from  = λ { ⟨ b , a ⟩ → refl }
        }

×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
×-assoc =
    record
        { to      = λ { ⟨ ⟨ a , b ⟩ , c ⟩ → ⟨ a , ⟨ b , c ⟩ ⟩ }
        ; from    = λ { ⟨ a , ⟨ b , c ⟩ ⟩ → ⟨ ⟨ a , b ⟩ , c ⟩ }
        ; from∘to = λ { ⟨ ⟨ a , b ⟩ , c ⟩ → refl }
        ; to∘from = λ { ⟨ a , ⟨ b , c ⟩ ⟩ → refl }
        }

⇔≃× : ∀ {A B : Set} → A ⇔ B ≃ (A → B) × (B → A)
⇔≃× {A} {B} =
    record
        { to      = to'
        ; from    = from'
        ; from∘to = λ { x → from' (to' x) ∎ }
        ; to∘from = λ { x@(⟨ A→B , B→A ⟩) → to' (from' x) ∎ }
        }
    where
    to' : A ⇔ B → (A → B) × (B → A)
    to' A⇔B = ⟨ to A⇔B , from A⇔B ⟩
    from' : (A → B) × (B → A) → A ⇔ B
    from' A×B = record { to = proj₁ A×B ; from = proj₂ A×B }

data ⊤ : Set where
    tt : ⊤

data _⊎_ (A B : Set) : Set where
    inj₁ : A → A ⊎ B
    inj₂ : B → A ⊎ B

infix 1 _⊎_

case-⊎ : ∀ {A B C : Set} → (A → C) → (B → C) → A ⊎ B → C
case-⊎ f g = λ { (inj₁ x) → f x ; (inj₂ y) → g y }

η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl

uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B)
    → case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl

⊎-comm : ∀ {A B : Set} → A ⊎ B ≃ B ⊎ A
⊎-comm =
    record
        { to       = swap
        ; from     = swap
        ; from∘to  = swap∘swap
        ; to∘from  = swap∘swap
        }
    where
    swap : ∀ {A B : Set} → A ⊎ B → B ⊎ A
    swap x = case-⊎ inj₂ inj₁ x

    swap∘swap : ∀ {A B : Set} (x : A ⊎ B) → swap (swap x) ≡ x
    swap∘swap (inj₁ a) = refl
    swap∘swap (inj₂ a) = refl

⊎-assoc : ∀ {A B C : Set} → (A ⊎ B) ⊎ C ≃ A ⊎ (B ⊎ C)
⊎-assoc {A} {B} {C} =
    record
        { to      = to'
        ; from    = from'
        ; from∘to = from∘to'
        ; to∘from = to∘from'
        }
    where
    to' : (A ⊎ B) ⊎ C → A ⊎ (B ⊎ C)
    to' (inj₁ (inj₁ x)) = inj₁ x
    to' (inj₁ (inj₂ x)) = inj₂ (inj₁ x)
    to' (inj₂ x)        = inj₂ (inj₂ x)

    from' : A ⊎ (B ⊎ C) → (A ⊎ B) ⊎ C
    from' (inj₁ x)        = inj₁ (inj₁ x)
    from' (inj₂ (inj₁ x)) = inj₁ (inj₂ x)
    from' (inj₂ (inj₂ x)) = inj₂ x

    from∘to' : (x : (A ⊎ B) ⊎ C) → from' (to' x) ≡ x
    from∘to' (inj₁ (inj₁ x)) = refl
    from∘to' (inj₁ (inj₂ x)) = refl
    from∘to' (inj₂ x)        = refl

    to∘from' : (x : A ⊎ (B ⊎ C)) → to' (from' x) ≡ x
    to∘from' (inj₁ x)        = refl
    to∘from' (inj₂ (inj₁ x)) = refl
    to∘from' (inj₂ (inj₂ x)) = refl

data ⊥ : Set where

⊥-identityˡ : ∀ {A : Set} → ⊥ ⊎ A ≃ A
⊥-identityˡ {A} =
    record
        { to      = λ { (inj₂ x) → x }
        ; from    = λ { x → inj₂ x }
        ; from∘to = λ { (inj₂ x) → refl }
        ; to∘from = λ { x → refl }
        }

⊥-identityʳ : ∀ {A : Set} → A ⊎ ⊥ ≃ A
⊥-identityʳ {A} = ≃-begin
    (A ⊎ ⊥)       ≃⟨ ⊎-comm ⟩
    (⊥ ⊎ A)       ≃⟨ ⊥-identityˡ ⟩
    A             ≃-∎

currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
    record
        { to      = λ { f ⟨ a , b ⟩ → f a b }
        ; from    = λ { f a b → f ⟨ a , b ⟩ }
        ; from∘to = λ { f → refl }
        ; to∘from = λ { f → extensionality λ { ⟨ a , b ⟩ → refl } }
        }

→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ (A → C) × (B → C)
→-distrib-⊎ =
    record
        { to      = λ { f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ }
        ; from    = λ { ⟨ f , g ⟩ → case-⊎ f g }
        ; from∘to = λ { f → extensionality λ { (inj₁ x) → refl ; (inj₂ x) → refl } }
        ; to∘from = λ { ⟨ f , g ⟩ → refl }
        }

→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
    record
        { to      = λ { f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ }
        ; from    = λ { ⟨ f , g ⟩ x → ⟨ f x , g x ⟩ }
        ; from∘to = λ { f → extensionality λ { x → η-× (f x) } }
        ; to∘from = λ { ⟨ f , g ⟩ → refl }
        }

×-distrib-⊎ : ∀ {a b c : Set} → (a ⊎ b) × c ≃ (a × c) ⊎ (b × c)
×-distrib-⊎ = record
    { to = λ { ⟨ inj₁ a , c ⟩ → inj₁ ⟨ a , c ⟩
             ; ⟨ inj₂ b , c ⟩ → inj₂ ⟨ b , c ⟩
             }
    ; from = λ { (inj₁ ⟨ a , c ⟩) → ⟨ inj₁ a , c ⟩
               ; (inj₂ ⟨ b , c ⟩) → ⟨ inj₂ b , c ⟩
               }
    ; from∘to = λ { ⟨ inj₁ a , c ⟩ → refl ; ⟨ inj₂ b , c ⟩ → refl }
    ; to∘from = λ { (inj₁ ⟨ a , c ⟩) → refl ; (inj₂ ⟨ b , c ⟩) → refl }
    }

⊎-distrib-× : ∀ {a b c : Set} → (a × b) ⊎ c ≲ (a ⊎ c) × (b ⊎ c)
⊎-distrib-× = record
    { to = λ { (inj₁ ⟨ a , b ⟩) → ⟨ inj₁ a , inj₁ b ⟩
             ; (inj₂ c)         → ⟨ inj₂ c , inj₂ c ⟩
             }
    ; from = λ { ⟨ inj₁ a , inj₁ b ⟩ → inj₁ ⟨ a , b ⟩
               ; ⟨ inj₂ c , _      ⟩ → inj₂ c
               ; ⟨ _      , inj₂ c ⟩ → inj₂ c
               }
    ; from∘to = λ { (inj₁ ⟨ a , b ⟩) → refl
                  ; (inj₂ c)         → refl
                  }
    }

⊎-weak-× : ∀ {a b c : Set} → (a ⊎ b) × c → a ⊎ (b × c)
⊎-weak-× ⟨ inj₁ a , c ⟩ = inj₁ a
⊎-weak-× ⟨ inj₂ b , c ⟩ = inj₂ ⟨ b , c ⟩

⊎×-implies-×⊎ : ∀ {a b c d : Set} → (a × b) ⊎ (c × d) → (a ⊎ c) × (b ⊎ d)
⊎×-implies-×⊎ (inj₁ ⟨ a , b ⟩) = ⟨ inj₁ a , inj₁ b ⟩
⊎×-implies-×⊎ (inj₂ ⟨ c , d ⟩) = ⟨ inj₂ c , inj₂ d ⟩