------------------------------------------------------------------------
-- 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.Bundles public
using (Magma; Semigroup; Monoid; CommutativeMonoid; CommutativeSemiring)
open import Algebra.Definitions
using (Identity; LeftIdentity; RightIdentity; Zero; LeftZero; RightZero
; Associative; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
open import Algebra.Structures public
using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid
; IsCommutativeSemiring)
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.Polymorphic using (⊥; ⊥-elim)
open import Data.Product.Base as Product
using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃; ∃-syntax)
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.Base using (⊤)
open import Level using (Level; Lift; 0ℓ; suc)
open import Function.Base
open import Function.Bundles
open import Function.Related.Propositional
import Function.Construct.Identity as Identity
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)
open import Relation.Nullary.Negation.Core using (¬_)
import Relation.Nullary.Indexed as I
private
variable
a b c d : Level
A B C D : Set a
------------------------------------------------------------------------
-- A lemma relating True dec and P, where dec : Dec P
open import Relation.Nullary.Decidable public
using ()
renaming (True-↔ to True↔)
------------------------------------------------------------------------
-- Properties of Σ and _×_
-- Σ is associative
Σ-assoc : ∀ {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 = mk↔ₛ′ Product.assocʳ Product.assocˡ (λ _ → refl) (λ _ → refl)
-- × is commutative
×-comm : ∀ (A : Set a) (B : Set b) → (A × B) ↔ (B × A)
×-comm _ _ = mk↔ₛ′ Product.swap Product.swap (λ _ → refl) λ _ → refl
-- × has ⊤ as its identity
×-identityˡ : ∀ ℓ → LeftIdentity {ℓ = ℓ} _↔_ ⊤ _×_
×-identityˡ _ _ = mk↔ₛ′ proj₂ -,_ (λ _ → refl) (λ _ → refl)
×-identityʳ : ∀ ℓ → RightIdentity {ℓ = ℓ} _↔_ ⊤ _×_
×-identityʳ _ _ = mk↔ₛ′ proj₁ (_, _) (λ _ → refl) (λ _ → refl)
×-identity : ∀ ℓ → Identity _↔_ ⊤ _×_
×-identity ℓ = ×-identityˡ ℓ , ×-identityʳ ℓ
-- × has ⊥ has its zero
×-zeroˡ : ∀ ℓ → LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥-elim > (λ _ → refl) (λ { () })
×-zeroʳ : ∀ ℓ → RightZero {ℓ = ℓ} _↔_ ⊥ _×_
×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥-elim , id > (λ _ → refl) (λ { () })
×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_
×-zero ℓ = ×-zeroˡ ℓ , ×-zeroʳ ℓ
------------------------------------------------------------------------
-- Properties of ⊎
-- ⊎ is associative
⊎-assoc : ∀ ℓ → Associative {ℓ = ℓ} _↔_ _⊎_
⊎-assoc ℓ _ _ _ = mk↔ₛ′
[ [ inj₁ , inj₂ ∘′ inj₁ ]′ , inj₂ ∘′ inj₂ ]′
[ inj₁ ∘′ inj₁ , [ inj₁ ∘′ inj₂ , inj₂ ]′ ]′
[ (λ _ → refl) , [ (λ _ → refl) , (λ _ → refl) ] ]
[ [ (λ _ → refl) , (λ _ → refl) ] , (λ _ → refl) ]
-- ⊎ is commutative
⊎-comm : ∀ (A : Set a) (B : Set b) → (A ⊎ B) ↔ (B ⊎ A)
⊎-comm _ _ = mk↔ₛ′ swap swap swap-involutive swap-involutive
-- ⊎ has ⊥ as its identity
⊎-identityˡ : ∀ ℓ → LeftIdentity _↔_ (⊥ {ℓ}) _⊎_
⊎-identityˡ _ _ = mk↔ₛ′ [ (λ ()) , id ]′ inj₂ (λ _ → refl)
[ (λ ()) , (λ _ → refl) ]
⊎-identityʳ : ∀ ℓ → RightIdentity _↔_ (⊥ {ℓ}) _⊎_
⊎-identityʳ _ _ = mk↔ₛ′ [ id , (λ ()) ]′ inj₁ (λ _ → refl)
[ (λ _ → refl) , (λ ()) ]
⊎-identity : ∀ ℓ → Identity _↔_ ⊥ _⊎_
⊎-identity ℓ = ⊎-identityˡ ℓ , ⊎-identityʳ ℓ
------------------------------------------------------------------------
-- Properties of Σ and ⊎
-- Σ distributes over ⊎
Σ-distribˡ-⊎ : {P : A → Set a} {Q : A → Set b} →
(∃ λ a → P a ⊎ Q a) ↔ (∃ P ⊎ ∃ Q)
Σ-distribˡ-⊎ = mk↔ₛ′
(uncurry λ x → [ inj₁ ∘′ (x ,_) , inj₂ ∘′ (x ,_) ]′)
[ Product.map₂ inj₁ , Product.map₂ inj₂ ]′
[ (λ _ → refl) , (λ _ → refl) ]
(uncurry λ _ → [ (λ _ → refl) , (λ _ → refl) ])
Σ-distribʳ-⊎ : {P : A ⊎ B → Set c} →
(Σ (A ⊎ B) P) ↔ (Σ A (P ∘ inj₁) ⊎ Σ B (P ∘ inj₂))
Σ-distribʳ-⊎ = mk↔ₛ′
(uncurry [ curry inj₁ , curry inj₂ ])
[ Product.dmap inj₁ id , Product.dmap inj₂ id ]
[ (λ _ → refl) , (λ _ → refl) ]
(uncurry [ (λ _ _ → refl) , (λ _ _ → refl) ])
------------------------------------------------------------------------
-- Properties of × and ⊎
-- × distributes over ⊎
-- primed variants are less level polymorphic
×-distribˡ-⊎ : (A × (B ⊎ C)) ↔ (A × B ⊎ A × C)
×-distribˡ-⊎ = Σ-distribˡ-⊎
×-distribˡ-⊎′ : ∀ ℓ → _DistributesOverˡ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribˡ-⊎′ ℓ _ _ _ = ×-distribˡ-⊎
×-distribʳ-⊎ : ((A ⊎ B) × C) ↔ (A × C ⊎ B × C)
×-distribʳ-⊎ = Σ-distribʳ-⊎
×-distribʳ-⊎′ : ∀ ℓ → _DistributesOverʳ_ {ℓ = ℓ} _↔_ _×_ _⊎_
×-distribʳ-⊎′ ℓ _ _ _ = ×-distribʳ-⊎
×-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 : SymmetricKind → (ℓ : Level) → Magma _ _
×-magma k ℓ = record
{ isMagma = ×-isMagma k ℓ
}
×-isSemigroup : ∀ k ℓ → IsSemigroup {Level.suc ℓ} (Related ⌊ k ⌋) _×_
×-isSemigroup k ℓ = record
{ isMagma = ×-isMagma k ℓ
; assoc = λ _ _ _ → ↔⇒ Σ-assoc
}
×-semigroup : SymmetricKind → (ℓ : Level) → Semigroup _ _
×-semigroup k ℓ = record
{ isSemigroup = ×-isSemigroup k ℓ
}
×-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _×_ ⊤
×-isMonoid k ℓ = record
{ isSemigroup = ×-isSemigroup k ℓ
; identity = (↔⇒ ∘ ×-identityˡ ℓ) , (↔⇒ ∘ ×-identityʳ ℓ)
}
×-monoid : SymmetricKind → (ℓ : Level) → Monoid _ _
×-monoid k ℓ = record
{ isMonoid = ×-isMonoid k ℓ
}
×-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _×_ ⊤
×-isCommutativeMonoid k ℓ = record
{ isMonoid = ×-isMonoid k ℓ
; comm = λ _ _ → ↔⇒ (×-comm _ _)
}
×-commutativeMonoid : SymmetricKind → (ℓ : 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 : SymmetricKind → (ℓ : 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 : SymmetricKind → (ℓ : Level) → Semigroup _ _
⊎-semigroup k ℓ = record
{ isSemigroup = ⊎-isSemigroup k ℓ
}
⊎-isMonoid : ∀ k ℓ → IsMonoid (Related ⌊ k ⌋) _⊎_ ⊥
⊎-isMonoid k ℓ = record
{ isSemigroup = ⊎-isSemigroup k ℓ
; identity = (↔⇒ ∘ ⊎-identityˡ ℓ) , (↔⇒ ∘ ⊎-identityʳ ℓ)
}
⊎-monoid : SymmetricKind → (ℓ : Level) → Monoid _ _
⊎-monoid k ℓ = record
{ isMonoid = ⊎-isMonoid k ℓ
}
⊎-isCommutativeMonoid : ∀ k ℓ → IsCommutativeMonoid (Related ⌊ k ⌋) _⊎_ ⊥
⊎-isCommutativeMonoid k ℓ = record
{ isMonoid = ⊎-isMonoid k ℓ
; comm = λ _ _ → ↔⇒ (⊎-comm _ _)
}
⊎-commutativeMonoid : SymmetricKind → (ℓ : Level) →
CommutativeMonoid _ _
⊎-commutativeMonoid k ℓ = record
{ isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
}
×-⊎-isCommutativeSemiring : ∀ k ℓ →
IsCommutativeSemiring (Related ⌊ k ⌋) _⊎_ _×_ ⊥ ⊤
×-⊎-isCommutativeSemiring k ℓ = isCommutativeSemiringˡ record
{ +-isCommutativeMonoid = ⊎-isCommutativeMonoid k ℓ
; *-isCommutativeMonoid = ×-isCommutativeMonoid k ℓ
; distribʳ = λ _ _ _ → ↔⇒ ×-distribʳ-⊎
; zeroˡ = ↔⇒ ∘ ×-zeroˡ ℓ
}
×-⊎-commutativeSemiring : SymmetricKind → (ℓ : 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)
ΠΠ↔ΠΠ _ = mk↔ₛ′ flip flip (λ _ → refl) (λ _ → 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 = mk↔ₛ′ to from (λ _ → refl) (λ _ → 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 : Set a} {B : A → Set b} →
((x : A) → B x) ↔ ({x : A} → B x)
Π↔Π = mk↔ₛ′ _$- λ- (λ _ → refl) (λ _ → refl)
------------------------------------------------------------------------
-- _→_ preserves the symmetric relations
→-cong-⇔ : A ⇔ B → C ⇔ D → (A → C) ⇔ (B → D)
→-cong-⇔ A⇔B C⇔D = mk⇔
(λ f → to C⇔D ∘ f ∘ from A⇔B)
(λ f → from C⇔D ∘ f ∘ to A⇔B)
where open Equivalence
→-cong-↔ : Extensionality a c → Extensionality b d →
{A : Set a} {B : Set b} {C : Set c} {D : Set d} →
A ↔ B → C ↔ D → (A → C) ↔ (B → D)
→-cong-↔ ext₁ ext₂ A↔B C↔D = mk↔ₛ′
(λ f → to C↔D ∘ f ∘ from A↔B)
(λ f → from C↔D ∘ f ∘ to A↔B)
(λ f → ext₂ λ x → begin
to C↔D (from C↔D (f (to A↔B (from A↔B x)))) ≡⟨ strictlyInverseˡ C↔D _ ⟩
f (to A↔B (from A↔B x)) ≡⟨ cong f $ strictlyInverseˡ A↔B x ⟩
f x ∎)
(λ f → ext₁ λ x → begin
from C↔D (to C↔D (f (from A↔B (to A↔B x)))) ≡⟨ strictlyInverseʳ C↔D _ ⟩
f (from A↔B (to A↔B x)) ≡⟨ cong f $ strictlyInverseʳ A↔B x ⟩
f x ∎)
where open Inverse; open ≡-Reasoning
→-cong : 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} = →-cong-⇔
→-cong extAC extBD {bijection} = →-cong-↔ extAC extBD
------------------------------------------------------------------------
-- ¬_ (at Level 0) preserves the symmetric relations
¬-cong-⇔ : A ⇔ B → (¬ A) ⇔ (¬ B)
¬-cong-⇔ A⇔B = →-cong-⇔ A⇔B (Identity.⇔-id _)
¬-cong : 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 refl)
------------------------------------------------------------------------
-- _⇔_ preserves _⇔_
-- The type of the following proof is a bit more general.
Related-cong :
∀ {k} →
A ∼[ ⌊ k ⌋ ] B → C ∼[ ⌊ k ⌋ ] D → (A ∼[ ⌊ k ⌋ ] C) ⇔ (B ∼[ ⌊ k ⌋ ] D)
Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
(λ 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
------------------------------------------------------------------------
-- Relating a predicate to an existentially quantified one with the
-- restriction that the quantified variable is equal to the given one
∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
(λ where (_ , refl , _) → refl) (λ where _ → refl)
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