------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic lemmas showing that various types are related (isomorphic or
-- equivalent or…)
------------------------------------------------------------------------

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

module Function.Related.TypeIsomorphisms where

open import Algebra
open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Bool.Base using (true; false)
open import Data.Empty using (⊥-elim)
open import Data.Empty.Polymorphic using () renaming (⊥-elim to ⊥ₚ-elim)
open import Data.Product.Base as Prod
  using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; )
open import Data.Product.Function.NonDependent.Propositional
open import Data.Sum.Base as Sum
open import Data.Sum.Properties using (swap-involutive)
open import Data.Sum.Function.Propositional using (_⊎-cong_)
open import Data.Unit.Polymorphic using ()
open import Level using (Level; Lift; 0ℓ; suc)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence as Eq using (_⇔_; Equivalence)
open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
open import Function.Related
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
import Relation.Nullary.Indexed as I
open import Relation.Nullary.Decidable using (True)

------------------------------------------------------------------------
-- Properties of Σ and _×_

-- Σ is associative
Σ-assoc :  {a b c}
            {A : Set a} {B : A  Set b} {C : (a : A)  B a  Set c} 
          Σ (Σ A B) (uncurry C)  Σ A  a  Σ (B a) (C a))
Σ-assoc = inverse  where ((a , b) , c)  (a , b , c))
                   where (a , b , c)  ((a , b) , c))
                   _  P.refl)  _  P.refl)

-- × is commutative

×-comm :  {a b} (A : Set a) (B : Set b)  (A × B)  (B × A)
×-comm _ _ = inverse Prod.swap Prod.swap  _  P.refl) λ _  P.refl

-- × has ⊤ as its identity

×-identityˡ :    LeftIdentity _↔_ ( {}) _×_
×-identityˡ _ _ = inverse proj₂ -,_  _  P.refl)  _  P.refl)

×-identityʳ :    RightIdentity _↔_ ( {}) _×_
×-identityʳ _ _ = inverse proj₁ (_, _)  _  P.refl)  _  P.refl)

×-identity :    Identity _↔_  _×_
×-identity  = ×-identityˡ  , ×-identityʳ 

-- × has ⊥ has its zero

×-zeroˡ :    LeftZero _↔_ ( {}) _×_
×-zeroˡ  A = inverse proj₁ < id , ⊥ₚ-elim >  { () })  _  P.refl)

×-zeroʳ :    RightZero _↔_ ( {}) _×_
×-zeroʳ  A = inverse proj₂ < ⊥ₚ-elim , id >  { () }) λ _  P.refl

×-zero :    Zero _↔_  _×_
×-zero   = ×-zeroˡ  , ×-zeroʳ 

------------------------------------------------------------------------
-- Properties of ⊎

-- ⊎ is associative

⊎-assoc :    Associative { = } _↔_ _⊎_
⊎-assoc  _ _ _ = inverse
  [ [ inj₁ , inj₂ ∘′ inj₁ ]′ , inj₂ ∘′ inj₂ ]′
  [ inj₁ ∘′ inj₁ , [ inj₁ ∘′ inj₂ , inj₂ ]′ ]′
  [ [  _  P.refl) ,  _  P.refl) ] ,  _  P.refl) ]
  [  _  P.refl) , [  _  P.refl) ,  _  P.refl) ] ]

-- ⊎ is commutative

⊎-comm :  {a b} (A : Set a) (B : Set b)  (A  B)  (B  A)
⊎-comm _ _ = inverse swap swap swap-involutive swap-involutive

-- ⊎ has ⊥ as its identity

⊎-identityˡ :    LeftIdentity _↔_ ( {}) _⊎_
⊎-identityˡ _ _ = inverse [  ()) , id ]′ inj₂
                          [  ()) ,  _  P.refl) ]  _  P.refl)

⊎-identityʳ :    RightIdentity _↔_ ( {}) _⊎_
⊎-identityʳ _ _ = inverse [ id ,  ()) ]′ inj₁
                          [  _  P.refl) ,  ()) ]  _  P.refl)

⊎-identity :    Identity _↔_  _⊎_
⊎-identity  = ⊎-identityˡ  , ⊎-identityʳ 

------------------------------------------------------------------------
-- Properties of × and ⊎

-- × distributes over ⊎

×-distribˡ-⊎ :    _DistributesOverˡ_ { = } _↔_ _×_ _⊎_
×-distribˡ-⊎  _ _ _ = inverse
  (uncurry λ x  [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
  [ Prod.map₂ inj₁ , Prod.map₂ inj₂ ]′
  (uncurry λ _  [  _  P.refl) ,  _  P.refl) ])
  [  _  P.refl) ,  _  P.refl) ]

