------------------------------------------------------------------------
-- The Agda standard library
--
-- Dependent product combinators for setoid equality preserving
-- functions.
--
-- NOTE: the first component of the equality is propositional equality.
------------------------------------------------------------------------

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

module Data.Product.Function.Dependent.Setoid where

open import Data.Product.Base using (map; _,_; proj₁; proj₂)
open import Data.Product.Relation.Binary.Pointwise.Dependent as Σ
open import Level using (Level)
open import Function
open import Function.Consequences.Setoid
open import Function.Properties.Injection using (mkInjection)
open import Function.Properties.Surjection using (mkSurjection; ↠⇒⇔)
open import Function.Properties.Equivalence using (mkEquivalence; ⇔⇒⟶; ⇔⇒⟵)
open import Function.Properties.RightInverse using (mkRightInverse)
open import Relation.Binary.Core using (_=[_]⇒_)
open import Relation.Binary.Bundles as B
open import Relation.Binary.Indexed.Heterogeneous
  using (IndexedSetoid)
open import Relation.Binary.Indexed.Heterogeneous.Construct.At
  using (_atₛ_)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
import Relation.Binary.PropositionalEquality.Properties as ≡

private
  variable
    i a b ℓ₁ ℓ₂ : Level
    I J : Set i
    A B : IndexedSetoid I a ℓ₁

------------------------------------------------------------------------
-- Properties related to "relatedness"
------------------------------------------------------------------------

private module _ (A : IndexedSetoid I a ℓ₁) where
  open IndexedSetoid A

  cast : ∀ {i j} → j ≡ i → Carrier i → Carrier j
  cast j≡i = ≡.subst Carrier (≡.sym $ j≡i)

  cast-cong : ∀ {i j} {x y : Carrier i}
               (j≡i : j ≡ i) →
               x ≈ y →
               cast j≡i x ≈ cast j≡i y
  cast-cong ≡.refl p = p

  cast-eq : ∀ {i j x} (eq : i ≡ j) → cast eq x ≈ x
  cast-eq ≡.refl = IndexedSetoid.refl A

private
  _×ₛ_ : (I : Set i) → IndexedSetoid I a ℓ₁ → Setoid _ _
  I ×ₛ A = Σ.setoid (≡.setoid I) A

------------------------------------------------------------------------
-- Functions

