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