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


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.


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)

  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


Dependent function types satisfy the universal property of dependent function types

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

    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)

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

Recent changes