ua.agda

{-# OPTIONS --cubical --lossy-unification #-}
module _ (Y : Set) where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence

F : Type → Type
F X = (X → X) → Y

traditional-version : ∀ {A B} → (A ≃ B) → (F A ≃ F B)
traditional-version e =
  (λ f g → f λ a → invEquiv e .fst (g (e .fst a))) ,
    -- obvious map from F A to F B, just tedious to write
  {!   !} -- too complicated to write the proof of equivalence down

univalent-version : ∀ {A B} → (A ≃ B) → (F A ≃ F B)
univalent-version e = pathToEquiv (cong F (ua e))

two-version-equal : ∀ {A B} (e : A ≃ B)
  → traditional-version e .fst ≡ univalent-version e .fst
two-version-equal e =
  funExt λ f →
  funExt λ g →
     (f λ a → invEquiv e .fst (g (e .fst a)))
    ≡⟨ cong f (funExt λ a →
      cong (invEquiv e .fst) (sym
        (transportRefl _ ∙ cong g (transportRefl _)))) ⟩
      f (transport
        (λ j → (ua e) (~ j) → (ua e) (~ j))
        g)
    ≡⟨ sym (transportRefl _) ⟩
      transport refl
        (f (transport
          (λ j → (ua e) (~ j) → (ua e) (~ j))
          g))
    ∎