module _ where
  open Func
  open Setoid

  function :
    (f : I ⟶ J) →
    (∀ {i} → Func (A atₛ i) (B atₛ (to f i))) →
    Func (I ×ₛ A) (J ×ₛ B)
  function {I = I} {J = J} {A = A} {B = B} I⟶J A⟶B = record
    { to    = to′
    ; cong  = cong′
    }
    where
    to′ = map (to I⟶J) (to A⟶B)

    cong′ : Congruent (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′
    cong′ (≡.refl , ∼) = (≡.refl , cong A⟶B ∼)

------------------------------------------------------------------------
-- Equivalences

module _ where
  open Equivalence

  equivalence :
    (I⇔J : I ⇔ J) →
    (∀ {i} → Func (A atₛ i) (B atₛ (to   I⇔J i))) →
    (∀ {j} → Func (B atₛ j) (A atₛ (from I⇔J j))) →
    Equivalence (I ×ₛ A) (J ×ₛ B)
  equivalence I⇔J A⟶B B⟶A = mkEquivalence
    (function (⇔⇒⟶ I⇔J) A⟶B)
    (function (⇔⇒⟵ I⇔J) B⟶A)

  equivalence-↪ :
    (I↪J : I ↪ J) →
    (∀ {i} → Equivalence (A atₛ (RightInverse.from I↪J i)) (B atₛ i)) →
    Equivalence (I ×ₛ A) (J ×ₛ B)
  equivalence-↪ {A = A} {B = B} I↪J A⇔B =
    equivalence (RightInverse.equivalence I↪J) A→B (fromFunction A⇔B)
    where
    A→B : ∀ {i} → Func (A atₛ i) (B atₛ (RightInverse.to I↪J i))
    A→B = record
      { to   = to      A⇔B ∘ cast      A (RightInverse.strictlyInverseʳ I↪J _)
      ; cong = to-cong A⇔B ∘ cast-cong A (RightInverse.strictlyInverseʳ I↪J _)
      }

  equivalence-↠ :
    (I↠J : I ↠ J) →
    (∀ {x} → Equivalence (A atₛ x) (B atₛ (Surjection.to I↠J x))) →
    Equivalence (I ×ₛ A) (J ×ₛ B)
  equivalence-↠ {A = A} {B = B} I↠J A⇔B =
    equivalence (↠⇒⇔ I↠J) B-to B-from
    where
    B-to : ∀ {x} → Func (A atₛ x) (B atₛ (Surjection.to I↠J x))
    B-to = toFunction A⇔B

    B-from : ∀ {y} → Func (B atₛ y) (A atₛ (Surjection.to⁻ I↠J y))
    B-from = record
      { to   = from      A⇔B ∘ cast      B (Surjection.to∘to⁻ I↠J _)
      ; cong = from-cong A⇔B ∘ cast-cong B (Surjection.to∘to⁻ I↠J _)
      }

------------------------------------------------------------------------
-- Injections

module _ where
  open Injection hiding (function)
  open IndexedSetoid

  injection :
    (I↣J : I ↣ J) →
    (∀ {i} → Injection (A atₛ i) (B atₛ (Injection.to I↣J i))) →
    Injection (I ×ₛ A) (J ×ₛ B)
  injection {I = I} {J = J} {A = A} {B = B} I↣J A↣B = mkInjection func inj
    where
    func : Func (I ×ₛ A) (J ×ₛ B)
    func = function (Injection.function I↣J) (Injection.function A↣B)

    inj : Injective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
    inj (to[i]≡to[j] , y) =
      injective I↣J to[i]≡to[j] ,
      lemma (injective I↣J to[i]≡to[j]) y
      where
      lemma :
        ∀ {i j} {x : Carrier A i} {y : Carrier A j} →
          i ≡ j →
          (_≈_ B (to A↣B x) (to A↣B y)) →
          _≈_ A x y
      lemma ≡.refl = Injection.injective A↣B

------------------------------------------------------------------------
-- Surjections

module _ where
  open Surjection hiding (function)
  open Setoid

  surjection :
    (I↠J : I ↠ J) →
    (∀ {x} → Surjection (A atₛ x) (B atₛ (to I↠J x))) →
    Surjection (I ×ₛ A) (J ×ₛ B)
  surjection {I = I} {J = J} {A = A} {B = B} I↠J A↠B =
    mkSurjection func surj
    where
    func : Func (I ×ₛ A) (J ×ₛ B)
    func = function (Surjection.function I↠J) (Surjection.function A↠B)

    to⁻′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
    to⁻′ (j , y) = to⁻ I↠J j , to⁻ A↠B (cast B (Surjection.to∘to⁻ I↠J _) y)

    strictlySurj : StrictlySurjective (Func.Eq₂._≈_ func) (Func.to func)
    strictlySurj (j , y) = to⁻′ (j , y) ,
      to∘to⁻ I↠J j , IndexedSetoid.trans B (to∘to⁻ A↠B _) (cast-eq B (to∘to⁻ I↠J j))

    surj : Surjective (Func.Eq₁._≈_ func) (Func.Eq₂._≈_ func) (Func.to func)
    surj = strictlySurjective⇒surjective (I ×ₛ A) (J ×ₛ B) (Func.cong func) strictlySurj

------------------------------------------------------------------------
-- LeftInverse

module _ where
  open RightInverse
  open Setoid

  left-inverse :
    (I↪J : I ↪ J) →
    (∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
    RightInverse (I ×ₛ A) (J ×ₛ B)
  left-inverse {I = I} {J = J} {A = A} {B = B} I↪J A↪B =
    mkRightInverse equiv invʳ
    where
    equiv : Equivalence (I ×ₛ A) (J ×ₛ B)
    equiv = equivalence-↪ I↪J (RightInverse.equivalence A↪B)

    strictlyInvʳ : StrictlyInverseʳ (_≈_ (I ×ₛ A)) (Equivalence.to equiv) (Equivalence.from equiv)
    strictlyInvʳ (i , x) = strictlyInverseʳ I↪J i , IndexedSetoid.trans A (strictlyInverseʳ A↪B _) (cast-eq A (strictlyInverseʳ I↪J i))

    invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) (Equivalence.to equiv) (Equivalence.from equiv)
    invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) (Equivalence.from-cong equiv) strictlyInvʳ


