{-# 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)