{-# OPTIONS --cubical --safe #-}
module Cubical.Foundations.UnivalenceId where

open import Cubical.Foundations.Prelude public
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ )
open import Cubical.Foundations.Id
open import Cubical.Foundations.Equiv
  renaming ( isEquiv      to isEquivPath
           ; _≃_          to EquivPath
           ; equivFun     to equivFunPath
           ; isPropIsEquiv to isPropIsEquivPath )
open import Cubical.Foundations.Univalence
  renaming ( EquivContr   to EquivContrPath )
open import Cubical.Foundations.Isomorphism

path≡Id :  {} {A B : Type }  Path _ (Path _ A B) (Id A B)
path≡Id = isoToPath (iso pathToId idToPath idToPathToId pathToIdToPath )

equivPathToEquivPath :  {} {A : Type } {B : Type }  (p : EquivPath A B) 
                       Path _ (equivToEquivPath (equivPathToEquiv p)) p
equivPathToEquivPath (f , p) i =
  ( f , isPropIsEquivPath f (equivToEquivPath (equivPathToEquiv (f , p)) .snd) p i )

equivPath≡Equiv :  {} {A B : Type }  Path _ (EquivPath A B) (A  B)
equivPath≡Equiv {} = isoToPath (iso (equivPathToEquiv {}) equivToEquivPath equivToEquiv equivPathToEquivPath)

univalenceId :  {} {A B : Type }  (A  B)  (A  B)
univalenceId {} {A = A} {B = B} = equivPathToEquiv rem
  where
  rem0 : Path _ (Lift (EquivPath A B)) (Lift (A  B))
  rem0 = congPath Lift equivPath≡Equiv

  rem1 : Path _ (Id A B) (Lift (A  B))
  rem1 i = hcomp  j  λ { (i = i0)  path≡Id {A = A} {B = B} j
                          ; (i = i1)  rem0 j })
                 (univalencePath {A = A} {B = B} i)

  rem : EquivPath (Id A B) (A  B)
  rem = compEquiv (eqweqmap rem1) (invEquiv LiftEquiv)