Mere functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2025-10-17.

module foundation.mere-functions where
Imports 
open import foundation.evaluation-functions
open import foundation.functoriality-propositional-truncation
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.propositions

Idea

The type of mere functions from A to B is the propositional truncation of the type of maps from A to B.

  mere-function A B := ║(A → B)║₋₁

Definitions

Mere functions between types

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  prop-mere-function : Prop (l1 ⊔ l2)
  prop-mere-function = trunc-Prop (A → B)

  mere-function : UU (l1 ⊔ l2)
  mere-function = type-Prop prop-mere-function

  is-prop-mere-function : is-prop mere-function
  is-prop-mere-function = is-prop-type-Prop prop-mere-function

The evaluation map on mere functions

If we have a mere function from A to B and A is inhabited, then B is inhabited.

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  ev-mere-function' : (mere-function A B) → A → ║ B ║₋₁
  ev-mere-function' |f| a = map-trunc-Prop (ev a) |f|

  ev-mere-function : (mere-function A B) → ║ A ║₋₁ → ║ B ║₋₁
  ev-mere-function |f| =
    rec-trunc-Prop (trunc-Prop B) (ev-mere-function' |f|)

Mere functions form a reflexive relation

module _
  {l : Level} (A : UU l)
  where

  refl-mere-function : mere-function A A
  refl-mere-function = unit-trunc-Prop id

Mere functions form a transitive relation

module _
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
  where

  transitive-mere-function :
    mere-function B C → mere-function A B → mere-function A C
  transitive-mere-function =
    map-binary-trunc-Prop (λ g f → g ∘ f)

See also

Recent changes