Type arithmetic with dependent function types

module foundation.type-arithmetic-dependent-function-types where
Imports 
open import foundation.functoriality-dependent-function-types
open import foundation.type-arithmetic-unit-type
open import foundation.unit-type

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.univalence
open import foundation-core.universe-levels

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 , 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-has-inverse 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