Mere functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-04-11.
Last modified on 2024-04-11.

module foundation.mere-functions where
open import foundation.propositional-truncations
open import foundation.universe-levels

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


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)║₋₁


Mere functions between types

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

  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)

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

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

Mere functions form a reflexive relation

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

  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}

  transitive-mere-function :
    mere-function B C  mere-function A B  mere-function A C
  transitive-mere-function |g| =
      ( prop-mere-function A C)
      ( λ f 
          ( prop-mere-function A C)
          ( λ g  unit-trunc-Prop (g  f))
          ( |g|))

See also

Recent changes