# Type arithmetic with dependent function types

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Victor Blanchi.

Created on 2022-07-17.

module foundation.type-arithmetic-dependent-function-types where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-function-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.univalence


## Properties

### Unit law when the base type is contractible

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

left-unit-law-Π-is-contr : ((a : A) → (B a)) ≃ B a
left-unit-law-Π-is-contr =
( left-unit-law-Π ( λ _ → B a)) ∘e
( equiv-Π
( λ _ → B a)
( terminal-map A , is-equiv-terminal-map-is-contr C)
( λ a → equiv-eq (ap B ( eq-is-contr C))))


### The swap function ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y) is an equivalence

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A → B → UU l3}
where

swap-Π : ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
swap-Π f y x = f x y

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A → B → UU l3}
where

is-equiv-swap-Π : is-equiv (swap-Π {C = C})
is-equiv-swap-Π = is-equiv-is-invertible swap-Π refl-htpy refl-htpy

equiv-swap-Π : ((x : A) (y : B) → C x y) ≃ ((y : B) (x : A) → C x y)
pr1 equiv-swap-Π = swap-Π
pr2 equiv-swap-Π = is-equiv-swap-Π