×-distribʳ-⊎ :    _DistributesOverʳ_ { = } _↔_ _×_ _⊎_
×-distribʳ-⊎  _ _ _ = inverse
  (uncurry [ curry inj₁ , curry inj₂ ]′)
  [ Prod.map₁ inj₁ , Prod.map₁ inj₂ ]′
  (uncurry [  _ _  P.refl) ,  _ _  P.refl) ])
  [  _  P.refl) ,  _  P.refl) ]

×-distrib-⊎ :    _DistributesOver_ { = } _↔_ _×_ _⊎_
×-distrib-⊎  = ×-distribˡ-⊎  , ×-distribʳ-⊎ 

------------------------------------------------------------------------
-- ⊥, ⊤, _×_ and _⊎_ form a commutative semiring

-- ⊤, _×_ form a commutative monoid

×-isMagma :  k   IsMagma {Level.suc } (Related  k ) _×_
×-isMagma k  = record
  { isEquivalence = SK-isEquivalence k 
  ; ∙-cong        = _×-cong_
  }

×-magma : Symmetric-kind  ( : Level)  Magma _ _
×-magma k  = record
  { isMagma = ×-isMagma k 
  }

×-isSemigroup :  k   IsSemigroup {Level.suc } (Related  k ) _×_
×-isSemigroup k  = record
  { isMagma = ×-isMagma k 
  ; assoc   = λ _ _ _  ↔⇒ Σ-assoc
  }

×-semigroup : Symmetric-kind  ( : Level)  Semigroup _ _
×-semigroup k  = record
  { isSemigroup = ×-isSemigroup k 
  }

×-isMonoid :  k   IsMonoid (Related  k ) _×_ 
×-isMonoid k  = record
  { isSemigroup = ×-isSemigroup k 
  ; identity    = (↔⇒  ×-identityˡ ) , (↔⇒  ×-identityʳ )
  }

×-monoid : Symmetric-kind  ( : Level)  Monoid _ _
×-monoid k  = record
  { isMonoid = ×-isMonoid k 
  }

×-isCommutativeMonoid :  k   IsCommutativeMonoid (Related  k ) _×_ 
×-isCommutativeMonoid k  = record
  { isMonoid = ×-isMonoid k 
  ; comm     = λ _ _  ↔⇒ (×-comm _ _)
  }

×-commutativeMonoid : Symmetric-kind  ( : Level)  CommutativeMonoid _ _
×-commutativeMonoid k  = record
  { isCommutativeMonoid = ×-isCommutativeMonoid k 
  }

-- ⊥, _⊎_ form a commutative monoid

⊎-isMagma :  k   IsMagma {Level.suc } (Related  k ) _⊎_
⊎-isMagma k  = record
  { isEquivalence = SK-isEquivalence k 
  ; ∙-cong        = _⊎-cong_
  }

⊎-magma : Symmetric-kind  ( : Level)  Magma _ _
⊎-magma k  = record
  { isMagma = ⊎-isMagma k 
  }

⊎-isSemigroup :  k   IsSemigroup {Level.suc } (Related  k ) _⊎_
⊎-isSemigroup k  = record
  { isMagma = ⊎-isMagma k 
  ; assoc   = λ A B C  ↔⇒ (⊎-assoc  A B C)
  }

⊎-semigroup : Symmetric-kind  ( : Level)  Semigroup _ _
⊎-semigroup k  = record
  { isSemigroup = ⊎-isSemigroup k 
  }

⊎-isMonoid :  k   IsMonoid (Related  k ) _⊎_ 
⊎-isMonoid k  = record
  { isSemigroup = ⊎-isSemigroup k 
  ; identity    = (↔⇒  ⊎-identityˡ ) , (↔⇒  ⊎-identityʳ )
  }

⊎-monoid : Symmetric-kind  ( : Level)  Monoid _ _
⊎-monoid k  = record
  { isMonoid = ⊎-isMonoid k 
  }

⊎-isCommutativeMonoid :  k   IsCommutativeMonoid (Related  k ) _⊎_ 
⊎-isCommutativeMonoid k  = record
  { isMonoid = ⊎-isMonoid k 
  ; comm     = λ _ _  ↔⇒ (⊎-comm _ _)
  }

⊎-commutativeMonoid : Symmetric-kind  ( : Level) 
                      CommutativeMonoid _ _
⊎-commutativeMonoid k  = record
  { isCommutativeMonoid = ⊎-isCommutativeMonoid k 
  }

