# The universal property of dependent function types

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-01-28.

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

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types

## Idea

Consider a family of types B over A. Then the dependent function type (a : A) → B a naturally has the structure of a span on the family of types B over A, where for each a : A the map

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

is given by evaluation at a.

A span 𝒮 := (S , f) is said to satisfy the universal property of dependent function types if for any type T the map

(T → S) → ((x : A) → T → B x)

given by h ↦ λ x t → f x (h t) is an equivalence. The dependent function type (x : A) → B x equipped with the span structure defined above satisfies the universal property of dependent function types.

In foundation.dependent-function-types we show that dependent function types satisfy the universal property of dependent function types. In this file we also show that the universal property of dependent function types is equivalent to being a terminal span on the type family B.

## Definitions

### The universal property of dependent function types

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} (𝒮 : span-type-family l3 B)
where

ev-span-type-family :
{l : Level} (T : UU l)
(T  spanning-type-span-type-family 𝒮)  (x : A)  T  B x
ev-span-type-family T h x t = map-span-type-family 𝒮 x (h t)

universal-property-dependent-function-types : UUω
universal-property-dependent-function-types =
{l : Level} (T : UU l)  is-equiv (ev-span-type-family T)

## Properties

### A span on a family of types satisfies the universal property of dependent function types if and only if it is terminal

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A  UU l2} (𝒮 : span-type-family l3 B)
where

abstract
is-terminal-universal-property-dependent-function-types :
universal-property-dependent-function-types 𝒮
is-terminal-span-type-family 𝒮
is-terminal-universal-property-dependent-function-types U 𝒯 =
is-contr-equiv' _
( equiv-tot
( λ h
( equiv-Π-equiv-family
( λ a
( equiv-Π-equiv-family  t  equiv-inv _ _)) ∘e
( equiv-funext))) ∘e
( equiv-funext)))
( is-contr-map-is-equiv
( U (spanning-type-span-type-family 𝒯))
( map-span-type-family 𝒯))

abstract
universal-property-dependent-function-types-is-terminal :
is-terminal-span-type-family 𝒮
universal-property-dependent-function-types 𝒮
universal-property-dependent-function-types-is-terminal U T =
is-equiv-is-contr-map
( λ g
is-contr-equiv _
( equiv-tot
( λ h
( equiv-Π-equiv-family
( λ a
( equiv-Π-equiv-family  t  equiv-inv _ _)) ∘e
( equiv-funext))) ∘e
( equiv-funext)))
( U (T , g)))