{-# OPTIONS --safe #-}

open import Prelude

module Swaps {A : Type a} ⦃ _ : IsDiscrete A ⦄ where

_/→_ : A → A → A → A
(x /→ y) z =
  if does (z ≟ x)
    then y
    else z

_/↔_ : A → A → A → A
(x /↔ y) z =
  if does (z ≟ x)
    then y
    else
  if does (z ≟ y)
    then x
    else z

swap-inv : ∀ x y z → (x /↔ y) ((y /↔ x) z) ≡ z
swap-inv x y z with z ≟ y | z ≟ x
... | yes z≡y | _ = cong (bool′ _ _) (it-does (x ≟ x) refl) ⨾ sym z≡y
... | no  z≢y | no  z≢x = cong (bool′ _ _) (it-doesn't (z ≟ x) z≢x) ⨾ cong (bool′ _ _) (it-doesn't (z ≟ y) z≢y)
... | no  z≢y | yes z≡x = cong (bool′ _ _) (it-doesn't (y ≟ x) (z≢y ∘ (z≡x ⨾_) ∘ sym)) ⨾ cong (bool′ _ _) (it-does (y ≟ y) refl) ⨾ sym z≡x

_/͍_ : A → A → A ⟷ A
(x /͍ y) .fst = x /↔ y
(x /͍ y) .snd = y /↔ x

_/⇔_ : A → A → A ⇔ A
(x /⇔ y) .fun = x /↔ y
(x /⇔ y) .inv = y /↔ x
(x /⇔ y) .rightInv = swap-inv x y
(x /⇔ y) .leftInv  = swap-inv y x

swap-leq : ∀ x y → (x /↔ y) x ≡ y
swap-leq x y = cong (bool′ _ _) (it-does (x ≟ x) refl)

swap-req : ∀ x y → (x /↔ y) y ≡ x
swap-req x y with y ≟ x
... | yes y≡x = y≡x
... | no  y≢x = cong (bool′ _ _) (it-does (y ≟ y) refl)


swap-neq : ∀ x y z → x ≢ z → y ≢ z → (x /↔ y) z ≡ z
swap-neq x y z x≢z y≢z = cong (bool′ _ _) (it-doesn't (z ≟ x) (x≢z ∘ sym)) ⨾ cong (bool z x) (it-doesn't (z ≟ y) (y≢z ∘ sym))