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

open import Cubical.Core.Everything
open import Cubical.Data.Prod
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Surjection
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation

private
  variable
     ℓ' : Level

module _ {A : Type } {B : Type ℓ'} (f : A  B) where
  private
    ℓ'' : Level
    ℓ'' = ℓ-max  ℓ'

    LiftA : Type ℓ''
    LiftA = Lift {j = ℓ'} A

  Total-fiber : Type ℓ''
  Total-fiber = Σ B \ b  fiber f b

  A→Total-fiber : A  Total-fiber
  A→Total-fiber a = f a , a , refl

  Total-fiber→A : Total-fiber  A
  Total-fiber→A (b , a , p) = a

  Total-fiber→A→Total-fiber :  t  A→Total-fiber (Total-fiber→A t)  t
  Total-fiber→A→Total-fiber (b , a , p) i = p i , a , λ j  p (i  j)

  A→Total-fiber→A :  a  Total-fiber→A (A→Total-fiber a)  a
  A→Total-fiber→A a = refl

  LiftA→Total-fiber : LiftA  Total-fiber
  LiftA→Total-fiber x = A→Total-fiber (lower x)

  Total-fiber→LiftA : Total-fiber  LiftA
  Total-fiber→LiftA x = lift (Total-fiber→A x)

  Total-fiber→LiftA→Total-fiber :  t  LiftA→Total-fiber (Total-fiber→LiftA t)  t
  Total-fiber→LiftA→Total-fiber (b , a , p) i = p i , a , λ j  p (i  j)

  LiftA→Total-fiber→LiftA :  a  Total-fiber→LiftA (LiftA→Total-fiber a)  a
  LiftA→Total-fiber→LiftA a = refl

  A≡Total : Lift A  Total-fiber
  A≡Total = isoToPath (iso
    LiftA→Total-fiber
    Total-fiber→LiftA
    Total-fiber→LiftA→Total-fiber
    LiftA→Total-fiber→LiftA)

  -- HoTT Lemma 4.8.2
  A≃Total : Lift A  Total-fiber
  A≃Total = isoToEquiv (iso
    LiftA→Total-fiber
    Total-fiber→LiftA
    Total-fiber→LiftA→Total-fiber
    LiftA→Total-fiber→LiftA)