Type arithmetic with dependent function types

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

Created on 2022-07-17.
Last modified on 2024-03-01.

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

See also

Recent changes