{-
This file contains:
- Id, refl and J (with definitional computation rule)
- Basic theory about Id, proved using J
- Lemmas for going back and forth between Path and Id
- Function extesionality for Id
- fiber, isContr, equiv all defined using Id
- The univalence axiom expressed using only Id ([EquivContr])
- Propositional truncation and its elimination principle
-}
{-# OPTIONS --safe #-}
module Cubical.Foundations.Id where
open import Cubical.Foundations.Prelude public
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ ; isPropIsContr)
  renaming ( refl      to reflPath
           ; transport to transportPath
           ; J         to JPath
           ; JRefl     to JPathRefl
           ; sym       to symPath
           ; _∙_       to compPath
           ; cong      to congPath
           ; funExt    to funExtPath
           ; isContr   to isContrPath
           ; isProp    to isPropPath
           ; isSet     to isSetPath
           ; fst       to pr₁ -- as in the HoTT book
           ; snd       to pr₂ )
open import Cubical.Foundations.Equiv
  renaming ( fiber        to fiberPath
           ; isEquiv   to isEquivPath
           ; _≃_       to EquivPath
           ; equivFun  to equivFunPath
           ; isPropIsEquiv to isPropIsEquivPath )
  hiding   ( equivCtr
           ; equivIsEquiv )
open import Cubical.Foundations.Univalence
  renaming ( EquivContr   to EquivContrPath )
open import Cubical.Foundations.Isomorphism
open import Cubical.HITs.PropositionalTruncation public
  renaming (rec to recPropTruncPath ; elim to elimPropTruncPath )
open import Cubical.Core.Id public
  using (Id; ⟨_,_⟩; faceId; pathId; elimId; _≡_)
private
  variable
     ℓ' : Level
    A : Type 
-- Version of the constructor for Id where the y is also
-- explicit. This is sometimes useful when it is needed for
-- typechecking (see JId below).
conId :  {x : A} φ (y : A [ φ   _  x) ])
          (w : (Path _ x (outS y)) [ φ   { (φ = i1)  λ _  x}) ]) 
          x  outS y
conId φ _ w =  φ , outS w 
-- Reflexivity
refl :  {x : A}  x  x
refl {x = x} =  i1 ,  _  x) 

-- Definition of J for Id
module _ {x : A} (P :  (y : A)  Id x y  Type ℓ') (d : P x refl) where
  J :  {y : A} (w : x  y)  P y w
  J {y = y} = elimId P  φ y w  comp  i  P _ (conId (φ  ~ i) (inS (outS w i))
                                                                   (inS  j  outS w (i  j)))))
                                        i  λ { (φ = i1)  d}) d) {y = y}
  -- Check that J of refl is the identity function
  Jdefeq : Path _ (J refl) d
  Jdefeq _ = d

-- Basic theory about Id, proved using J
transport :  (B : A  Type ℓ') {x y : A}
            x  y  B x  B y
transport B {x} p b = J  y p  B y) b p
_⁻¹ : {x y : A}  x  y  y  x
_⁻¹ {x = x} p = J  z _  z  x) refl p
ap :  {B : Type ℓ'} (f : A  B)   {x y : A}  x  y  f x  f y
ap f {x} = J  z _  f x  f z) refl
_∙_ :  {x y z : A}  x  y  y  z  x  z
_∙_ {x = x} p = J  y _  x  y) p
infix  4 _∙_
infix  3 _∎
infixr 2 _≡⟨_⟩_
_≡⟨_⟩_ : (x : A) {y z : A}  x  y  y  z  x  z
_ ≡⟨ p  q = p  q
_∎ : (x : A)  x  x
_  = refl
-- Convert between Path and Id
pathToId :  {x y : A}  Path _ x y  Id x y
pathToId {x = x} = JPath  y _  Id x y) refl
pathToIdRefl :  {x : A}  Path _ (pathToId  _  x)) refl
pathToIdRefl {x = x} = JPathRefl  y _  Id x y) refl
idToPath :  {x y : A}  Id x y  Path _ x y
idToPath {x = x} = J  y _  Path _ x y)  _  x)
idToPathRefl :  {x : A}  Path _ (idToPath {x = x} refl) reflPath
idToPathRefl {x = x} _ _ = x
pathToIdToPath :  {x y : A}  (p : Path _ x y)  Path _ (idToPath (pathToId p)) p
pathToIdToPath {x = x} = JPath  y p  Path _ (idToPath (pathToId p)) p)
                                i  idToPath (pathToIdRefl i))
