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
Imports 
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 =
    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)
  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 |g| =
    rec-trunc-Prop
      ( prop-mere-function A C)
      ( λ f →
        rec-trunc-Prop
          ( prop-mere-function A C)
          ( λ g → unit-trunc-Prop (g ∘ f))
          ( |g|))

See also

Recent changes