Evaluation of functions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-02-06.
Last modified 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

See also

Recent changes