×-⊎-isCommutativeSemiring :  k  
  IsCommutativeSemiring (Related  k ) _⊎_ _×_  
×-⊎-isCommutativeSemiring k  = isCommutativeSemiringˡ record
  { +-isCommutativeMonoid = ⊎-isCommutativeMonoid k 
  ; *-isCommutativeMonoid = ×-isCommutativeMonoid k 
  ; distribʳ              = λ A B C  ↔⇒ (×-distribʳ-⊎  A B C)
  ; zeroˡ                 = ↔⇒  ×-zeroˡ 
  }

×-⊎-commutativeSemiring : Symmetric-kind  ( : Level) 
                          CommutativeSemiring (Level.suc ) 
×-⊎-commutativeSemiring k  = record
  { isCommutativeSemiring = ×-⊎-isCommutativeSemiring k 
  }

------------------------------------------------------------------------
-- Some reordering lemmas

ΠΠ↔ΠΠ :  {a b p} {A : Set a} {B : Set b} (P : A  B  Set p) 
        ((x : A) (y : B)  P x y)  ((y : B) (x : A)  P x y)
ΠΠ↔ΠΠ _ = inverse flip flip  _  P.refl)  _  P.refl)

∃∃↔∃∃ :  {a b p} {A : Set a} {B : Set b} (P : A  B  Set p) 
        (∃₂ λ x y  P x y)  (∃₂ λ y x  P x y)
∃∃↔∃∃ P = inverse to from  _  P.refl)  _  P.refl)
  where
  to : (∃₂ λ x y  P x y)  (∃₂ λ y x  P x y)
  to (x , y , Pxy) = (y , x , Pxy)

  from : (∃₂ λ y x  P x y)  (∃₂ λ x y  P x y)
  from (y , x , Pxy) = (x , y , Pxy)

------------------------------------------------------------------------
-- Implicit and explicit function spaces are isomorphic

Π↔Π :  {a b} {A : Set a} {B : A  Set b} 
      ((x : A)  B x)  ({x : A}  B x)
Π↔Π = inverse  f {x}  f x)  f x  f)  _  P.refl)  _  P.refl)

------------------------------------------------------------------------
-- _→_ preserves the symmetric relations

_→-cong-⇔_ :
   {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
  A  B  C  D  (A  C)  (B  D)
A⇔B →-cong-⇔ C⇔D = Eq.equivalence
   f x  Equivalence.to   C⇔D ⟨$⟩ f (Equivalence.from A⇔B ⟨$⟩ x))
   f x  Equivalence.from C⇔D ⟨$⟩ f (Equivalence.to   A⇔B ⟨$⟩ x))

→-cong :
   {a b c d} 
  Extensionality a c  Extensionality b d 
   {k} {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
  A ∼[  k  ] B  C ∼[  k  ] D  (A  C) ∼[  k  ] (B  D)
→-cong extAC extBD {equivalence} A⇔B C⇔D = A⇔B →-cong-⇔ C⇔D
→-cong extAC extBD {bijection}   A↔B C↔D = record
  { to         = Equivalence.to   A→C⇔B→D
  ; from       = Equivalence.from A→C⇔B→D
  ; inverse-of = record
    { left-inverse-of  = λ f  extAC λ x  begin
        Inverse.from C↔D ⟨$⟩ (Inverse.to C↔D ⟨$⟩
          f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x)))  ≡⟨ Inverse.left-inverse-of C↔D _ 
        f (Inverse.from A↔B ⟨$⟩ (Inverse.to A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.left-inverse-of A↔B x 
        f x                                                 
    ; right-inverse-of = λ f  extBD λ x  begin
        Inverse.to C↔D ⟨$⟩ (Inverse.from C↔D ⟨$⟩
          f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x)))  ≡⟨ Inverse.right-inverse-of C↔D _ 
        f (Inverse.to A↔B ⟨$⟩ (Inverse.from A↔B ⟨$⟩ x))     ≡⟨ P.cong f $ Inverse.right-inverse-of A↔B x 
        f x                                                 
    }
  }
  where
  open P.≡-Reasoning
  A→C⇔B→D = ↔⇒ A↔B →-cong-⇔ ↔⇒ C↔D

------------------------------------------------------------------------
-- ¬_ (at Level 0) preserves the symmetric relations

¬-cong-⇔ :  {a b} {A : Set a} {B : Set b} 
           A  B  (¬ A)  (¬ B)
¬-cong-⇔ A⇔B =  A⇔B →-cong-⇔ Eq.id

¬-cong :  {a b}  Extensionality a 0ℓ  Extensionality b 0ℓ 
          {k} {A : Set a} {B : Set b} 
         A ∼[  k  ] B  (¬ A) ∼[  k  ] (¬ B)
