{-# OPTIONS --without-K --safe #-}
module Function.Bijection where
open import Data.Product
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
open import Function.Equality as F
using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
open import Function.Injection as Inj hiding (id; _∘_; injection)
open import Function.Surjection as Surj hiding (id; _∘_; surjection)
open import Function.LeftInverse as Left hiding (id; _∘_; leftInverse)
record Bijective {f₁ f₂ t₁ t₂}
{From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
(to : From ⟶ To) :
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
field
injective : Injective to
surjective : Surjective to
open Surjective surjective public
left-inverse-of : from LeftInverseOf to
left-inverse-of x = injective (right-inverse-of (to ⟨$⟩ x))
record Bijection {f₁ f₂ t₁ t₂}
(From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
field
to : From ⟶ To
bijective : Bijective to
open Bijective bijective public
injection : Injection From To
injection = record
{ to = to
; injective = injective
}
surjection : Surjection From To
surjection = record
{ to = to
; surjective = surjective
}
open Surjection surjection public
using (equivalence; right-inverse; from-to)
left-inverse : LeftInverse From To
left-inverse = record
{ to = to
; from = from
; left-inverse-of = left-inverse-of
}
open LeftInverse left-inverse public using (to-from)
infix 3 _⤖_
_⤖_ : ∀ {f t} → Set f → Set t → Set _
From ⤖ To = Bijection (P.setoid From) (P.setoid To)
bijection : ∀ {f t} {From : Set f} {To : Set t} →
(to : From → To) (from : To → From) →
(∀ {x y} → to x ≡ to y → x ≡ y) →
(∀ x → to (from x) ≡ x) →
From ⤖ To
bijection to from inj invʳ = record
{ to = P.→-to-⟶ to
; bijective = record
{ injective = inj
; surjective = record
{ from = P.→-to-⟶ from
; right-inverse-of = invʳ
}
}
}
id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Bijection S S
id {S = S} = record
{ to = F.id
; bijective = record
{ injective = Injection.injective (Inj.id {S = S})
; surjective = Surjection.surjective (Surj.id {S = S})
}
}
infixr 9 _∘_
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
{F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
Bijection M T → Bijection F M → Bijection F T
f ∘ g = record
{ to = to f ⟪∘⟫ to g
; bijective = record
{ injective = Injection.injective (Inj._∘_ (injection f) (injection g))
; surjective = Surjection.surjective (Surj._∘_ (surjection f) (surjection g))
}
} where open Bijection