Dependent function types

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-01-28.

module foundation.dependent-function-types where
Imports 
open import foundation.dependent-pair-types
open import foundation.spans-families-of-types
open import foundation.terminal-spans-families-of-types
open import foundation.type-arithmetic-dependent-function-types
open import foundation.universal-property-dependent-function-types
open import foundation.universe-levels

Idea

Consider a family B of types over A. A dependent function that takes elements x : A to elements of type B x is an assignment of an element f x : B x for each x : A. In Agda, dependent functions can be written using λ-abstraction, i.e., using the syntax

  λ x → f x.

Informally, we also use the notation x ↦ f x for the assignment of values of a dependent function f.

The type of dependent function (x : A) → B x is built in to the kernel of Agda, and doesn’t need to be introduced by us. The purpose of this file is to record some properties of dependent function types.

Definitions

The structure of a span on a family of types on a dependent function type

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

  span-type-family-Π : span-type-family (l1 ⊔ l2) B
  pr1 span-type-family-Π = (x : A) → B x
  pr2 span-type-family-Π x f = f x

Properties

Dependent function types satisfy the universal property of dependent function types

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

  abstract
    universal-property-dependent-function-types-Π :
      universal-property-dependent-function-types (span-type-family-Π B)
    universal-property-dependent-function-types-Π T = is-equiv-swap-Π

Dependent function types are terminal spans on families of types

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

  abstract
    is-terminal-span-type-family-Π :
      is-terminal-span-type-family (span-type-family-Π B)
    is-terminal-span-type-family-Π =
      is-terminal-universal-property-dependent-function-types
        ( span-type-family-Π B)
        ( universal-property-dependent-function-types-Π B)

Recent changes