Overture.Functions

Foundational function infrastructure

This is the Overture.Functions module of the Agda Universal Algebra Library.

This module collects the foundational definitions concerning raw functions A → B between bare types that are needed by the canonical Setoid/ tree. All the definitions here take their arguments at the level of bare types and raw functions; none presupposes a setoid structure. The setoid-respecting analogues — image and surjectivity for setoid functions 𝐴 ⟶ 𝐵 — live in Setoid.Functions.* and are independent. The two coexist because they have genuinely different type signatures and serve genuinely different call sites.¹

The contents fall into three clusters.

• Image and inverse. An inductive type Image f ∋ b representing the image of a raw function as the existence of a preimage, together with the Inv operation that extracts a preimage from an inhabitant of that type. The inductive presentation lets us compute a range-restricted inverse, which is what surjectivity needs.

• Surjectivity. A predicate IsSurjective f, the right-inverse SurjInv, the right-inverse-correctness lemma SurjInvIsInverseʳ, and the composition law epic-factor (used in the homomorphism factorization theorem in Setoid.Homomorphisms.Factor).

• Coordinate projection. Given an indexed family B : I → Type b over a type I with decidable equality, the projection proj j : (∀ i → B i) → B j and its surjectivity proof projIsOnto. Used in Setoid.Algebras.Products to witness that the carrier-level projection from a product algebra onto a single factor is a surjection — a bare-types claim about raw functions, even though it sits inside the Setoid tree.²

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Overture.Functions where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda standard library ------------------------------------------
open import Data.Empty        using ( ⊥-elim )
open import Data.Product      using ( Σ ; Σ-syntax ; _,_ ; proj₁ ; proj₂ )
open import Function          using ( _∘_ ; _$_ ; Surjective )
open import Level             using ( Level ; _⊔_ )
open import Relation.Binary   using ( Decidable )
open import Relation.Nullary  using ( Dec ; yes ; no )

open import Axiom.UniquenessOfIdentityProofs  using ( module Decidable⇒UIP )
open import Relation.Binary.PropositionalEquality
                              using ( _≡_ ; refl ; sym ; trans ; cong ; cong-app )

-- Imports from agda-algebras ------------------------------------------------------
open import Overture.Basic  using ( _≈_ ; _∙_ ; transport )

private variable a b c ι : Level

The image of a raw function

The image of a raw function f : A → B at a point b : B is the proposition that some a : A satisfies f a ≡ b. We represent it as an inductive type with one constructor, eq, which packages the witness a together with the equality proof. This inductive presentation matters: an inhabitant of Image f ∋ b carries an actual point of A, so we can extract that point computationally (the function Inv below). The corresponding Σ-type formulation Σ[ a ∈ A ] f a ≡ b would be logically equivalent but syntactically less convenient at the call sites; the legacy module has used the inductive form throughout, and the canonical Setoid tree consumes it that way.

module _ {A : Type a}{B : Type b} where

  data Image_∋_ (f : A → B) : B → Type (a ⊔ b) where
    eq : {b : B} → ∀ a → b ≡ f a → Image f ∋ b

Given an inhabitant of Image f ∋ b, we recover the underlying preimage by pattern matching on eq. This is the Inv function, a range-restricted inverse: it is defined exactly on those b : B that are demonstrably in the image of f.

  Inv : (f : A → B){b : B} → Image f ∋ b → A
  Inv _ (eq a _) = a

  InvIsInverseʳ : {f : A → B}{b : B}(q : Image f ∋ b) → f (Inv f q) ≡ b
  InvIsInverseʳ (eq _ p) = sym p

Surjectivity of raw functions

A raw function f : A → B is surjective when every b : B is in the image of f. The library distinguishes this from stdlib's Function.Surjective, which is a more general "respects two arbitrary equivalences" notion; the bare-types IsSurjective is the specialization to propositional equality on both sides. Conversion in either direction is straightforward, as the two helper lemmas below show.

module _ {A : Type a}{B : Type b} where

  IsSurjective : (A → B) → Type (a ⊔ b)
  IsSurjective f = ∀ y → Image f ∋ y

  IsSurjective→Surjective :  (f : A → B) → IsSurjective f
   →                         Surjective _≡_ _≡_ f
  IsSurjective→Surjective f fE y = goal
    where
    imgfy→A : Image f ∋ y → Σ[ x ∈ A ] f x ≡ y
    imgfy→A (eq x p) = x , sym p
    goal : Σ[ x ∈ A ] ({z : A} → z ≡ x → f z ≡ y)
    goal = proj₁ (imgfy→A $ fE y)
         , λ z≡fst → trans (cong f z≡fst) $ proj₂ (imgfy→A $ fE y)

  Surjective→IsSurjective :  (f : A → B) → Surjective {A = A} _≡_ _≡_ f
   →                         IsSurjective f
  Surjective→IsSurjective f fE y = eq (proj₁ $ fE y) (sym $ proj₂ (fE y) refl)

