{-# OPTIONS --safe #-}
module Cubical.Foundations.Equiv.Fiberwise where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma

private
  variable
     ℓ' ℓ'' : Level

module _ {A : Type } (P : A  Type ℓ') (Q : A  Type ℓ'')
         (f :  x  P x  Q x)
         where
  private
    total : (Σ A P)  (Σ A Q)
    total = (\ p  p .fst , f (p .fst) (p .snd))

  -- Thm 4.7.6
  fibers-total :  {xv}  Iso (fiber total (xv)) (fiber (f (xv .fst)) (xv .snd))
  fibers-total {xv} = iso h g h-g g-h
   where
    h :  {xv}  fiber total xv  fiber (f (xv .fst)) (xv .snd)
    h {xv} (p , eq) = J (\ xv eq  fiber (f (xv .fst)) (xv .snd)) ((p .snd) , refl) eq
    g :  {xv}  fiber (f (xv .fst)) (xv .snd)  fiber total xv
    g {xv} (p , eq) = (xv .fst , p) , (\ i  _ , eq i)
    h-g :  {xv} y  h {xv} (g {xv} y)  y
    h-g {x , v} (p , eq) = J  _ eq₁  h (g (p , eq₁))  (p , eq₁)) (JRefl  xv₁ eq₁  fiber (f (xv₁ .fst)) (xv₁ .snd)) ((p , refl))) (eq)
    g-h :  {xv} y  g {xv} (h {xv} y)  y
    g-h {xv} ((a , p) , eq) = J  _ eq₁  g (h ((a , p) , eq₁))  ((a , p) , eq₁))
                                (cong g (JRefl  xv₁ eq₁  fiber (f (xv₁ .fst)) (xv₁ .snd)) (p , refl)))
                                eq
  -- Thm 4.7.7 (fiberwise equivalences)
  fiberEquiv : ([tf] : isEquiv total)
                 x  isEquiv (f x)
  fiberEquiv [tf] x .equiv-proof y = isContrRetract (fibers-total .Iso.inv) (fibers-total .Iso.fun) (fibers-total .Iso.rightInv)
                                                    ([tf] .equiv-proof (x , y))

  totalEquiv : (fx-equiv :  x  isEquiv (f x))
                isEquiv total
  totalEquiv fx-equiv .equiv-proof (x , v) = isContrRetract (fibers-total .Iso.fun) (fibers-total .Iso.inv) (fibers-total .Iso.leftInv)
                                                            (fx-equiv x .equiv-proof v)


module _ {U : Type } (_~_ : U  U  Type ℓ')
         (idTo~ :  {A B}  A  B  A ~ B)
         (c :  A  ∃![ X  U ] (A ~ X))
       where

  isContrToUniv :  {A B}  isEquiv (idTo~ {A} {B})
  isContrToUniv {A} {B}
    = fiberEquiv  z  A  z)  z  A ~ z) (\ B  idTo~ {A} {B})
                  { .equiv-proof y
                     isContrΣ (isContrSingl _)
                                   \ a  isContr→isContrPath (c A) _ _
                    })
                 B


{-
  The following is called fundamental theorem of identity types in Egbert Rijke's
  introduction to homotopy type theory.
-}
recognizeId : {A : Type } {a : A} (Eq : A  Type ℓ')
   Eq a
   isContr (Σ _ Eq)
   (x : A)  (a  x)  (Eq x)
recognizeId {A = A} {a = a} Eq eqRefl eqContr x = (fiberMap x) , (isEquivFiberMap x)
  where
    fiberMap : (x : A)  a  x  Eq x
    fiberMap x = J  x p  Eq x) eqRefl

    mapOnSigma : Σ[ x  A ] a  x  Σ _ Eq
    mapOnSigma pair = fst pair , fiberMap (fst pair) (snd pair)

    equivOnSigma : (x : A)  isEquiv mapOnSigma
    equivOnSigma x = isEquivFromIsContr mapOnSigma (isContrSingl a) eqContr

    isEquivFiberMap : (x : A)  isEquiv (fiberMap x)
    isEquivFiberMap = fiberEquiv  x  a  x) Eq fiberMap (equivOnSigma x)

fundamentalTheoremOfId : {A : Type } (Eq : A  A  Type ℓ')
   ((x : A)  Eq x x)
   ((x : A)  isContr (Σ[ y  A ] Eq x y))
   (x y : A)  (x  y)  (Eq x y)
fundamentalTheoremOfId Eq eqRefl eqContr x = recognizeId (Eq x) (eqRefl x) (eqContr x)