Fibered equivalences
module foundation.fibered-equivalences where
Imports
open import foundation.embeddings open import foundation.equivalences open import foundation.fibered-maps open import foundation.pullbacks open import foundation.slice open import foundation-core.cartesian-product-types open import foundation-core.dependent-pair-types open import foundation-core.fibers-of-maps open import foundation-core.functions open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes open import foundation-core.universe-levels
Idea
A fibered equivalence is a fibered map
h
A -------> B
| |
f| |g
| |
V V
X -------> Y
i
such that both i and h are equivalences.
Definition
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) where equiv-over : (X → Y) → UU (l1 ⊔ l2 ⊔ l4) equiv-over i = Σ (A ≃ B) (is-map-over f g i ∘ map-equiv) fibered-equiv : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) fibered-equiv = Σ (X ≃ Y) (equiv-over ∘ map-equiv) fiberwise-equiv-over : (X → Y) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) fiberwise-equiv-over i = Σ (fiberwise-map-over f g i) (is-fiberwise-equiv) fam-equiv-over : (X → Y) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) fam-equiv-over i = (x : X) → (fib f x) ≃ (fib g (i x))
Properties
The induced maps on fibers are equivalences
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) (i : X → Y) where eq-equiv-over-equiv-slice : equiv-slice (i ∘ f) g ＝ equiv-over f g i eq-equiv-over-equiv-slice = refl eq-equiv-slice-equiv-over : equiv-over f g i ＝ equiv-slice (i ∘ f) g eq-equiv-slice-equiv-over = refl equiv-equiv-over-fiberwise-equiv : fiberwise-equiv (fib (i ∘ f)) (fib g) ≃ equiv-over f g i equiv-equiv-over-fiberwise-equiv = equiv-equiv-slice-fiberwise-equiv (i ∘ f) g
Fibered equivalences embed into the type of fibered maps
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) (i : X → Y) where map-Σ-is-equiv-equiv-over : (equiv-over f g i) → Σ (map-over f g i) (is-equiv ∘ pr1) pr1 (pr1 (map-Σ-is-equiv-equiv-over ((h , is-equiv-h) , H))) = h pr2 (pr1 (map-Σ-is-equiv-equiv-over ((h , is-equiv-h) , H))) = H pr2 (map-Σ-is-equiv-equiv-over ((h , is-equiv-h) , H)) = is-equiv-h map-equiv-over-Σ-is-equiv : Σ (map-over f g i) (is-equiv ∘ pr1) → (equiv-over f g i) pr1 (pr1 (map-equiv-over-Σ-is-equiv ((h , H) , is-equiv-h))) = h pr2 (pr1 (map-equiv-over-Σ-is-equiv ((h , H) , is-equiv-h))) = is-equiv-h pr2 (map-equiv-over-Σ-is-equiv ((h , H) , is-equiv-h)) = H is-equiv-map-Σ-is-equiv-equiv-over : is-equiv map-Σ-is-equiv-equiv-over is-equiv-map-Σ-is-equiv-equiv-over = is-equiv-has-inverse map-equiv-over-Σ-is-equiv refl-htpy refl-htpy equiv-Σ-is-equiv-equiv-over : (equiv-over f g i) ≃ Σ (map-over f g i) (is-equiv ∘ pr1) pr1 equiv-Σ-is-equiv-equiv-over = map-Σ-is-equiv-equiv-over pr2 equiv-Σ-is-equiv-equiv-over = is-equiv-map-Σ-is-equiv-equiv-over is-equiv-map-equiv-over-Σ-is-equiv : is-equiv map-equiv-over-Σ-is-equiv is-equiv-map-equiv-over-Σ-is-equiv = is-equiv-has-inverse map-Σ-is-equiv-equiv-over refl-htpy refl-htpy equiv-equiv-over-Σ-is-equiv : Σ (map-over f g i) (is-equiv ∘ pr1) ≃ (equiv-over f g i) pr1 equiv-equiv-over-Σ-is-equiv = map-equiv-over-Σ-is-equiv pr2 equiv-equiv-over-Σ-is-equiv = is-equiv-map-equiv-over-Σ-is-equiv emb-map-over-equiv-over : equiv-over f g i ↪ map-over f g i emb-map-over-equiv-over = comp-emb ( emb-subtype (is-equiv-Prop ∘ pr1)) ( emb-equiv equiv-Σ-is-equiv-equiv-over) map-emb-map-over-equiv-over : equiv-over f g i → map-over f g i map-emb-map-over-equiv-over = map-emb emb-map-over-equiv-over module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) where is-fibered-equiv-fibered-map : fibered-map f g → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-fibered-equiv-fibered-map (i , h , H) = is-equiv i × is-equiv h map-Σ-is-fibered-equiv-fibered-map-fibered-equiv : (fibered-equiv f g) → Σ (fibered-map f g) (is-fibered-equiv-fibered-map) pr1 (pr1 (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv ((i , is-equiv-i) , (h , is-equiv-h) , H))) = i pr1 (pr2 (pr1 (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv ((i , is-equiv-i) , (h , is-equiv-h) , H)))) = h pr2 (pr2 (pr1 (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv ((i , is-equiv-i) , (h , is-equiv-h) , H)))) = H pr1 (pr2 (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv ((i , is-equiv-i) , (h , is-equiv-h) , H))) = is-equiv-i pr2 (pr2 (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv ((i , is-equiv-i) , (h , is-equiv-h) , H))) = is-equiv-h map-fibered-equiv-Σ-is-fibered-equiv-fibered-map : (Σ (fibered-map f g) (is-fibered-equiv-fibered-map)) → (fibered-equiv f g) pr1 (pr1 (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map ((i , h , H) , is-equiv-i , is-equiv-h))) = i pr2 (pr1 (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map ((i , h , H) , is-equiv-i , is-equiv-h))) = is-equiv-i pr1 (pr1 (pr2 (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map ((i , h , H) , is-equiv-i , is-equiv-h)))) = h pr2 (pr1 (pr2 (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map ((i , h , H) , is-equiv-i , is-equiv-h)))) = is-equiv-h pr2 (pr2 (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map ((i , h , H) , is-equiv-i , is-equiv-h))) = H is-equiv-map-Σ-is-fibered-equiv-fibered-map-fibered-equiv : is-equiv (map-Σ-is-fibered-equiv-fibered-map-fibered-equiv) is-equiv-map-Σ-is-fibered-equiv-fibered-map-fibered-equiv = is-equiv-has-inverse ( map-fibered-equiv-Σ-is-fibered-equiv-fibered-map) ( refl-htpy) ( refl-htpy) equiv-Σ-is-fibered-equiv-fibered-map-fibered-equiv : (fibered-equiv f g) ≃ Σ (fibered-map f g) (is-fibered-equiv-fibered-map) pr1 equiv-Σ-is-fibered-equiv-fibered-map-fibered-equiv = map-Σ-is-fibered-equiv-fibered-map-fibered-equiv pr2 equiv-Σ-is-fibered-equiv-fibered-map-fibered-equiv = is-equiv-map-Σ-is-fibered-equiv-fibered-map-fibered-equiv is-equiv-map-fibered-equiv-Σ-is-fibered-equiv-fibered-map : is-equiv (map-fibered-equiv-Σ-is-fibered-equiv-fibered-map) is-equiv-map-fibered-equiv-Σ-is-fibered-equiv-fibered-map = is-equiv-has-inverse ( map-Σ-is-fibered-equiv-fibered-map-fibered-equiv) ( refl-htpy) ( refl-htpy) equiv-fibered-equiv-Σ-is-fibered-equiv-fibered-map : Σ (fibered-map f g) (is-fibered-equiv-fibered-map) ≃ (fibered-equiv f g) pr1 equiv-fibered-equiv-Σ-is-fibered-equiv-fibered-map = map-fibered-equiv-Σ-is-fibered-equiv-fibered-map pr2 equiv-fibered-equiv-Σ-is-fibered-equiv-fibered-map = is-equiv-map-fibered-equiv-Σ-is-fibered-equiv-fibered-map is-prop-is-fibered-equiv-fibered-map : (ihH : fibered-map f g) → is-prop (is-fibered-equiv-fibered-map ihH) is-prop-is-fibered-equiv-fibered-map (i , h , H) = is-prop-prod (is-property-is-equiv i) (is-property-is-equiv h) is-fibered-equiv-fibered-map-Prop : fibered-map f g → Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4) pr1 (is-fibered-equiv-fibered-map-Prop ihH) = is-fibered-equiv-fibered-map ihH pr2 (is-fibered-equiv-fibered-map-Prop ihH) = is-prop-is-fibered-equiv-fibered-map ihH emb-fibered-map-fibered-equiv : fibered-equiv f g ↪ fibered-map f g emb-fibered-map-fibered-equiv = comp-emb ( emb-subtype is-fibered-equiv-fibered-map-Prop) ( emb-equiv equiv-Σ-is-fibered-equiv-fibered-map-fibered-equiv) map-fibered-map-fibered-equiv : fibered-equiv f g → fibered-map f g map-fibered-map-fibered-equiv = map-emb emb-fibered-map-fibered-equiv
Fibered equivalences are pullback squares
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) (ihH : fibered-map f g) where is-fibered-equiv-is-pullback : is-equiv (pr1 ihH) → is-pullback (pr1 ihH) g (cone-fibered-map f g ihH) → is-fibered-equiv-fibered-map f g ihH pr1 (is-fibered-equiv-is-pullback is-equiv-i pb) = is-equiv-i pr2 (is-fibered-equiv-is-pullback is-equiv-i pb) = is-equiv-is-pullback' (pr1 ihH) g (cone-fibered-map f g ihH) is-equiv-i pb is-pullback-is-fibered-equiv : is-fibered-equiv-fibered-map f g ihH → is-pullback (pr1 ihH) g (cone-fibered-map f g ihH) is-pullback-is-fibered-equiv (is-equiv-i , is-equiv-h) = is-pullback-is-equiv' (pr1 ihH) g (cone-fibered-map f g ihH) is-equiv-i is-equiv-h equiv-is-fibered-equiv-is-pullback : is-equiv (pr1 ihH) → is-pullback (pr1 ihH) g (cone-fibered-map f g ihH) ≃ is-fibered-equiv-fibered-map f g ihH equiv-is-fibered-equiv-is-pullback is-equiv-i = equiv-prop ( is-property-is-pullback (pr1 ihH) g (cone-fibered-map f g ihH)) ( is-prop-is-fibered-equiv-fibered-map f g ihH) ( is-fibered-equiv-is-pullback is-equiv-i) ( is-pullback-is-fibered-equiv) equiv-is-pullback-is-fibered-equiv : is-equiv (pr1 ihH) → is-fibered-equiv-fibered-map f g ihH ≃ is-pullback (pr1 ihH) g (cone-fibered-map f g ihH) equiv-is-pullback-is-fibered-equiv is-equiv-i = inv-equiv (equiv-is-fibered-equiv-is-pullback is-equiv-i) fibered-equiv-is-pullback : is-equiv (pr1 ihH) → is-pullback (pr1 ihH) g (cone-fibered-map f g ihH) → fibered-equiv f g pr1 (pr1 (fibered-equiv-is-pullback is-equiv-i pb)) = pr1 ihH pr2 (pr1 (fibered-equiv-is-pullback is-equiv-i pb)) = is-equiv-i pr1 (pr1 (pr2 (fibered-equiv-is-pullback is-equiv-i pb))) = pr1 (pr2 ihH) pr2 (pr1 (pr2 (fibered-equiv-is-pullback is-equiv-i pb))) = pr2 (is-fibered-equiv-is-pullback is-equiv-i pb) pr2 (pr2 (fibered-equiv-is-pullback is-equiv-i pb)) = pr2 (pr2 ihH) is-pullback-fibered-equiv : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → X) (g : B → Y) (e : fibered-equiv f g) → is-pullback ( pr1 (pr1 e)) ( g) ( cone-fibered-map f g (map-fibered-map-fibered-equiv f g e)) is-pullback-fibered-equiv f g ((i , is-equiv-i) , (h , is-equiv-h) , H) = is-pullback-is-fibered-equiv f g (i , h , H) (is-equiv-i , is-equiv-h)
Examples
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where self-fibered-equiv : A ≃ B → fibered-equiv id id pr1 (self-fibered-equiv e) = e pr1 (pr2 (self-fibered-equiv e)) = e pr2 (pr2 (self-fibered-equiv e)) = refl-htpy id-fibered-equiv : (f : A → B) → fibered-equiv f f pr1 (id-fibered-equiv f) = id-equiv pr1 (pr2 (id-fibered-equiv f)) = id-equiv pr2 (pr2 (id-fibered-equiv f)) = refl-htpy id-fibered-equiv-htpy : (f g : A → B) → f ~ g → fibered-equiv f g pr1 (id-fibered-equiv-htpy f g H) = id-equiv pr1 (pr2 (id-fibered-equiv-htpy f g H)) = id-equiv pr2 (pr2 (id-fibered-equiv-htpy f g H)) = H