{-# OPTIONS --without-K --safe #-}
module Data.Product.Function.Dependent.Propositional where
open import Data.Product
open import Data.Product.Function.NonDependent.Setoid
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Relation.Binary hiding (_⇔_)
open import Function.Base
open import Function.Equality using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Equiv using (_⇔_; module Equivalence)
open import Function.HalfAdjointEquivalence using (↔→≃; _≃_)
open import Function.Injection as Inj
using (Injective; _↣_; module Injection)
open import Function.Inverse as Inv using (_↔_; module Inverse)
open import Function.LeftInverse as LeftInv
using (_↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Related.TypeIsomorphisms
open import Function.Surjection as Surj using (_↠_; module Surjection)
open import Relation.Binary.PropositionalEquality as P using (_≡_)
module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
{b₁ b₂} {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
where
⇔ : (A₁⇔A₂ : A₁ ⇔ A₂) →
(∀ {x} → B₁ x → B₂ (Equivalence.to A₁⇔A₂ ⟨$⟩ x)) →
(∀ {y} → B₂ y → B₁ (Equivalence.from A₁⇔A₂ ⟨$⟩ y)) →
Σ A₁ B₁ ⇔ Σ A₂ B₂
⇔ A₁⇔A₂ B-to B-from = Equiv.equivalence
(map (Equivalence.to A₁⇔A₂ ⟨$⟩_) B-to)
(map (Equivalence.from A₁⇔A₂ ⟨$⟩_) B-from)
⇔-↠ : ∀ (A₁↠A₂ : A₁ ↠ A₂) →
(∀ {x} → _⇔_ (B₁ x) (B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x))) →
_⇔_ (Σ A₁ B₁) (Σ A₂ B₂)
⇔-↠ A₁↠A₂ B₁⇔B₂ = Equiv.equivalence
(map (Surjection.to A₁↠A₂ ⟨$⟩_) (Equivalence.to B₁⇔B₂ ⟨$⟩_))
(map (Surjection.from A₁↠A₂ ⟨$⟩_)
((Equivalence.from B₁⇔B₂ ⟨$⟩_) ∘
P.subst B₂ (P.sym $ Surjection.right-inverse-of A₁↠A₂ _)))
↣ : ∀ (A₁↔A₂ : A₁ ↔ A₂) →
(∀ {x} → B₁ x ↣ B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
Σ A₁ B₁ ↣ Σ A₂ B₂
↣ A₁↔A₂ B₁↣B₂ = Inj.injection to to-injective
where
open P.≡-Reasoning
A₁≃A₂ = ↔→≃ A₁↔A₂
subst-application′ :
let open _≃_ A₁≃A₂ in
{x₁ x₂ : A₁} {y : B₁ (from (to x₁))}
(g : ∀ x → B₁ (from (to x)) → B₂ (to x)) (eq : to x₁ ≡ to x₂) →
P.subst B₂ eq (g x₁ y) ≡ g x₂ (P.subst B₁ (P.cong from eq) y)
subst-application′ {x₁} {x₂} {y} g eq =
P.subst B₂ eq (g x₁ y) ≡⟨ P.cong (P.subst B₂ eq) (P.sym (g′-lemma _ _)) ⟩
P.subst B₂ eq (g′ (to x₁) y) ≡⟨ P.subst-application B₁ g′ eq ⟩
g′ (to x₂) (P.subst B₁ (P.cong from eq) y) ≡⟨ g′-lemma _ _ ⟩
g x₂ (P.subst B₁ (P.cong from eq) y) ∎
where
open _≃_ A₁≃A₂
g′ : ∀ x → B₁ (from x) → B₂ x
g′ x =
P.subst B₂ (right-inverse-of x) ∘
g (from x) ∘
P.subst B₁ (P.sym (P.cong from (right-inverse-of x)))
g′-lemma : ∀ x y → g′ (to x) y ≡ g x y
g′-lemma x y =
P.subst B₂ (right-inverse-of (to x))
(g (from (to x)) $
P.subst B₁ (P.sym (P.cong from (right-inverse-of (to x)))) y) ≡⟨ P.cong (λ p → P.subst B₂ p (g (from (to x))
(P.subst B₁ (P.sym (P.cong from p)) y)))
(P.sym (left-right x)) ⟩
P.subst B₂ (P.cong to (left-inverse-of x))
(g (from (to x)) $
P.subst B₁
(P.sym (P.cong from (P.cong to (left-inverse-of x))))
y) ≡⟨ lemma _ ⟩
g x y ∎
where
lemma :
∀ {x′} eq {y : B₁ (from (to x′))} →
P.subst B₂ (P.cong to eq)
(g (from (to x))
(P.subst B₁ (P.sym (P.cong from (P.cong to eq))) y)) ≡
g x′ y
lemma P.refl = P.refl
to = map (_≃_.to A₁≃A₂) (Injection.to B₁↣B₂ ⟨$⟩_)
to-injective : Injective (P.→-to-⟶ {B = P.setoid _} to)
to-injective {(x₁ , x₂)} {(y₁ , y₂)} =
Σ-≡,≡→≡ ∘′
map (_≃_.injective A₁≃A₂) (λ {eq₁} eq₂ →
let lemma =
Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂ ≡⟨⟩
Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁
(P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
(P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
(P.trans (_≃_.left-inverse-of A₁≃A₂ y₁)
P.refl)))
x₂ ≡⟨ P.cong (λ p → Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁
(P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ _))
(P.trans (P.cong (_≃_.from A₁≃A₂) eq₁) p))
x₂)
(P.trans-reflʳ _) ⟩
Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁
(P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
(P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
(_≃_.left-inverse-of A₁≃A₂ y₁)))
x₂ ≡⟨ P.cong (Injection.to B₁↣B₂ ⟨$⟩_)
(P.sym (P.subst-subst (P.sym (_≃_.left-inverse-of A₁≃A₂ _)))) ⟩
Injection.to B₁↣B₂ ⟨$⟩
(P.subst B₁ (P.trans (P.cong (_≃_.from A₁≃A₂) eq₁)
(_≃_.left-inverse-of A₁≃A₂ y₁)) $
P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂) ≡⟨ P.cong (Injection.to B₁↣B₂ ⟨$⟩_)
(P.sym (P.subst-subst (P.cong (_≃_.from A₁≃A₂) eq₁))) ⟩
Injection.to B₁↣B₂ ⟨$⟩
(P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ y₁) $
P.subst B₁ (P.cong (_≃_.from A₁≃A₂) eq₁) $
P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂) ≡⟨ P.sym (subst-application′
(λ x y → Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x) y)
eq₁) ⟩
P.subst B₂ eq₁
(Injection.to B₁↣B₂ ⟨$⟩
(P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x₁) $
P.subst B₁ (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁)) x₂)) ≡⟨ P.cong (P.subst B₂ eq₁ ∘ (Injection.to B₁↣B₂ ⟨$⟩_))
(P.subst-subst (P.sym (_≃_.left-inverse-of A₁≃A₂ _))) ⟩
P.subst B₂ eq₁
(Injection.to B₁↣B₂ ⟨$⟩
P.subst B₁
(P.trans (P.sym (_≃_.left-inverse-of A₁≃A₂ x₁))
(_≃_.left-inverse-of A₁≃A₂ x₁))
x₂) ≡⟨ P.cong (λ p → P.subst B₂ eq₁
(Injection.to B₁↣B₂ ⟨$⟩ P.subst B₁ p x₂))
(P.trans-symˡ (_≃_.left-inverse-of A₁≃A₂ _)) ⟩
P.subst B₂ eq₁
(Injection.to B₁↣B₂ ⟨$⟩ P.subst B₁ P.refl x₂) ≡⟨⟩
P.subst B₂ eq₁ (Injection.to B₁↣B₂ ⟨$⟩ x₂) ≡⟨ eq₂ ⟩
Injection.to B₁↣B₂ ⟨$⟩ y₂ ∎
in
P.subst B₁ (_≃_.injective A₁≃A₂ eq₁) x₂ ≡⟨ Injection.injective B₁↣B₂ lemma ⟩
y₂ ∎) ∘
Σ-≡,≡←≡
↞ : (A₁↞A₂ : A₁ ↞ A₂) →
(∀ {x} → B₁ (LeftInverse.from A₁↞A₂ ⟨$⟩ x) ↞ B₂ x) →
Σ A₁ B₁ ↞ Σ A₂ B₂
↞ A₁↞A₂ B₁↞B₂ = record
{ to = P.→-to-⟶ to
; from = P.→-to-⟶ from
; left-inverse-of = left-inverse-of
}
where
open P.≡-Reasoning
from = map (LeftInverse.from A₁↞A₂ ⟨$⟩_) (LeftInverse.from B₁↞B₂ ⟨$⟩_)
to = map
(LeftInverse.to A₁↞A₂ ⟨$⟩_)
(λ {x} y →
LeftInverse.to B₁↞B₂ ⟨$⟩
P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x)) y)
left-inverse-of : ∀ p → from (to p) ≡ p
left-inverse-of (x , y) = Σ-≡,≡→≡
( LeftInverse.left-inverse-of A₁↞A₂ x
, (P.subst B₁ (LeftInverse.left-inverse-of A₁↞A₂ x)
(LeftInverse.from B₁↞B₂ ⟨$⟩ (LeftInverse.to B₁↞B₂ ⟨$⟩
(P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x))
y))) ≡⟨ P.cong (P.subst B₁ _) (LeftInverse.left-inverse-of B₁↞B₂ _) ⟩
P.subst B₁ (LeftInverse.left-inverse-of A₁↞A₂ x)
(P.subst B₁ (P.sym (LeftInverse.left-inverse-of A₁↞A₂ x))
y) ≡⟨ P.subst-subst-sym (LeftInverse.left-inverse-of A₁↞A₂ x) ⟩
y ∎)
)
↠ : (A₁↠A₂ : A₁ ↠ A₂) →
(∀ {x} → B₁ x ↠ B₂ (Surjection.to A₁↠A₂ ⟨$⟩ x)) →
Σ A₁ B₁ ↠ Σ A₂ B₂
↠ A₁↠A₂ B₁↠B₂ = record
{ to = P.→-to-⟶ to
; surjective = record
{ from = P.→-to-⟶ from
; right-inverse-of = right-inverse-of
}
}
where
open P.≡-Reasoning
to = map (Surjection.to A₁↠A₂ ⟨$⟩_)
(Surjection.to B₁↠B₂ ⟨$⟩_)
from = map
(Surjection.from A₁↠A₂ ⟨$⟩_)
(λ {x} y →
Surjection.from B₁↠B₂ ⟨$⟩
P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x)) y)
right-inverse-of : ∀ p → to (from p) ≡ p
right-inverse-of (x , y) = Σ-≡,≡→≡
( Surjection.right-inverse-of A₁↠A₂ x
, (P.subst B₂ (Surjection.right-inverse-of A₁↠A₂ x)
(Surjection.to B₁↠B₂ ⟨$⟩ (Surjection.from B₁↠B₂ ⟨$⟩
(P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x))
y))) ≡⟨ P.cong (P.subst B₂ _) (Surjection.right-inverse-of B₁↠B₂ _) ⟩
P.subst B₂ (Surjection.right-inverse-of A₁↠A₂ x)
(P.subst B₂ (P.sym (Surjection.right-inverse-of A₁↠A₂ x))
y) ≡⟨ P.subst-subst-sym (Surjection.right-inverse-of A₁↠A₂ x) ⟩
y ∎)
)
↔ : (A₁↔A₂ : A₁ ↔ A₂) →
(∀ {x} → B₁ x ↔ B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
Σ A₁ B₁ ↔ Σ A₂ B₂
↔ A₁↔A₂ B₁↔B₂ = Inv.inverse
(Surjection.to surjection′ ⟨$⟩_)
(Surjection.from surjection′ ⟨$⟩_)
left-inverse-of
(Surjection.right-inverse-of surjection′)
where
open P.≡-Reasoning
A₁≃A₂ = ↔→≃ A₁↔A₂
surjection′ : _↠_ (Σ A₁ B₁) (Σ A₂ B₂)
surjection′ =
↠ (Inverse.surjection (_≃_.inverse A₁≃A₂))
(Inverse.surjection B₁↔B₂)
left-inverse-of :
∀ p → Surjection.from surjection′ ⟨$⟩
(Surjection.to surjection′ ⟨$⟩ p) ≡ p
left-inverse-of (x , y) = Σ-≡,≡→≡
( _≃_.left-inverse-of A₁≃A₂ x
, (P.subst B₁ (_≃_.left-inverse-of A₁≃A₂ x)
(Inverse.from B₁↔B₂ ⟨$⟩
(P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
(_≃_.to A₁≃A₂ x)))
(Inverse.to B₁↔B₂ ⟨$⟩ y))) ≡⟨ P.subst-application B₂ (λ _ → Inverse.from B₁↔B₂ ⟨$⟩_) _ ⟩
Inverse.from B₁↔B₂ ⟨$⟩
(P.subst B₂ (P.cong (_≃_.to A₁≃A₂)
(_≃_.left-inverse-of A₁≃A₂ x))
(P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
(_≃_.to A₁≃A₂ x)))
(Inverse.to B₁↔B₂ ⟨$⟩ y))) ≡⟨ P.cong (λ eq → Inverse.from B₁↔B₂ ⟨$⟩ P.subst B₂ eq
(P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂ _)) _))
(_≃_.left-right A₁≃A₂ _) ⟩
Inverse.from B₁↔B₂ ⟨$⟩
(P.subst B₂ (_≃_.right-inverse-of A₁≃A₂
(_≃_.to A₁≃A₂ x))
(P.subst B₂ (P.sym (_≃_.right-inverse-of A₁≃A₂
(_≃_.to A₁≃A₂ x)))
(Inverse.to B₁↔B₂ ⟨$⟩ y))) ≡⟨ P.cong (Inverse.from B₁↔B₂ ⟨$⟩_)
(P.subst-subst-sym (_≃_.right-inverse-of A₁≃A₂ _)) ⟩
Inverse.from B₁↔B₂ ⟨$⟩ (Inverse.to B₁↔B₂ ⟨$⟩ y) ≡⟨ Inverse.left-inverse-of B₁↔B₂ _ ⟩
y ∎)
)
private
swap-coercions : ∀ {k a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
{B₁ : A₁ → Set b₁} (B₂ : A₂ → Set b₂)
(A₁↔A₂ : _↔_ A₁ A₂) →
(∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
∀ {x} → B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x) ∼[ k ] B₂ x
swap-coercions {k} {B₁ = B₁} B₂ A₁↔A₂ eq {x} =
B₁ (Inverse.from A₁↔A₂ ⟨$⟩ x)
∼⟨ eq ⟩
B₂ (Inverse.to A₁↔A₂ ⟨$⟩ (Inverse.from A₁↔A₂ ⟨$⟩ x))
↔⟨ K-reflexive
(P.cong B₂ $ Inverse.right-inverse-of A₁↔A₂ x) ⟩
B₂ x
∎
where open EquationalReasoning
cong : ∀ {k a₁ a₂ b₁ b₂}
{A₁ : Set a₁} {A₂ : Set a₂}
{B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
(A₁↔A₂ : _↔_ A₁ A₂) →
(∀ {x} → B₁ x ∼[ k ] B₂ (Inverse.to A₁↔A₂ ⟨$⟩ x)) →
Σ A₁ B₁ ∼[ k ] Σ A₂ B₂
cong {implication} =
λ A₁↔A₂ → map (_⟨$⟩_ (Inverse.to A₁↔A₂))
cong {reverse-implication} {B₂ = B₂} =
λ A₁↔A₂ B₁←B₂ → lam (map (_⟨$⟩_ (Inverse.from A₁↔A₂))
(app-← (swap-coercions B₂ A₁↔A₂ B₁←B₂)))
cong {equivalence} = ⇔-↠ ∘ Inverse.surjection
cong {injection} = ↣
cong {reverse-injection} {B₂ = B₂} =
λ A₁↔A₂ B₁↢B₂ → lam (↣ (Inv.sym A₁↔A₂)
(app-↢ (swap-coercions B₂ A₁↔A₂ B₁↢B₂)))
cong {left-inverse} =
λ A₁↔A₂ → ↞ (Inverse.left-inverse A₁↔A₂) ∘ swap-coercions _ A₁↔A₂
cong {surjection} = ↠ ∘ Inverse.surjection
cong {bijection} = ↔