------------------------------------------------------------------------
-- Inverses

module _ where
  open Inverse hiding (inverse)
  open Setoid

  inverse : (I↔J : I ↔ J) →
            (∀ {i} → Inverse (A atₛ i) (B atₛ (to I↔J i))) →
            Inverse (I ×ₛ A) (J ×ₛ B)
  inverse {I = I} {J = J} {A = A} {B = B} I↔J A↔B = record
    { to = to′
    ; from = from′
    ; to-cong = to′-cong
    ; from-cong = from′-cong
    ; inverse = invˡ , invʳ
    }
    where
    to′ : Carrier (I ×ₛ A) → Carrier (J ×ₛ B)
    to′ (i , x) = to I↔J i , to A↔B x

    to′-cong : Congruent (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′
    to′-cong (≡.refl , x≈y) = to-cong I↔J ≡.refl , to-cong A↔B x≈y

    from′ : Carrier (J ×ₛ B) → Carrier (I ×ₛ A)
    from′ (j , y) = from I↔J j , from A↔B (cast B (strictlyInverseˡ I↔J _) y)

    from′-cong : Congruent (_≈_ (J ×ₛ B)) (_≈_ (I ×ₛ A)) from′
    from′-cong (≡.refl , x≈y) = from-cong I↔J ≡.refl , from-cong A↔B (cast-cong B (strictlyInverseˡ I↔J _) x≈y)

    strictlyInvˡ : StrictlyInverseˡ (_≈_ (J ×ₛ B)) to′ from′
    strictlyInvˡ (i , x) = strictlyInverseˡ I↔J i ,
        IndexedSetoid.trans B (strictlyInverseˡ A↔B _)
          (cast-eq B (strictlyInverseˡ I↔J i))

    invˡ : Inverseˡ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′ from′
    invˡ = strictlyInverseˡ⇒inverseˡ (I ×ₛ A) (J ×ₛ B) to′-cong strictlyInvˡ

    lem : ∀ {i j} → i ≡ j → ∀ {x : IndexedSetoid.Carrier B (to I↔J i)} {y : IndexedSetoid.Carrier B (to I↔J j)} →
          IndexedSetoid._≈_ B x y →
          IndexedSetoid._≈_ A (from A↔B x) (from A↔B y)
    lem ≡.refl x≈y = from-cong A↔B x≈y

    strictlyInvʳ : StrictlyInverseʳ (_≈_ (I ×ₛ A)) to′ from′
    strictlyInvʳ (i , x) = strictlyInverseʳ I↔J i ,
      IndexedSetoid.trans A (lem (strictlyInverseʳ I↔J _) (cast-eq B (strictlyInverseˡ I↔J _))) (strictlyInverseʳ A↔B _)

    invʳ : Inverseʳ (_≈_ (I ×ₛ A)) (_≈_ (J ×ₛ B)) to′ from′
    invʳ = strictlyInverseʳ⇒inverseʳ (I ×ₛ A) (J ×ₛ B) from′-cong strictlyInvʳ