# Mere functions

Content created by Egbert Rijke and Fredrik Bakke.

Created 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|))