{-# OPTIONS --without-K --safe #-}
module Function.Bundles where
open import Function.Base using (_∘_)
import Function.Definitions as FunctionDefinitions
import Function.Structures as FunctionStructures
open import Level using (Level; _⊔_; suc)
open import Data.Product using (_,_; proj₁; proj₂)
open import Relation.Binary hiding (_⇔_)
open import Relation.Binary.PropositionalEquality as ≡
using (_≡_)
open Setoid using (isEquivalence)
private
variable
a b ℓ₁ ℓ₂ : Level
module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
open Setoid To using () renaming (Carrier to B; _≈_ to _≈₂_)
open FunctionDefinitions _≈₁_ _≈₂_
open FunctionStructures _≈₁_ _≈₂_
record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
cong : to Preserves _≈₁_ ⟶ _≈₂_
isCongruent : IsCongruent to
isCongruent = record
{ cong = cong
; isEquivalence₁ = isEquivalence From
; isEquivalence₂ = isEquivalence To
}
open IsCongruent isCongruent public
using (module Eq₁; module Eq₂)
record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
cong : to Preserves _≈₁_ ⟶ _≈₂_
injective : Injective to
function : Func
function = record
{ to = to
; cong = cong
}
open Func function public
hiding (to; cong)
isInjection : IsInjection to
isInjection = record
{ isCongruent = isCongruent
; injective = injective
}
record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
cong : to Preserves _≈₁_ ⟶ _≈₂_
surjective : Surjective to
to⁻ : B → A
to⁻ = proj₁ ∘ surjective
isCongruent : IsCongruent to
isCongruent = record
{ cong = cong
; isEquivalence₁ = isEquivalence From
; isEquivalence₂ = isEquivalence To
}
open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
isSurjection : IsSurjection to
isSurjection = record
{ isCongruent = isCongruent
; surjective = surjective
}
record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
cong : to Preserves _≈₁_ ⟶ _≈₂_
bijective : Bijective to
injective : Injective to
injective = proj₁ bijective
surjective : Surjective to
surjective = proj₂ bijective
injection : Injection
injection = record
{ cong = cong
; injective = injective
}
surjection : Surjection
surjection = record
{ cong = cong
; surjective = surjective
}
open Injection injection public using (isInjection)
open Surjection surjection public using (isSurjection; to⁻)
isBijection : IsBijection to
isBijection = record
{ isInjection = isInjection
; surjective = surjective
}
open IsBijection isBijection public using (module Eq₁; module Eq₂)
record Equivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from-cong : from Preserves _≈₂_ ⟶ _≈₁_
record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from-cong : from Preserves _≈₂_ ⟶ _≈₁_
inverseˡ : Inverseˡ to from
isCongruent : IsCongruent to
isCongruent = record
{ cong = to-cong
; isEquivalence₁ = isEquivalence From
; isEquivalence₂ = isEquivalence To
}
open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
isLeftInverse : IsLeftInverse to from
isLeftInverse = record
{ isCongruent = isCongruent
; from-cong = from-cong
; inverseˡ = inverseˡ
}
equivalence : Equivalence
equivalence = record
{ to-cong = to-cong
; from-cong = from-cong
}
record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from-cong : from Preserves _≈₂_ ⟶ _≈₁_
inverseʳ : Inverseʳ to from
isCongruent : IsCongruent to
isCongruent = record
{ cong = to-cong
; isEquivalence₁ = isEquivalence From
; isEquivalence₂ = isEquivalence To
}
isRightInverse : IsRightInverse to from
isRightInverse = record
{ isCongruent = isCongruent
; from-cong = from-cong
; inverseʳ = inverseʳ
}
equivalence : Equivalence
equivalence = record
{ to-cong = to-cong
; from-cong = from-cong
}
record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from-cong : from Preserves _≈₂_ ⟶ _≈₁_
inverse : Inverseᵇ to from
inverseˡ : Inverseˡ to from
inverseˡ = proj₁ inverse
inverseʳ : Inverseʳ to from
inverseʳ = proj₂ inverse
leftInverse : LeftInverse
leftInverse = record
{ to-cong = to-cong
; from-cong = from-cong
; inverseˡ = inverseˡ
}
rightInverse : RightInverse
rightInverse = record
{ to-cong = to-cong
; from-cong = from-cong
; inverseʳ = inverseʳ
}
open LeftInverse leftInverse public using (isLeftInverse)
open RightInverse rightInverse public using (isRightInverse)
isInverse : IsInverse to from
isInverse = record
{ isLeftInverse = isLeftInverse
; inverseʳ = inverseʳ
}
open IsInverse isInverse public using (module Eq₁; module Eq₂)
record BiEquivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from₁ : B → A
from₂ : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from₁-cong : from₁ Preserves _≈₂_ ⟶ _≈₁_
from₂-cong : from₂ Preserves _≈₂_ ⟶ _≈₁_
record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
to : A → B
from₁ : B → A
from₂ : B → A
to-cong : to Preserves _≈₁_ ⟶ _≈₂_
from₁-cong : from₁ Preserves _≈₂_ ⟶ _≈₁_
from₂-cong : from₂ Preserves _≈₂_ ⟶ _≈₁_
inverseˡ : Inverseˡ to from₁
inverseʳ : Inverseʳ to from₂
to-isCongruent : IsCongruent to
to-isCongruent = record
{ cong = to-cong
; isEquivalence₁ = isEquivalence From
; isEquivalence₂ = isEquivalence To
}
isBiInverse : IsBiInverse to from₁ from₂
isBiInverse = record
{ to-isCongruent = to-isCongruent
; from₁-cong = from₁-cong
; from₂-cong = from₂-cong
; inverseˡ = inverseˡ
; inverseʳ = inverseʳ
}
biEquivalence : BiEquivalence
biEquivalence = record
{ to-cong = to-cong
; from₁-cong = from₁-cong
; from₂-cong = from₂-cong
}
infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_
_⟶_ : Set a → Set b → Set _
A ⟶ B = Func (≡.setoid A) (≡.setoid B)
_↣_ : Set a → Set b → Set _
A ↣ B = Injection (≡.setoid A) (≡.setoid B)
_↠_ : Set a → Set b → Set _
A ↠ B = Surjection (≡.setoid A) (≡.setoid B)
_⤖_ : Set a → Set b → Set _
A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)
_⇔_ : Set a → Set b → Set _
A ⇔ B = Equivalence (≡.setoid A) (≡.setoid B)
_↩_ : Set a → Set b → Set _
A ↩ B = LeftInverse (≡.setoid A) (≡.setoid B)
_↪_ : Set a → Set b → Set _
A ↪ B = RightInverse (≡.setoid A) (≡.setoid B)
_↩↪_ : Set a → Set b → Set _
A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B)
_↔_ : Set a → Set b → Set _
A ↔ B = Inverse (≡.setoid A) (≡.setoid B)
module _ {A : Set a} {B : Set b} where
open FunctionDefinitions {A = A} {B} _≡_ _≡_
mk⟶ : (A → B) → A ⟶ B
mk⟶ to = record
{ to = to
; cong = ≡.cong to
}
mk↣ : ∀ {to : A → B} → Injective to → A ↣ B
mk↣ {to} inj = record
{ to = to
; cong = ≡.cong to
; injective = inj
}
mk↠ : ∀ {to : A → B} → Surjective to → A ↠ B
mk↠ {to} surj = record
{ to = to
; cong = ≡.cong to
; surjective = surj
}
mk⤖ : ∀ {to : A → B} → Bijective to → A ⤖ B
mk⤖ {to} bij = record
{ to = to
; cong = ≡.cong to
; bijective = bij
}
mk⇔ : ∀ (to : A → B) (from : B → A) → A ⇔ B
mk⇔ to from = record
{ to = to
; from = from
; to-cong = ≡.cong to
; from-cong = ≡.cong from
}
mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ to from → A ↩ B
mk↩ {to} {from} invˡ = record
{ to = to
; from = from
; to-cong = ≡.cong to
; from-cong = ≡.cong from
; inverseˡ = invˡ
}
mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ to from → A ↪ B
mk↪ {to} {from} invʳ = record
{ to = to
; from = from
; to-cong = ≡.cong to
; from-cong = ≡.cong from
; inverseʳ = invʳ
}
mk↩↪ : ∀ {to : A → B} {from₁ : B → A} {from₂ : B → A} →
Inverseˡ to from₁ → Inverseʳ to from₂ → A ↩↪ B
mk↩↪ {to} {from₁} {from₂} invˡ invʳ = record
{ to = to
; from₁ = from₁
; from₂ = from₂
; to-cong = ≡.cong to
; from₁-cong = ≡.cong from₁
; from₂-cong = ≡.cong from₂
; inverseˡ = invˡ
; inverseʳ = invʳ
}
mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ to from → A ↔ B
mk↔ {to} {from} inv = record
{ to = to
; from = from
; to-cong = ≡.cong to
; from-cong = ≡.cong from
; inverse = inv
}
mk↔′ : ∀ (to : A → B) (from : B → A) → Inverseˡ to from → Inverseʳ to from → A ↔ B
mk↔′ to from invˡ invʳ = mk↔ {to = to} {from = from} (invˡ , invʳ)