idToPathToId :  {x y : A}  (p : Id x y)  Path _ (pathToId (idToPath p)) p
idToPathToId {x = x} = J  b p  Path _ (pathToId (idToPath p)) p) pathToIdRefl

-- We get function extensionality by going back and forth between Path and Id
funExt :  {B : A  Type ℓ'} {f g : (x : A)  B x} 
         ((x : A)  f x  g x)  f  g
funExt p = pathToId  i x  idToPath (p x) i)

-- Equivalences expressed using Id
fiber :  {A : Type } {B : Type ℓ'} (f : A  B) (y : B)  Type (ℓ-max  ℓ')
fiber {A = A} f y = Σ[ x  A ] f x  y
isContr : Type   Type 
isContr A = Σ[ x  A ] (∀ y  x  y)
isProp : Type   Type 
isProp A = (x y : A)  x  y
isSet : Type   Type 
isSet A = (x y : A)  isProp (x  y)
record isEquiv {A : Type } {B : Type ℓ'} (f : A  B) : Type (ℓ-max  ℓ') where
  field
    equiv-proof : (y : B)  isContr (fiber f y)
open isEquiv public
infix 4 _≃_
_≃_ :  (A : Type ) (B : Type ℓ')  Type (ℓ-max  ℓ')
A  B = Σ[ f  (A  B) ] (isEquiv f)
equivFun :  {B : Type ℓ'}  A  B  A  B
equivFun e = pr₁ e
equivIsEquiv :  {B : Type ℓ'} (e : A  B)  isEquiv (equivFun e)
equivIsEquiv e = pr₂ e
equivCtr :  {B : Type ℓ'} (e : A  B) (y : B)  fiber (equivFun e) y
equivCtr e y = e .pr₂ .equiv-proof y .pr₁

-- Functions for going between the various definitions. This could
-- also be achieved by making lines in the universe and transporting
-- back and forth along them.
fiberPathToFiber :  {B : Type ℓ'} {f : A  B} {y : B} 
  fiberPath f y  fiber f y
fiberPathToFiber (x , p) = (x , pathToId p)
fiberToFiberPath :  {B : Type ℓ'} {f : A  B} {y : B} 
  fiber f y  fiberPath f y
fiberToFiberPath (x , p) = (x , idToPath p)
fiberToFiber :  {B : Type ℓ'} {f : A  B} {y : B}
  (p : fiber f y)  Path _ (fiberPathToFiber (fiberToFiberPath p)) p
fiberToFiber (x , p) = λ i  x , idToPathToId p i
fiberPathToFiberPath :  {B : Type ℓ'} {f : A  B} {y : B}
  (p : fiberPath f y)  Path _ (fiberToFiberPath (fiberPathToFiber p)) p
fiberPathToFiberPath (x , p) = λ i  x , pathToIdToPath p i
isContrPathToIsContr : isContrPath A  isContr A
isContrPathToIsContr (ctr , p) = (ctr , λ y  pathToId (p y))
isContrToIsContrPath : isContr A  isContrPath A
isContrToIsContrPath (ctr , p) = (ctr , λ y  idToPath (p y))
isPropPathToIsProp : isPropPath A  isProp A
isPropPathToIsProp H x y = pathToId (H x y)
isPropToIsPropPath : isProp A  isPropPath A
isPropToIsPropPath H x y i = idToPath (H x y) i
-- Specialized helper lemmas for going back and forth between
-- isContrPath and isContr:
helper1 :  {A B : Type } (f : A  B) (g : B  A)
            (h : (y : B)  Path B (f (g y)) y)  isContrPath A  isContr B
helper1 f g h (x , p) =
  (f x , λ y  pathToId  i  hcomp  j  λ { (i = i0)  f x
                                              ; (i = i1)  h y j })
                                     (f (p (g y) i))))
helper2 :  {A B : Type } (f : A  B) (g : B  A)
            (h : (y : A)  Path A (g (f y)) y)  isContr B  isContrPath A
helper2 {A = A} f g h (x , p) = (g x , λ y  idToPath (rem y))
  where
  rem :  (y : A)  g x  y
  rem y =
    g x     ≡⟨ ap g (p (f y)) 
    g (f y) ≡⟨ pathToId (h y) 
    y       
-- This proof is essentially the one for proving that isContr with
-- Path is a proposition, but as we are working with Id we have to
-- insert a lof of conversion functions. It is still nice that is
-- works like this though.
isPropIsContr :  (p1 p2 : isContr A)  Path (isContr A) p1 p2
isPropIsContr (a0 , p0) (a1 , p1) j =
  ( idToPath (p0 a1) j ,
    hcomp  i  λ { (j = i0)   λ x  idToPathToId (p0 x) i
                   ; (j = i1)   λ x  idToPathToId (p1 x) i })
           x  pathToId  i  hcomp  k  λ { (i = i0)  idToPath (p0 a1) j
                                                ; (i = i1)  idToPath (p0 x) (j  k)
                                                ; (j = i0)  idToPath (p0 x) (i  k)
                                                ; (j = i1)  idToPath (p1 x) i })
                                       (idToPath (p0 (idToPath (p1 x) i)) j))))
-- We now prove that isEquiv is a proposition
isPropIsEquiv :  {A : Type } {B : Type }  {f : A  B}  (h1 h2 : isEquiv f)  Path _ h1 h2
equiv-proof (isPropIsEquiv {f = f} h1 h2 i) y =
  isPropIsContr {A = fiber f y} (h1 .equiv-proof y) (h2 .equiv-proof y) i
-- Go from a Path equivalence to an Id equivalence
equivPathToEquiv :  {A : Type } {B : Type ℓ'}  EquivPath A B  A  B
equivPathToEquiv (f , p) =
  (f , λ { .equiv-proof y  helper1 fiberPathToFiber fiberToFiberPath fiberToFiber (p .equiv-proof y) })
-- Go from an Id equivalence to a Path equivalence
equivToEquivPath :  {A : Type } {B : Type ℓ'}  A  B  EquivPath A B
equivToEquivPath (f , p) =
  (f , λ { .equiv-proof y  helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y) })
equivToEquiv :  {A : Type } {B : Type }  (p : A  B)  Path _ (equivPathToEquiv (equivToEquivPath p)) p
equivToEquiv (f , p) i =
  (f , isPropIsEquiv  { .equiv-proof y  helper1 fiberPathToFiber fiberToFiberPath fiberToFiber
                                             (helper2 fiberPathToFiber fiberToFiberPath fiberPathToFiberPath (p .equiv-proof y)) }) p i)

-- We can finally prove univalence with Id everywhere from the one for Path
EquivContr :  (A : Type )  isContr (Σ[ T  Type  ] (T  A))
EquivContr { = } A = helper1 f1 f2 f12 (EquivContrPath A)
  where
  f1 : {A : Type }  Σ[ T  Type  ] (EquivPath T A)  Σ[ T  Type  ] (T  A)
  f1 (x , p) = x , equivPathToEquiv p
  f2 : {A : Type }  Σ[ T  Type  ] (T  A)  Σ[ T  Type  ] (EquivPath T A)
  f2 (x , p) = x , equivToEquivPath p
  f12 : (y : Σ[ T  Type  ] (T  A))  Path (Σ[ T  Type  ] (T  A)) (f1 (f2 y)) y
  f12 (x , p) i = x , equivToEquiv {A = x} {B = A} p i
-- Propositional truncation
∥∥-isProp :  (x y :  A ∥₁)  x  y
∥∥-isProp x y = pathToId (squash₁ x y)
∥∥-recursion :  {A : Type } {P : Type }  isProp P  (A  P)   A ∥₁  P
∥∥-recursion Pprop f x = recPropTruncPath (isPropToIsPropPath Pprop) f x
∥∥-induction :  {A : Type } {P :  A ∥₁  Type }  ((a :  A ∥₁)  isProp (P a)) 
                ((x : A)  P  x ∣₁)  (a :  A ∥₁)  P a
∥∥-induction Pprop f x = elimPropTruncPath  a  isPropToIsPropPath (Pprop a)) f x

-- Univalence
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)) .pr₂) 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)