------------------------------------------------------------------------
-- 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)
import Function.Construct.Symmetry as Sym
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
------------------------------------------------------------------------
-- RightInverse
module _ where
open RightInverse
open Setoid
rightInverse :
(I↪J : I ↪ J) →
(∀ {j} → RightInverse (A atₛ (from I↪J j)) (B atₛ j)) →
RightInverse (I ×ₛ A) (J ×ₛ B)
rightInverse {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ʳ
------------------------------------------------------------------------
-- LeftInverse
module _ where
open LeftInverse
open Setoid
leftInverse :
(I↩J : I ↩ J) →
(∀ {i} → LeftInverse (A atₛ i) (B atₛ (to I↩J i))) →
LeftInverse (I ×ₛ A) (J ×ₛ B)
leftInverse {I = I} {J = J} {A = A} {B = B} I↩J A↩B =
Sym.leftInverse (rightInverse (Sym.rightInverse I↩J) (Sym.rightInverse A↩B))
------------------------------------------------------------------------
-- 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ʳ
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.3
left-inverse = rightInverse
{-# WARNING_ON_USAGE left-inverse
"Warning: left-inverse was deprecated in v2.3.
Please use rightInverse or leftInverse instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4