¬-cong extA extB A≈B = →-cong extA extB A≈B (K-reflexive P.refl)

------------------------------------------------------------------------
-- _⇔_ preserves _⇔_

-- The type of the following proof is a bit more general.

Related-cong :
   {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} 
  A ∼[  k  ] B  C ∼[  k  ] D  (A ∼[  k  ] C)  (B ∼[  k  ] D)
Related-cong {A = A} {B} {C} {D} A≈B C≈D =
  Eq.equivalence  A≈C  B  ∼⟨ SK-sym A≈B 
                          A  ∼⟨ A≈C 
                          C  ∼⟨ C≈D 
                          D  )
                  B≈D  A  ∼⟨ A≈B 
                          B  ∼⟨ B≈D 
                          D  ∼⟨ SK-sym C≈D 
                          C  )
  where open EquationalReasoning

------------------------------------------------------------------------
-- A lemma relating True dec and P, where dec : Dec P

True↔ :  {p} {P : Set p}
        (dec : Dec P)  ((p₁ p₂ : P)  p₁  p₂)  True dec  P
True↔ ( true because  [p]) irr =
  inverse  _  invert [p])  _  _)  _  P.refl) (irr _)
True↔ (false because ofⁿ ¬p) _ =
  inverse (λ()) (invert (ofⁿ ¬p))  ()) (⊥-elim  ¬p)

------------------------------------------------------------------------
-- Equality between pairs can be expressed as a pair of equalities

module _ {a b} {A : Set a} {B : A  Set b} {p₁ p₂ : Σ A B} where
  Σ-≡,≡→≡ : Σ (proj₁ p₁  proj₁ p₂)
               p  P.subst B p (proj₂ p₁)  proj₂ p₂) 
            p₁  p₂
  Σ-≡,≡→≡ (P.refl , P.refl) = P.refl

  Σ-≡,≡←≡ : p₁  p₂ 
            Σ (proj₁ p₁  proj₁ p₂)
               p  P.subst B p (proj₂ p₁)  proj₂ p₂)
  Σ-≡,≡←≡ P.refl = P.refl , P.refl

  private

    left-inverse-of : (p : Σ (proj₁ p₁  proj₁ p₂)
                              x  P.subst B x (proj₂ p₁)  proj₂ p₂)) 
                      Σ-≡,≡←≡ (Σ-≡,≡→≡ p)  p
    left-inverse-of (P.refl , P.refl) = P.refl

    right-inverse-of : (p : p₁  p₂)  Σ-≡,≡→≡ (Σ-≡,≡←≡ p)  p
    right-inverse-of P.refl = P.refl

  Σ-≡,≡↔≡ : ( λ (p : proj₁ p₁  proj₁ p₂) 
               P.subst B p (proj₂ p₁)  proj₂ p₂) 
            p₁  p₂
  Σ-≡,≡↔≡ = inverse Σ-≡,≡→≡ Σ-≡,≡←≡ left-inverse-of right-inverse-of

module _ {a b} {A : Set a} {B : Set b} {p₁ p₂ : A × B} where
  ×-≡,≡→≡ : (proj₁ p₁  proj₁ p₂) × (proj₂ p₁  proj₂ p₂)  p₁  p₂
  ×-≡,≡→≡ (P.refl , P.refl) = P.refl

  ×-≡,≡←≡ : p₁  p₂ 
            (proj₁ p₁  proj₁ p₂) × (proj₂ p₁  proj₂ p₂)
  ×-≡,≡←≡ P.refl = P.refl , P.refl

  private
    left-inverse-of : (p : (proj₁ p₁  proj₁ p₂) × (proj₂ p₁  proj₂ p₂)) 
                      ×-≡,≡←≡ (×-≡,≡→≡ p)  p
    left-inverse-of (P.refl , P.refl) = P.refl

    right-inverse-of : (p : p₁  p₂)  ×-≡,≡→≡ (×-≡,≡←≡ p)  p
    right-inverse-of P.refl = P.refl

  ×-≡,≡↔≡ : (proj₁ p₁  proj₁ p₂ × proj₂ p₁  proj₂ p₂)  p₁  p₂
  ×-≡,≡↔≡ = inverse ×-≡,≡→≡ ×-≡,≡←≡ left-inverse-of right-inverse-of

×-≡×≡↔≡,≡ :  {a b} {A : Set a} {B : Set b} {x y} (p : A × B) 
            (x  proj₁ p × y  proj₂ p)  (x , y)  p
×-≡×≡↔≡,≡ _ = ×-≡,≡↔≡