------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of inverses.
------------------------------------------------------------------------

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

module Function.Properties.Inverse where

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Function.Bundles
import Function.Properties.RightInverse as RightInverse
open import Level using (Level; _⊔_)
open import Relation.Binary.Core using (REL)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as P
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
import Function.Consequences.Setoid as Consequences

import Function.Construct.Identity as Identity
import Function.Construct.Symmetry as Symmetry
import Function.Construct.Composition as Composition

private
  variable
    a b  ℓ₁ ℓ₂ : Level
    A B C D : Set a
    S T U V : Setoid a 

------------------------------------------------------------------------
-- Setoid bundles

open Identity    public using () renaming (inverse to refl)
open Symmetry    public using () renaming (inverse to sym)
open Composition public using () renaming (inverse to trans)

isEquivalence : IsEquivalence (Inverse {a} {b})
isEquivalence = record
  { refl  = λ {x}  Identity.inverse x
  ; sym   = sym
  ; trans = trans
  }

------------------------------------------------------------------------
-- Propositional bundles

↔-refl : A  A
↔-refl = Identity.↔-id _

↔-sym : A  B  B  A
↔-sym = Symmetry.↔-sym

↔-trans : A  B  B  C  A  C
↔-trans = Composition.inverse

-- need to η-expand for everything to line up properly
↔-isEquivalence : IsEquivalence { = } _↔_
↔-isEquivalence = record
  { refl  = ↔-refl
  ; sym   = ↔-sym
  ; trans = ↔-trans
  }

------------------------------------------------------------------------
-- Conversion functions

toFunction : Inverse S T  Func S T
toFunction I = record { to = to ; cong = to-cong }
  where open Inverse I

fromFunction : Inverse S T  Func T S
fromFunction I = record { to = from ; cong = from-cong }
  where open Inverse I

Inverse⇒Injection : Inverse S T  Injection S T
Inverse⇒Injection {S = S} {T = T} I = record
  { to = to
  ; cong = to-cong
  ; injective = inverseʳ⇒injective to inverseʳ
  } where open Inverse I; open Consequences S T

Inverse⇒Surjection : Inverse S T  Surjection S T
Inverse⇒Surjection {S = S} {T = T} I = record
  { to = to
  ; cong = to-cong
  ; surjective = inverseˡ⇒surjective inverseˡ
  } where open Inverse I; open Consequences S T

Inverse⇒Bijection : Inverse S T  Bijection S T
Inverse⇒Bijection {S = S} {T = T} I = record
  { to        = to
  ; cong      = to-cong
  ; bijective = inverseᵇ⇒bijective inverse
  } where open Inverse I; open Consequences S T

Inverse⇒Equivalence : Inverse S T  Equivalence S T
Inverse⇒Equivalence I = record
  { to        = to
  ; from      = from
  ; to-cong   = to-cong
  ; from-cong = from-cong
  } where open Inverse I

↔⇒⟶ : A  B  A  B
↔⇒⟶ = toFunction

↔⇒⟵ : A  B  B  A
↔⇒⟵ = fromFunction

↔⇒↣ : A  B  A  B
↔⇒↣ = Inverse⇒Injection

↔⇒↠ : A  B  A  B
↔⇒↠ = Inverse⇒Surjection

↔⇒⤖ : A  B  A  B
↔⇒⤖ = Inverse⇒Bijection

↔⇒⇔ : A  B  A  B
↔⇒⇔ = Inverse⇒Equivalence

↔⇒↩ : A  B  A  B
↔⇒↩ = Inverse.leftInverse

↔⇒↪ : A  B  A  B
↔⇒↪ = Inverse.rightInverse

-- The functions above can be combined with the following lemma to
-- transport an arbitrary relation R (e.g. Injection) across
-- inverses.
transportVia : {R :  {a b ℓ₁ ℓ₂}  REL (Setoid a ℓ₁) (Setoid b ℓ₂) (a  b  ℓ₁  ℓ₂)} 
               (∀ {a b c ℓ₁ ℓ₂ ℓ₃} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} {U : Setoid c ℓ₃}  R S T  R T U  R S U) 
               (∀ {a b ℓ₁ ℓ₂} {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}  Inverse S T  R S T) 
               Inverse S T  R T U  Inverse U V  R S V
transportVia R-trans inv⇒R IBA RBC ICD =
  R-trans (inv⇒R IBA) (R-trans RBC (inv⇒R ICD))

------------------------------------------------------------------------
-- Other

module _ (ext :  {a b}  Extensionality a b) where

  ↔-fun : A  B  C  D  (A  C)  (B  D)
  ↔-fun A↔B C↔D = mk↔ₛ′
     a→c b  to C↔D (a→c (from A↔B b)))
     b→d a  from C↔D (b→d (to A↔B a)))
     b→d  ext λ _  P.trans (strictlyInverseˡ C↔D _ ) (P.cong b→d (strictlyInverseˡ A↔B _)))
     a→c  ext λ _  P.trans (strictlyInverseʳ C↔D _ ) (P.cong a→c (strictlyInverseʳ A↔B _)))
    where open Inverse

module _ (I : Inverse S T) where
  open Inverse I

  to-from :  {x y}  to x Eq₂.≈ y  from y Eq₁.≈ x
  to-from = RightInverse.to-from rightInverse