Univalence

Transport of function types
The types of axioms

{-# OPTIONS --without-K --safe #-}

module univalence-consequences where 

open import mltt
open import twocatconstructions
open import basichomotopy
open import univalence-base
open import univalence-funext

open ≡-Reasoning
open ◾-lemmas

Transport of function types

We deduce some consequences from the univalence and function extensionality axioms. Of course, we now know the latter follows from the former. However, it simplifies some of the statements to directly assume function extensionality instead of univalence.

Some of these lemmas are of independent interest, in that they allow, or will allow, to explicitly compute transports involving function types. The general scheme is the following: given have dependent types \(P , Q \colon A → 𝓤\), we consider the transport of a function type \(f \colon P x → Q x\) along a path \(p \colon x ≡ y\) in the base.

The first one, as a matter of fact, does not rely on function extensionality, and can be cleanly proved by path induction.

transport-is-conjugation : ∀ {ℓ ℓ'} {A : Set ℓ} {P Q : A → Set ℓ'} {x y : A}
                           (p : x ≡ y) (f : P x → Q x) → 
                           transport (λ v → P v → Q v) p f ≡ (λ u → transport Q p (f (transport P (p ⁻¹) u)))
transport-is-conjugation refl f = refl

The main task is to compare the transport of \(f \colon P x → Q x\) along \(p \colon x ≡ y\) to a function \(g \colon P y → Q y\). For this, we assume function extensionality:

module funext-transport {ℓ ℓ' : Level}
                        (hfe : hfunext ℓ' ℓ') 
                          where


  transport-and-equality : {A : Set ℓ} {P Q : A → Set ℓ'} {x y : A}
                           (p : x ≡ y) (f : P x → Q x) (g : P y → Q y) →
                           (transport (λ v → P v → Q v) p f ≡ g) ≃ ( Π[ u ∈ P x ] (transport Q p (f u) ≡ g (transport P p u)) )
  transport-and-equality refl f g = (happly f g) , (hfe f g)

  -- using the syntax declaration
  transport-and-equality' : {A : Set ℓ} {P Q : A → Set ℓ'} {x y : A}
                            (p : x ≡ y) (f : P x → Q x) (g : P y → Q y) →
                            p ✴ f ≡ g ≃ ( Π[ u ∈ P x ] (transport Q p (f u) ≡ g (transport P p u)) )
  transport-and-equality' refl f g = (happly f g) , (hfe f g)

  module transport-and-equality-path
          {A : Set ℓ} {P Q : A → Set ℓ'} {x y : A}
          (p : x ≡ y) (f : P x → Q x) (g : P y → Q y)
          (q : p ✴ f ≡ g)
            where


    q̂ : Π[ u ∈ P x ] (transport Q p (f u) ≡ g (transport P p u))
    q̂ = π₁ (transport-and-equality p f g) q

    q̂₁ : Π[ u ∈ P x ] (transport (λ v → P v → Q v) p f (transport P p u) ≡ g (transport P p u))
    q̂₁ u = transport (λ v → P v → Q v) p f (transport P p u)        ≡⟨ ap (ev' (transport P p u)) (transport-is-conjugation p f)  ⟩
           transport Q p (f (transport P (p ⁻¹) (transport P p u))) ≡⟨ ap (transport Q p) lemma  ⟩
           transport Q p (f u)                                      ≡⟨ q̂ u ⟩
           g (transport P p u)                                      ∎
              where
                open transport-lemmas
                lemma : f (transport P (p ⁻¹) (transport P p u)) ≡ f u
                lemma = f (transport P (p ⁻¹) (transport P p u)) ≡⟨ ap f (transport◾ p (p ⁻¹)  {u}) ⟩
                        f (transport P (p ◾ p ⁻¹) u)             ≡⟨ ap f (transport≡ (rinv p))  ⟩
                        f u                                      ∎

  identity : {A : Set ℓ} {P Q : A → Set ℓ'} {x y : A}
             (p : x ≡ y) (f : P x → Q x) (g : P y → Q y)
             (q : p ✴ f ≡ g) → (u : P x) → 
             (happly (transport (λ v → P v → Q v) p f) g q) (transport P p u) ≡ transport-and-equality-path.q̂₁ p f g q u 
  identity refl f g q u = (ru (ap (λ f₁ → f₁ u) q)) ⁻¹

module univ-transport {ℓ : Level} (ua : is-univalent ℓ) (A B : Set ℓ) (u : A ≃ B) where

  open U-Rules ua

  p : A ≡ B
  p = Eq→Id A B u

  e : A → B
  e = π₁ u

  e⁻¹ : B → A
  e⁻¹ = Id→Fun (p ⁻¹)

  private

    e₁ : A → B
    e₁ = Id→Fun p

    γ : e₁ ≡ e
    γ = ap π₁ (Eq→Id-is-rinv u)

    -- γ̂ : e₁ ~ e
    -- γ̂ = happly _ _ γ

  function-transport₁ : (f : A → A) → transport (λ Z → Z → Z) p f ≡ λ b → e (f (e⁻¹ b))
  function-transport₁ f = transport (λ Z → Z → Z) p f   ≡⟨ transport-is-conjugation {P = λ Z → Z} {Q = λ Z → Z} {A} {B} p f ⟩
                          (λ b → e₁ (f (e⁻¹ b)))        ≡⟨ ap (λ h → (λ b → h (f (e⁻¹ b)))) γ ⟩
                          (λ b → e (f (e⁻¹ b)))         ∎

  function-transport₂ : (f : A → A → A) → transport (λ Z → Z → Z → Z) p f ≡ λ b b₁ → e (f (e⁻¹ b) (e⁻¹ b₁))
  function-transport₂ f = transport (λ Z → Z → Z → Z) p f 
                                    ≡⟨ transport-is-conjugation {P = λ Z → Z} {Q = λ Z → Z → Z} {A} {B} p f ⟩
                          (λ b → transport (λ Z → Z → Z) p (f (e⁻¹ b)))
                                    ≡⟨ dfe _ _ δ ⟩
                          (λ b b₁ → e (f (e⁻¹ b) (e⁻¹ b₁))) ∎
                            where
                              dfe : dfunext ℓ ℓ
                              dfe = univalence→dfunext ua

                              δ = λ b → function-transport₁ (f (e⁻¹ b))

top ⇑

The types of axioms

open import sets-logic
open import more-logic

iseq-is-prop : ∀ {ℓ ℓ'} → dfunext ℓ' (ℓ ⊔ ℓ') → dfunext (ℓ ⊔ ℓ') (ℓ ⊔ ℓ') →
               {A : Set ℓ}{B : Set ℓ'} (f : A → B) →
               isProp (isweq f)
iseq-is-prop dfe dfe⁺ f = Π-prop-is-prop dfe (λ b → isSingleton-is-Prop dfe⁺ {hfib f b})

top ⇑

Univalence—Ⅳ

Contents

Transport of function types

The types of axioms