open import 1Lab.HLevel.Retracts
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.Equiv.Fibrewise where

Fibrewise Equivalences🔗

In HoTT, a type family P : A → Type can be seen as a fibration with total space Σ P, with the fibration being the projection fst. Because of this, a function with type (X : _) → P x → Q x can be referred as a fibrewise map.

A function like this can be lifted to a function on total spaces:

total : ((x : A)  P x  Q x)
       Σ P  Σ Q
total f (x , y) = x , f x y

Furthermore, the fibres of total f correspond to fibres of f, in the following manner:

total-fibres : {f : (x : A)  P x  Q x} {x : A} {v : Q x}
              Iso (fibre (f x) v) (fibre (total f) (x , v))
total-fibres {A = A} {P = P} {Q = Q} {f = f} {x = x} {v = v} = the-iso where
  open is-iso

  to : {x : A} {v : Q x}  fibre (f x) v  fibre (total f) (x , v)
  to (v' , p) = (_ , v') , λ i  _ , p i

  from : {x : A} {v : Q x}  fibre (total f) (x , v)  fibre (f x) v
  from ((x , v) , p) =
    J  { (x , v) _  fibre (f x) v } )
      (v , refl)
      p

  the-iso : {x : A} {v : Q x}  Iso (fibre (f x) v) (fibre (total f) (x , v))
  the-iso .fst = to
  the-iso .snd .is-iso.inv = from
  the-iso .snd .is-iso.rinv ((x , v) , p) =
    J  { _ p  to (from ((x , v) , p))  ((x , v) , p) })
      (ap to (J-refl {A = Σ Q}  { (x , v) _  fibre (f x) v } ) (v , refl)))
      p
  the-iso .snd .is-iso.linv (v , p) =
    J  { _ p  from (to (v , p))  (v , p) })
      (J-refl {A = Σ Q}  { (x , v) _  fibre (f x) v } ) (v , refl))
      p

From this, we immediately get that a fibrewise transformation is an equivalence iff. it induces an equivalence of total spaces by total.

total→equiv : {f : (x : A)  P x  Q x}
             is-equiv (total f)
             {x : A}  is-equiv (f x)
total→equiv eqv {x} .is-eqv y =
  iso→is-hlevel 0 (total-fibres .snd .is-iso.inv)
                  (is-iso.inverse (total-fibres .snd))
                  (eqv .is-eqv (x , y))

equiv→total : {f : (x : A)  P x  Q x}
             ({x : A}  is-equiv (f x))
             is-equiv (total f)
equiv→total always-eqv .is-eqv y =
  iso→is-hlevel 0
    (total-fibres .fst)
    (total-fibres .snd)
    (always-eqv .is-eqv (y .snd))