{-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.Functions.Fibration where open import Cubical.Foundations.Prelude open import Cubical.Foundations.HLevels using (isOfHLevel→isOfHLevelDep) open import Cubical.Foundations.Function open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.Properties open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Path open import Cubical.Foundations.Univalence open import Cubical.Foundations.Transport open import Cubical.Data.Sigma private variable ℓ ℓb : Level B : Type ℓb module FiberIso {ℓ} (p⁻¹ : B → Type ℓ) (x : B) where p : Σ B p⁻¹ → B p = fst fwd : fiber p x → p⁻¹ x fwd ((x' , y) , q) = subst (λ z → p⁻¹ z) q y bwd : p⁻¹ x → fiber p x bwd y = (x , y) , refl fwd-bwd : ∀ x → fwd (bwd x) ≡ x fwd-bwd y = transportRefl y bwd-fwd : ∀ x → bwd (fwd x) ≡ x bwd-fwd ((x' , y) , q) i = h (r i) where h : Σ[ s ∈ singl x ] p⁻¹ (s .fst) → fiber p x h ((x , p) , y) = (x , y) , sym p r : Path (Σ[ s ∈ singl x ] p⁻¹ (s .fst)) ((x , refl ) , subst p⁻¹ q y) ((x' , sym q) , y ) r = ΣPathP (isContrSingl x .snd (x' , sym q) , toPathP (transport⁻Transport (λ i → p⁻¹ (q i)) y)) -- HoTT Lemma 4.8.1 fiberEquiv : fiber p x ≃ p⁻¹ x fiberEquiv = isoToEquiv (iso fwd bwd fwd-bwd bwd-fwd) open FiberIso using (fiberEquiv) public module _ {ℓ} {E : Type ℓ} (p : E → B) where -- HoTT Lemma 4.8.2 totalEquiv : E ≃ Σ B (fiber p) totalEquiv = isoToEquiv isom where isom : Iso E (Σ B (fiber p)) Iso.fun isom x = p x , x , refl Iso.inv isom (b , x , q) = x Iso.leftInv isom x i = x Iso.rightInv isom (b , x , q) i = q i , x , λ j → q (i ∧ j) module _ (B : Type ℓb) (ℓ : Level) where private ℓ' = ℓ-max ℓb ℓ -- HoTT Theorem 4.8.3 fibrationEquiv : (Σ[ E ∈ Type ℓ' ] (E → B)) ≃ (B → Type ℓ') fibrationEquiv = isoToEquiv isom where isom : Iso (Σ[ E ∈ Type ℓ' ] (E → B)) (B → Type ℓ') Iso.fun isom (E , p) = fiber p Iso.inv isom p⁻¹ = Σ B p⁻¹ , fst Iso.rightInv isom p⁻¹ i x = ua (fiberEquiv p⁻¹ x) i Iso.leftInv isom (E , p) i = ua e (~ i) , fst ∘ ua-unglue e (~ i) where e = totalEquiv p module ForSets {E : Type ℓ} {isSetB : isSet B} (f : E → B) where module _ {x x'} {px : x ≡ x'} {a' : fiber f x} {b' : fiber f x'} where -- fibers are equal when their representatives are equal fibersEqIfRepsEq : fst a' ≡ fst b' → PathP (λ i → fiber f (px i)) a' b' fibersEqIfRepsEq p = ΣPathP (p , (isOfHLevel→isOfHLevelDep 1 (λ (v , w) → isSetB (f v) w) (snd a') (snd b') (λ i → (p i , px i)))) -- The path type in a fiber of f is equivalent to a fiber of (cong f) open import Cubical.Foundations.Function fiberPath : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {b : B} (h h' : fiber f b) → (Σ[ p ∈ (fst h ≡ fst h') ] (PathP (λ i → f (p i) ≡ b) (snd h) (snd h'))) ≡ fiber (cong f) (h .snd ∙∙ refl ∙∙ sym (h' .snd)) fiberPath h h' = cong (Σ (h .fst ≡ h' .fst)) (funExt λ p → flipSquarePath ∙ PathP≡doubleCompPathʳ _ _ _ _) fiber≡ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {b : B} (h h' : fiber f b) → (h ≡ h') ≡ fiber (cong f) (h .snd ∙∙ refl ∙∙ sym (h' .snd)) fiber≡ {f = f} {b = b} h h' = ΣPath≡PathΣ ⁻¹ ∙ fiberPath h h' FibrationStr : (B : Type ℓb) → Type ℓ → Type (ℓ-max ℓ ℓb) FibrationStr B A = A → B Fibration : (B : Type ℓb) → (ℓ : Level) → Type (ℓ-max ℓb (ℓ-suc ℓ)) Fibration {ℓb = ℓb} B ℓ = Σ[ A ∈ Type ℓ ] FibrationStr B A