Evaluation of functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-02-06.

module foundation.evaluation-functions where

Imports
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.identity-types


Idea

Consider a family of types B over A and let a : A be an element. The evaluation function at a

  ev : ((x : A) → B x) → B a


is the map given by f ↦ f a, evaluating dependent functions at a.

Definitions

The evaluation function

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

ev : ((x : A) → B x) → B a
ev f = f a


The evaluation function with an explicit type family

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

ev-dependent-function : ((x : A) → B x) → B a
ev-dependent-function = ev a


The evaluation function for nondependent functions

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

ev-function : (A → B) → B
ev-function = ev a


The evaluation function of implicit functions

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

ev-implicit-function : ({x : A} → B x) → B a
ev-implicit-function f = f {a}


The evaluation function of implicit functions, specified with an explicit type family

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

ev-implicit-function' : ({x : A} → B x) → B a
ev-implicit-function' = ev-implicit-function a