A right-inverse of a surjective f is obtained by composing Inv with the surjectivity proof. The right-inverse property is then immediate from InvIsInverseʳ above.

  SurjInv : (f : A → B) → IsSurjective f → B → A
  SurjInv f fE = Inv f ∘ fE

  SurjInvIsInverseʳ :  (f : A → B)(fE : IsSurjective f)
   →                   ∀ b → f ((SurjInv f fE) b) ≡ b
  SurjInvIsInverseʳ f fE b = InvIsInverseʳ (fE b)

The composition law for surjective functions: if f factors through g via h, and f is surjective, then so is h. This is consumed in Setoid.Homomorphisms.Factor to lift surjectivity through the homomorphism factorization diagram.

module _ {A : Type a}{B : Type b}{C : Type c} where

  epic-factor :  (f : A → B)(g : A → C)(h : C → B)
   →             f ≈ h ∘ g → IsSurjective f → IsSurjective h
  epic-factor f g h compId fe y = goal
    where
     finv : B → A
     finv = SurjInv f fe

     ζ : y ≡ f (finv y)
     ζ = sym (SurjInvIsInverseʳ f fe y)

     η : y ≡ (h ∘ g) (finv y)
     η = ζ ∙ compId (finv y)

     goal : Image h ∋ y
     goal = eq (g (finv y)) η

  epic-factor-intensional :  (f : A → B)(g : A → C)(h : C → B)
   →                         f ≡ h ∘ g → IsSurjective f → IsSurjective h
  epic-factor-intensional f g h compId fe y = goal
    where
     finv : B → A
     finv = SurjInv f fe

     ζ : f (finv y) ≡ y
     ζ = SurjInvIsInverseʳ f fe y

     η : (h ∘ g) (finv y) ≡ y
     η = (cong-app (sym compId) (finv y)) ∙ ζ

     goal : Image h ∋ y
     goal = eq (g (finv y)) (sym η)

Coordinate projection out of a dependent product

Given an indexed family B : I → Type b and a "default" point bs₀ : ∀ i → B i of the dependent product, we define the coordinate projection proj j and prove it surjective. The default point and the decidable equality on I are both essential: without a fallback value at indices i ≠ j we cannot construct a preimage of an arbitrary b : B j, and without decidable equality we cannot decide which coordinate to fill in with b.

The auxiliary update modifies the default point at the single coordinate j to take a given value b, leaving the other coordinates alone. The auxiliary update-id says that update bs₀ (j , b) evaluated at j gives back b, regardless of which proof of j ≡ j the decision procedure happens to produce. The latter is where uniqueness-of-identity-proofs (UIP) for the index type I enters: update-id cannot be proved without it, because the "yes" case has to handle a propositionally-but-not-definitionally trivial equality proof. The Decidable⇒UIP module from stdlib gives us UIP for any type with decidable equality, which is the assumption already made on I.

module _
  {I : Type ι}
  (_≟_ : Decidable {A = I} _≡_)
  {B : I → Type b}
  (bs₀ : ∀ i → B i)
  where
  open Decidable⇒UIP _≟_ using ( ≡-irrelevant )

  proj : (j : I) → (∀ i → B i) → B j
  proj j xs = xs j

  update : (∀ i → B i) → ((j , _) : Σ I B) → (∀ i → Dec (i ≡ j) → B i)
  update _   (_ , b)  i (yes x)  = transport B (sym x) b
  update bs  _        i (no  _)  = bs i

  update-id : ∀{j b} → (c : Dec (j ≡ j)) → update bs₀ (j , b) j c ≡ b
  update-id {j} {b}  (yes p) = cong (λ x → transport B x b)
                                    (≡-irrelevant (sym p) refl)
  update-id          (no ¬p) = ⊥-elim (¬p refl)

  proj-is-onto : ∀{j} → Surjective {A = ∀ i → B i} _≡_ _≡_ (proj j)
  proj-is-onto {j} b = bs , λ x → trans (cong (λ u → proj j u) x) pf
    where
    bs : (i : I) → B i
    bs i = update bs₀ (j , b) i (i ≟ j)

    pf : proj j bs ≡ b
    pf = update-id (j ≟ j)

  projIsOnto : ∀{j} → IsSurjective (proj j)
  projIsOnto {j} = Surjective→IsSurjective (proj j) proj-is-onto

---

---

1. This module is a Category-A relocation under GitHub Issue #303 [M2-6]; see src/Legacy/Base/DEPRECATED.md for the full inventory and migration guidance. ↩

2. A setoid-respecting upgrade is tracked as a follow-up to Issue #303 [M2-6]. ↩