Martin Escardo, 2012- Expanded on demand whenever a general equivalence is needed. \begin{code} {-# OPTIONS --safe --without-K #-} open import MLTT.Plus-Properties open import MLTT.Spartan open import MLTT.Two-Properties open import UF.Base open import UF.Equiv open import UF.FunExt open import UF.Lower-FunExt open import UF.PropIndexedPiSigma open import UF.Retracts open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.Subsingletons-Properties module UF.EquivalenceExamples where curry-uncurry' : funext 𝓤 (𝓥 ⊔ 𝓦) → funext (𝓤 ⊔ 𝓥) 𝓦 → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Z : (Σ x ꞉ X , Y x) → 𝓦 ̇ } → Π Z ≃ (Π x ꞉ X , Π y ꞉ Y x , Z (x , y)) curry-uncurry' {𝓤} {𝓥} {𝓦} fe fe' {X} {Y} {Z} = qinveq c (u , uc , cu) where c : (w : Π Z) → ((x : X) (y : Y x) → Z (x , y)) c f x y = f (x , y) u : ((x : X) (y : Y x) → Z (x , y)) → Π Z u g (x , y) = g x y cu : ∀ g → c (u g) = g cu g = dfunext fe (λ x → dfunext (lower-funext 𝓤 𝓦 fe') (λ y → refl)) uc : ∀ f → u (c f) = f uc f = dfunext fe' (λ w → refl) curry-uncurry : (fe : FunExt) → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Z : (Σ x ꞉ X , Y x) → 𝓦 ̇ } → Π Z ≃ (Π x ꞉ X , Π y ꞉ Y x , Z (x , y)) curry-uncurry {𝓤} {𝓥} {𝓦} fe = curry-uncurry' (fe 𝓤 (𝓥 ⊔ 𝓦)) (fe (𝓤 ⊔ 𝓥) 𝓦) Σ-=-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {σ τ : Σ A} → (σ = τ) ≃ (Σ p ꞉ pr₁ σ = pr₁ τ , transport A p (pr₂ σ) = pr₂ τ) Σ-=-≃ {𝓤} {𝓥} {X} {A} {x , a} {y , b} = qinveq from-Σ-= (to-Σ-= , ε , η) where η : (σ : Σ p ꞉ x = y , transport A p a = b) → from-Σ-= (to-Σ-= σ) = σ η (refl , refl) = refl ε : (q : x , a = y , b) → to-Σ-= (from-Σ-= q) = q ε refl = refl ×-=-≃ : {X : 𝓤 ̇ } {A : 𝓥 ̇ } {σ τ : X × A} → (σ = τ) ≃ (pr₁ σ = pr₁ τ) × (pr₂ σ = pr₂ τ) ×-=-≃ {𝓤} {𝓥} {X} {A} {x , a} {y , b} = qinveq from-×-=' (to-×-=' , (ε , η)) where η : (t : (x = y) × (a = b)) → from-×-=' (to-×-=' t) = t η (refl , refl) = refl ε : (u : x , a = y , b) → to-×-=' (from-×-=' u) = u ε refl = refl Σ-assoc : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Z : Σ Y → 𝓦 ̇ } → Σ Z ≃ (Σ x ꞉ X , Σ y ꞉ Y x , Z (x , y)) Σ-assoc {𝓤} {𝓥} {𝓦} {X} {Y} {Z} = qinveq c (u , (λ τ → refl) , (λ σ → refl)) where c : Σ Z → Σ x ꞉ X , Σ y ꞉ Y x , Z (x , y) c ((x , y) , z) = (x , (y , z)) u : (Σ x ꞉ X , Σ y ꞉ Y x , Z (x , y)) → Σ Z u (x , (y , z)) = ((x , y) , z) Σ-flip : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : X → Y → 𝓦 ̇ } → (Σ x ꞉ X , Σ y ꞉ Y , A x y) ≃ (Σ y ꞉ Y , Σ x ꞉ X , A x y) Σ-flip {𝓤} {𝓥} {𝓦} {X} {Y} {A} = qinveq f (g , ε , η) where f : (Σ x ꞉ X , Σ y ꞉ Y , A x y) → (Σ y ꞉ Y , Σ x ꞉ X , A x y) f (x , y , p) = y , x , p g : (Σ y ꞉ Y , Σ x ꞉ X , A x y) → (Σ x ꞉ X , Σ y ꞉ Y , A x y) g (y , x , p) = x , y , p ε : ∀ σ → g (f σ) = σ ε (x , y , p) = refl η : ∀ τ → f (g τ) = τ η (y , x , p) = refl Σ-interchange : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : X → 𝓦 ̇ } {B : Y → 𝓣 ̇ } → (Σ x ꞉ X , Σ y ꞉ Y , A x × B y) ≃ ((Σ x ꞉ X , A x) × (Σ y ꞉ Y , B y)) Σ-interchange {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} {A} {B} = qinveq f (g , ε , η) where f : (Σ x ꞉ X , Σ y ꞉ Y , A x × B y) → ((Σ x ꞉ X , A x) × (Σ y ꞉ Y , B y)) f (x , y , a , b) = ((x , a) , (y , b)) g : codomain f → domain f g ((x , a) , (y , b)) = (x , y , a , b) ε : ∀ σ → g (f σ) = σ ε (x , y , a , b) = refl η : ∀ τ → f (g τ) = τ η ((x , a) , (y , b)) = refl Σ-cong : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Y' : X → 𝓦 ̇ } → ((x : X) → Y x ≃ Y' x) → Σ Y ≃ Σ Y' Σ-cong {𝓤} {𝓥} {𝓦} {X} {Y} {Y'} φ = qinveq f (g , gf , fg) where f : Σ Y → Σ Y' f (x , y) = x , ⌜ φ x ⌝ y g : Σ Y' → Σ Y g (x , y') = x , ⌜ φ x ⌝⁻¹ y' fg : (w' : Σ Y') → f (g w') = w' fg (x , y') = to-Σ-=' (inverses-are-sections ⌜ φ x ⌝ ⌜ φ x ⌝-is-equiv y') gf : (w : Σ Y) → g (f w) = w gf (x , y) = to-Σ-=' (inverses-are-retractions ⌜ φ x ⌝ ⌜ φ x ⌝-is-equiv y) ΠΣ-distr-≃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {P : (x : X) → A x → 𝓦 ̇ } → (Π x ꞉ X , Σ a ꞉ A x , P x a) ≃ (Σ f ꞉ Π A , Π x ꞉ X , P x (f x)) ΠΣ-distr-≃ = qinveq ΠΣ-distr (ΠΣ-distr⁻¹ , (λ _ → refl) , (λ _ → refl)) Π×-distr : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ } → (Π x ꞉ X , A x × B x) ≃ ((Π x ꞉ X , A x) × (Π x ꞉ X , B x)) Π×-distr = ΠΣ-distr-≃ Π×-distr₂ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : X → Y → 𝓦 ̇ } {B : X → Y → 𝓣 ̇ } → (Π x ꞉ X , Π y ꞉ Y , A x y × B x y) ≃ ((Π x ꞉ X , Π y ꞉ Y , A x y) × (Π x ꞉ X , Π y ꞉ Y , B x y)) Π×-distr₂ = qinveq (λ f → (λ x y → pr₁ (f x y)) , (λ x y → pr₂ (f x y))) ((λ (g , h) x y → g x y , h x y) , (λ _ → refl) , (λ _ → refl)) Σ+-distr : (X : 𝓤 ̇ ) (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) → (Σ x ꞉ X , A x + B x) ≃ ((Σ x ꞉ X , A x) + (Σ x ꞉ X , B x)) Σ+-distr X A B = qinveq f (g , η , ε) where f : (Σ x ꞉ X , A x + B x) → (Σ x ꞉ X , A x) + (Σ x ꞉ X , B x) f (x , inl a) = inl (x , a) f (x , inr b) = inr (x , b) g : ((Σ x ꞉ X , A x) + (Σ x ꞉ X , B x)) → (Σ x ꞉ X , A x + B x) g (inl (x , a)) = x , inl a g (inr (x , b)) = x , inr b η : g ∘ f ∼ id η (x , inl a) = refl η (x , inr b) = refl ε : f ∘ g ∼ id ε (inl (x , a)) = refl ε (inr (x , b)) = refl Σ+-split : (X : 𝓤 ̇ ) (Y : 𝓥 ̇ ) (A : X + Y → 𝓦 ̇ ) → (Σ x ꞉ X , A (inl x)) + (Σ y ꞉ Y , A (inr y)) ≃ (Σ z ꞉ X + Y , A z) Σ+-split X Y A = qinveq f (g , η , ε) where f : (Σ x ꞉ X , A (inl x)) + (Σ y ꞉ Y , A (inr y)) → (Σ z ꞉ X + Y , A z) f (inl (x , a)) = inl x , a f (inr (y , a)) = inr y , a g : (Σ z ꞉ X + Y , A z) → (Σ x ꞉ X , A (inl x)) + (Σ y ꞉ Y , A (inr y)) g (inl x , a) = inl (x , a) g (inr y , a) = inr (y , a) η : g ∘ f ∼ id η (inl _) = refl η (inr _) = refl ε : f ∘ g ∼ id ε (inl _ , _) = refl ε (inr _ , _) = refl Π-cong : funext 𝓤 𝓥 → funext 𝓤 𝓦 → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Y' : X → 𝓦 ̇ } → ((x : X) → Y x ≃ Y' x) → Π Y ≃ Π Y' Π-cong fe fe' {X} {Y} {Y'} φ = qinveq f (g , gf , fg) where f : ((x : X) → Y x) → ((x : X) → Y' x) f h x = ⌜ φ x ⌝ (h x) g : ((x : X) → Y' x) → (x : X) → Y x g k x = ⌜ φ x ⌝⁻¹ (k x) fg : (k : ((x : X) → Y' x)) → f (g k) = k fg k = dfunext fe' (λ x → inverses-are-sections ⌜ φ x ⌝ ⌜ φ x ⌝-is-equiv (k x)) gf : (h : ((x : X) → Y x)) → g (f h) = h gf h = dfunext fe (λ x → inverses-are-retractions ⌜ φ x ⌝ ⌜ φ x ⌝-is-equiv (h x)) \end{code} An application of Π-cong is the following: \begin{code} ≃-funext₂ : funext 𝓤 (𝓥 ⊔ 𝓦) → funext 𝓥 𝓦 → {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {A : (x : X) → Y x → 𝓦 ̇ } (f g : (x : X) (y : Y x) → A x y) → (f = g) ≃ (∀ x y → f x y = g x y) ≃-funext₂ fe fe' {X} f g = (f = g) ≃⟨ ≃-funext fe f g ⟩ (f ∼ g) ≃⟨ Π-cong fe fe (λ x → ≃-funext fe' (f x) (g x)) ⟩ (∀ x → f x ∼ g x) ■ 𝟙-lneutral : {Y : 𝓤 ̇ } → 𝟙 {𝓥} × Y ≃ Y 𝟙-lneutral {𝓤} {𝓥} {Y} = qinveq f (g , ε , η) where f : 𝟙 × Y → Y f (o , y) = y g : Y → 𝟙 × Y g y = (⋆ , y) η : ∀ x → f (g x) = x η y = refl ε : ∀ z → g (f z) = z ε (o , y) = ap (_, y) (𝟙-is-prop ⋆ o) ×-comm : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X × Y ≃ Y × X ×-comm {𝓤} {𝓥} {X} {Y} = qinveq f (g , ε , η) where f : X × Y → Y × X f (x , y) = (y , x) g : Y × X → X × Y g (y , x) = (x , y) η : ∀ z → f (g z) = z η z = refl ε : ∀ t → g (f t) = t ε t = refl 𝟙-rneutral : {Y : 𝓤 ̇ } → Y × 𝟙 {𝓥} ≃ Y 𝟙-rneutral {𝓤} {𝓥} {Y} = Y × 𝟙 ≃⟨ ×-comm ⟩ 𝟙 × Y ≃⟨ 𝟙-lneutral {𝓤} {𝓥} ⟩ Y ■ +comm : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X + Y ≃ Y + X +comm {𝓤} {𝓥} {X} {Y} = qinveq f (g , η , ε) where f : X + Y → Y + X f (inl x) = inr x f (inr y) = inl y g : Y + X → X + Y g (inl y) = inr y g (inr x) = inl x ε : (t : Y + X) → (f ∘ g) t = t ε (inl y) = refl ε (inr x) = refl η : (u : X + Y) → (g ∘ f) u = u η (inl x) = refl η (inr y) = refl one-𝟘-only : 𝟘 {𝓤} ≃ 𝟘 {𝓥} one-𝟘-only = qinveq 𝟘-elim (𝟘-elim , 𝟘-induction , 𝟘-induction) one-𝟙-only : {𝓤 𝓥 : Universe} → 𝟙 {𝓤} ≃ 𝟙 {𝓥} one-𝟙-only = qinveq unique-to-𝟙 (unique-to-𝟙 , (λ ⋆ → refl) , (λ ⋆ → refl)) 𝟘-rneutral : {X : 𝓤 ̇ } → X ≃ X + 𝟘 {𝓥} 𝟘-rneutral {𝓤} {𝓥} {X} = qinveq f (g , η , ε) where f : X → X + 𝟘 f = inl g : X + 𝟘 → X g (inl x) = x g (inr y) = 𝟘-elim y ε : (y : X + 𝟘) → (f ∘ g) y = y ε (inl x) = refl ε (inr y) = 𝟘-elim y η : (x : X) → (g ∘ f) x = x η x = refl 𝟘-rneutral' : {X : 𝓤 ̇ } → X + 𝟘 {𝓥} ≃ X 𝟘-rneutral' = ≃-sym 𝟘-rneutral 𝟘-lneutral : {X : 𝓤 ̇ } → 𝟘 {𝓥} + X ≃ X 𝟘-lneutral {𝓤} {𝓥} {X} = (𝟘 + X) ≃⟨ +comm ⟩ (X + 𝟘) ≃⟨ 𝟘-rneutral' {𝓤} {𝓥} ⟩ X ■ 𝟘-lneutral' : {X : 𝓤 ̇ } → X ≃ 𝟘 {𝓥} + X 𝟘-lneutral' = ≃-sym 𝟘-lneutral 𝟘-lneutral'' : 𝟙 {𝓤} ≃ 𝟘 {𝓥} + 𝟙 {𝓦} 𝟘-lneutral'' {𝓤} {𝓥} {𝓦} = 𝟙 {𝓤} ≃⟨ one-𝟙-only ⟩ 𝟙 {𝓦} ≃⟨ 𝟘-lneutral' ⟩ (𝟘 {𝓥} + 𝟙 {𝓦}) ■ +assoc : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } → (X + Y) + Z ≃ X + (Y + Z) +assoc {𝓤} {𝓥} {𝓦} {X} {Y} {Z} = qinveq f (g , η , ε) where f : (X + Y) + Z → X + (Y + Z) f (inl (inl x)) = inl x f (inl (inr y)) = inr (inl y) f (inr z) = inr (inr z) g : X + (Y + Z) → (X + Y) + Z g (inl x) = inl (inl x) g (inr (inl y)) = inl (inr y) g (inr (inr z)) = inr z ε : (t : X + (Y + Z)) → (f ∘ g) t = t ε (inl x) = refl ε (inr (inl y)) = refl ε (inr (inr z)) = refl η : (u : (X + Y) + Z) → (g ∘ f) u = u η (inl (inl x)) = refl η (inl (inr x)) = refl η (inr x) = refl +-cong : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } {B : 𝓣 ̇ } → X ≃ A → Y ≃ B → X + Y ≃ A + B +-cong f g = qinveq (+functor ⌜ f ⌝ ⌜ g ⌝) (+functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ , ε , η) where ε : +functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ ∘ +functor ⌜ f ⌝ ⌜ g ⌝ ∼ id ε (inl x) = ap inl (inverses-are-retractions ⌜ f ⌝ ⌜ f ⌝-is-equiv x) ε (inr y) = ap inr (inverses-are-retractions ⌜ g ⌝ ⌜ g ⌝-is-equiv y) η : +functor ⌜ f ⌝ ⌜ g ⌝ ∘ +functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ ∼ id η (inl a) = ap inl (inverses-are-sections ⌜ f ⌝ ⌜ f ⌝-is-equiv a) η (inr b) = ap inr (inverses-are-sections ⌜ g ⌝ ⌜ g ⌝-is-equiv b) ×𝟘 : {X : 𝓤 ̇ } → 𝟘 {𝓥} ≃ X × 𝟘 {𝓦} ×𝟘 {𝓤} {𝓥} {𝓦} {X} = qinveq unique-from-𝟘 ((λ (x , y) → 𝟘-elim y) , 𝟘-induction , (λ (x , y) → 𝟘-elim y)) 𝟙distr : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X × Y + X ≃ X × (Y + 𝟙 {𝓦}) 𝟙distr {𝓤} {𝓥} {𝓦} {X} {Y} = qinveq f (g , η , ε) where f : X × Y + X → X × (Y + 𝟙) f (inl (x , y)) = x , inl y f (inr x) = x , inr ⋆ g : X × (Y + 𝟙) → X × Y + X g (x , inl y) = inl (x , y) g (x , inr O) = inr x ε : f ∘ g ∼ id ε (x , inl y) = refl ε (x , inr ⋆) = refl η : g ∘ f ∼ id η (inl (x , y)) = refl η (inr x) = refl Ap+ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (Z : 𝓦 ̇ ) → X ≃ Y → X + Z ≃ Y + Z Ap+ {𝓤} {𝓥} {𝓦} {X} {Y} Z f = qinveq (+functor ⌜ f ⌝ id) (+functor ⌜ f ⌝⁻¹ id , η , ε) where η : +functor ⌜ f ⌝⁻¹ id ∘ +functor ⌜ f ⌝ id ∼ id η (inl x) = ap inl (inverses-are-retractions ⌜ f ⌝ ⌜ f ⌝-is-equiv x) η (inr z) = ap inr refl ε : +functor ⌜ f ⌝ id ∘ +functor ⌜ f ⌝⁻¹ id ∼ id ε (inl x) = ap inl (inverses-are-sections ⌜ f ⌝ ⌜ f ⌝-is-equiv x) ε (inr z) = ap inr refl ×comm : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X × Y ≃ Y × X ×comm {𝓤} {𝓥} {X} {Y} = qinveq (λ (x , y) → (y , x)) ((λ (y , x) → (x , y)) , (λ _ → refl) , (λ _ → refl)) ×-cong : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } {B : 𝓣 ̇ } → X ≃ A → Y ≃ B → X × Y ≃ A × B ×-cong f g = qinveq (×functor ⌜ f ⌝ ⌜ g ⌝) (×functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ , ε , η) where ε : ×functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ ∘ ×functor ⌜ f ⌝ ⌜ g ⌝ ∼ id ε (x , y) = to-×-= (inverses-are-retractions ⌜ f ⌝ ⌜ f ⌝-is-equiv x) (inverses-are-retractions ⌜ g ⌝ ⌜ g ⌝-is-equiv y) η : ×functor ⌜ f ⌝ ⌜ g ⌝ ∘ ×functor ⌜ f ⌝⁻¹ ⌜ g ⌝⁻¹ ∼ id η (a , b) = to-×-= (inverses-are-sections ⌜ f ⌝ ⌜ f ⌝-is-equiv a) (inverses-are-sections ⌜ g ⌝ ⌜ g ⌝-is-equiv b) 𝟘→ : {X : 𝓤 ̇ } → funext 𝓦 𝓤 → 𝟙 {𝓥} ≃ (𝟘 {𝓦} → X) 𝟘→ {𝓤} {𝓥} {𝓦} {X} fe = qinveq f (g , η , ε) where f : 𝟙 → (𝟘 → X) f ⋆ y = 𝟘-elim y g : (𝟘 → X) → 𝟙 g h = ⋆ ε : f ∘ g ∼ id ε h = dfunext fe (λ z → 𝟘-elim z) η : g ∘ f ∼ id η ⋆ = refl 𝟙→ : {X : 𝓤 ̇ } → funext 𝓥 𝓤 → X ≃ (𝟙 {𝓥} → X) 𝟙→ {𝓤} {𝓥} {X} fe = qinveq f (g , η , ε) where f : X → 𝟙 → X f x ⋆ = x g : (𝟙 → X) → X g h = h ⋆ ε : (h : 𝟙 → X) → f (g h) = h ε h = dfunext fe γ where γ : (t : 𝟙) → f (g h) t = h t γ ⋆ = refl η : (x : X) → g (f x) = x η x = refl →𝟙 : {X : 𝓤 ̇ } → funext 𝓤 𝓥 → (X → 𝟙 {𝓥}) ≃ 𝟙 {𝓥} →𝟙 {𝓤} {𝓥} {X} fe = qinveq f (g , ε , η) where f : (X → 𝟙) → 𝟙 f = unique-to-𝟙 g : (t : 𝟙) → X → 𝟙 g t = unique-to-𝟙 ε : (α : X → 𝟙) → g ⋆ = α ε α = dfunext fe λ (x : X) → 𝟙-is-prop (g ⋆ x) (α x) η : (t : 𝟙) → ⋆ = t η = 𝟙-is-prop ⋆ Π×+ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : X + Y → 𝓦 ̇ } → funext (𝓤 ⊔ 𝓥) 𝓦 → (Π x ꞉ X , A (inl x)) × (Π y ꞉ Y , A (inr y)) ≃ (Π z ꞉ X + Y , A z) Π×+ {𝓤} {𝓥} {𝓦} {X} {Y} {A} fe = qinveq f (g , ε , η) where f : (Π x ꞉ X , A (inl x)) × (Π y ꞉ Y , A (inr y)) → (Π z ꞉ X + Y , A z) f (l , r) (inl x) = l x f (l , r) (inr y) = r y g : (Π z ꞉ X + Y , A z) → (Π x ꞉ X , A (inl x)) × (Π y ꞉ Y , A (inr y)) g h = h ∘ inl , h ∘ inr η : f ∘ g ∼ id η h = dfunext fe γ where γ : (z : X + Y) → (f ∘ g) h z = h z γ (inl x) = refl γ (inr y) = refl ε : g ∘ f ∼ id ε (l , r) = refl +→ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } → funext (𝓤 ⊔ 𝓥) 𝓦 → (X + Y → Z) ≃ (X → Z) × (Y → Z) +→ fe = ≃-sym (Π×+ fe) →× : {A : 𝓤 ̇ } {X : A → 𝓥 ̇ } {Y : A → 𝓦 ̇ } → ((a : A) → X a × Y a) ≃ Π X × Π Y →× {𝓤} {𝓥} {𝓦} {A} {X} {Y} = qinveq f (g , ε , η) where f : ((a : A) → X a × Y a) → Π X × Π Y f φ = (λ a → pr₁ (φ a)) , (λ a → pr₂ (φ a)) g : Π X × Π Y → (a : A) → X a × Y a g (γ , δ) a = γ a , δ a ε : (φ : (a : A) → X a × Y a) → g (f φ) = φ ε φ = refl η : (α : Π X × Π Y) → f (g α) = α η (γ , δ) = refl →cong : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } {B : 𝓣 ̇ } → funext 𝓦 𝓣 → funext 𝓤 𝓥 → X ≃ A → Y ≃ B → (X → Y) ≃ (A → B) →cong {𝓤} {𝓥} {𝓦} {𝓣} {X} {Y} {A} {B} fe fe' f g = qinveq ϕ (γ , ((λ h → dfunext fe' (η h)) , (λ k → dfunext fe (ε k)))) where ϕ : (X → Y) → (A → B) ϕ h = ⌜ g ⌝ ∘ h ∘ ⌜ f ⌝⁻¹ γ : (A → B) → (X → Y) γ k = ⌜ g ⌝⁻¹ ∘ k ∘ ⌜ f ⌝ ε : (k : A → B) → ϕ (γ k) ∼ k ε k a = ⌜ g ⌝ (⌜ g ⌝⁻¹ (k (⌜ f ⌝ (⌜ f ⌝⁻¹ a)))) =⟨ I ⟩ k (⌜ f ⌝ (⌜ f ⌝⁻¹ a)) =⟨ II ⟩ k a ∎ where I = inverses-are-sections ⌜ g ⌝ ⌜ g ⌝-is-equiv _ II = ap k (inverses-are-sections ⌜ f ⌝ ⌜ f ⌝-is-equiv a) η : (h : X → Y) → γ (ϕ h) ∼ h η h x = ⌜ g ⌝⁻¹ (⌜ g ⌝ (h (⌜ f ⌝⁻¹ (⌜ f ⌝ x)))) =⟨ I ⟩ h (⌜ f ⌝⁻¹ (⌜ f ⌝ x)) =⟨ II ⟩ h x ∎ where I = inverses-are-retractions ⌜ g ⌝ ⌜ g ⌝-is-equiv _ II = ap h (inverses-are-retractions ⌜ f ⌝ ⌜ f ⌝-is-equiv x) →cong' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {B : 𝓣 ̇ } → funext 𝓤 𝓣 → funext 𝓤 𝓥 → Y ≃ B → (X → Y) ≃ (X → B) →cong' fe fe' = →cong fe fe' (≃-refl _) →cong'' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {A : 𝓦 ̇ } → funext 𝓦 𝓥 → funext 𝓤 𝓥 → X ≃ A → (X → Y) ≃ (A → Y) →cong'' fe fe' e = →cong fe fe' e (≃-refl _) pr₁-≃ : (X : 𝓤 ̇ ) (A : X → 𝓥 ̇ ) → ((x : X) → is-singleton (A x)) → (Σ x ꞉ X , A x) ≃ X pr₁-≃ X A f = pr₁ , pr₁-is-equiv X A f NatΣ-fiber-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → (x : X) (b : B x) → fiber (ζ x) b ≃ fiber (NatΣ ζ) (x , b) NatΣ-fiber-equiv A B ζ x b = qinveq (f b) (g b , ε b , η b) where f : (b : B x) → fiber (ζ x) b → fiber (NatΣ ζ) (x , b) f _ (a , refl) = (x , a) , refl g : (b : B x) → fiber (NatΣ ζ) (x , b) → fiber (ζ x) b g _ ((x , a) , refl) = a , refl ε : (b : B x) (w : fiber (ζ x) b) → g b (f b w) = w ε _ (a , refl) = refl η : (b : B x) (t : fiber (NatΣ ζ) (x , b)) → f b (g b t) = t η b (a , refl) = refl NatΣ-vv-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → ((x : X) → is-vv-equiv (ζ x)) → is-vv-equiv (NatΣ ζ) NatΣ-vv-equiv A B ζ i (x , b) = equiv-to-singleton (≃-sym (NatΣ-fiber-equiv A B ζ x b)) (i x b) NatΣ-vv-equiv-converse : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → is-vv-equiv (NatΣ ζ) → ((x : X) → is-vv-equiv (ζ x)) NatΣ-vv-equiv-converse A B ζ e x b = equiv-to-singleton (NatΣ-fiber-equiv A B ζ x b) (e (x , b)) NatΣ-is-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → ((x : X) → is-equiv (ζ x)) → is-equiv (NatΣ ζ) NatΣ-is-equiv A B ζ i = vv-equivs-are-equivs (NatΣ ζ) (NatΣ-vv-equiv A B ζ (λ x → equivs-are-vv-equivs (ζ x) (i x))) NatΣ-equiv-converse : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → is-equiv (NatΣ ζ) → ((x : X) → is-equiv (ζ x)) NatΣ-equiv-converse A B ζ e x = vv-equivs-are-equivs (ζ x) (NatΣ-vv-equiv-converse A B ζ (equivs-are-vv-equivs (NatΣ ζ) e) x) NatΣ-equiv-gives-fiberwise-equiv : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ } (φ : Nat A B) → is-equiv (NatΣ φ) → is-fiberwise-equiv φ NatΣ-equiv-gives-fiberwise-equiv = NatΣ-equiv-converse _ _ Σ-cong' : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) → ((x : X) → A x ≃ B x) → Σ A ≃ Σ B Σ-cong' A B f = NatΣ (λ x → ⌜ f x ⌝) , NatΣ-is-equiv A B (λ x → ⌜ f x ⌝) (λ x → ⌜ f x ⌝-is-equiv) Σ-change-of-variable' : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : X → 𝓦 ̇ ) (g : Y → X) → is-hae g → Σ γ ꞉ ((Σ y ꞉ Y , A (g y)) → Σ A) , qinv γ Σ-change-of-variable' {𝓤} {𝓥} {𝓦} {X} {Y} A g (f , η , ε , α) = γ , φ , φγ , γφ where γ : (Σ y ꞉ Y , A (g y)) → Σ A γ (y , a) = (g y , a) φ : Σ A → Σ y ꞉ Y , A (g y) φ (x , a) = (f x , transport⁻¹ A (ε x) a) γφ : (σ : Σ A) → γ (φ σ) = σ γφ (x , a) = to-Σ-= (ε x , p) where p : transport A (ε x) (transport⁻¹ A (ε x) a) = a p = back-and-forth-transport (ε x) φγ : (τ : (Σ y ꞉ Y , A (g y))) → φ (γ τ) = τ φγ (y , a) = to-Σ-= (η y , q) where q = transport (λ - → A (g -)) (η y) (transport⁻¹ A (ε (g y)) a) =⟨ i ⟩ transport A (ap g (η y)) (transport⁻¹ A (ε (g y)) a) =⟨ ii ⟩ transport A (ε (g y)) (transport⁻¹ A (ε (g y)) a) =⟨ iii ⟩ a ∎ where i = transport-ap A g (η y) ii = ap (λ - → transport A - (transport⁻¹ A (ε (g y)) a)) (α y) iii = back-and-forth-transport (ε (g y)) Σ-change-of-variable : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : X → 𝓦 ̇ ) (g : Y → X) → is-equiv g → (Σ y ꞉ Y , A (g y)) ≃ (Σ x ꞉ X , A x) Σ-change-of-variable {𝓤} {𝓥} {𝓦} {X} {Y} A g e = γ , qinvs-are-equivs γ q where γ : (Σ y ꞉ Y , A (g y)) → Σ A γ = pr₁ (Σ-change-of-variable' A g (equivs-are-haes g e)) q : qinv γ q = pr₂ (Σ-change-of-variable' A g (equivs-are-haes g e)) Σ-change-of-variable-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : X → 𝓦 ̇ ) (e : Y ≃ X) → (Σ y ꞉ Y , A (⌜ e ⌝ y)) ≃ (Σ x ꞉ X , A x) Σ-change-of-variable-≃ A (g , i) = Σ-change-of-variable A g i Σ-bicong : {X : 𝓤 ̇ } (Y : X → 𝓥 ̇ ) {X' : 𝓤' ̇ } (Y' : X' → 𝓥' ̇ ) (𝕗 : X ≃ X') → ((x : X) → Y x ≃ Y' (⌜ 𝕗 ⌝ x)) → Σ Y ≃ Σ Y' Σ-bicong {𝓤} {𝓥} {𝓤'} {𝓥'} {X} Y {X'} Y' 𝕗 φ = Σ Y ≃⟨ Σ-cong φ ⟩ (Σ x ꞉ X , Y' (⌜ 𝕗 ⌝ x)) ≃⟨ Σ-change-of-variable-≃ Y' 𝕗 ⟩ Σ Y' ■ dprecomp : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : Y → 𝓦 ̇ ) (f : X → Y) → Π A → Π (A ∘ f) dprecomp A f = _∘ f dprecomp-is-equiv : funext 𝓤 𝓦 → funext 𝓥 𝓦 → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : Y → 𝓦 ̇ ) (f : X → Y) → is-equiv f → is-equiv (dprecomp A f) dprecomp-is-equiv fe fe' {X} {Y} A f i = qinvs-are-equivs φ ((ψ , ψφ , φψ)) where g = inverse f i η = inverses-are-retractions f i ε = inverses-are-sections f i τ : (x : X) → ap f (η x) = ε (f x) τ = half-adjoint-condition f i φ : Π A → Π (A ∘ f) φ = dprecomp A f ψ : Π (A ∘ f) → Π A ψ k y = transport A (ε y) (k (g y)) φψ₀ : (k : Π (A ∘ f)) (x : X) → transport A (ε (f x)) (k (g (f x))) = k x φψ₀ k x = transport A (ε (f x)) (k (g (f x))) =⟨ a ⟩ transport A (ap f (η x))(k (g (f x))) =⟨ b ⟩ transport (A ∘ f) (η x) (k (g (f x))) =⟨ c ⟩ k x ∎ where a = ap (λ - → transport A - (k (g (f x)))) ((τ x)⁻¹) b = (transport-ap A f (η x)) ⁻¹ c = apd k (η x) φψ : φ ∘ ψ ∼ id φψ k = dfunext fe (φψ₀ k) ψφ₀ : (h : Π A) (y : Y) → transport A (ε y) (h (f (g y))) = h y ψφ₀ h y = apd h (ε y) ψφ : ψ ∘ φ ∼ id ψφ h = dfunext fe' (ψφ₀ h) Π-change-of-variable : funext 𝓤 𝓦 → funext 𝓥 𝓦 → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : Y → 𝓦 ̇ ) (f : X → Y) → is-equiv f → (Π y ꞉ Y , A y) ≃ (Π x ꞉ X , A (f x)) Π-change-of-variable fe fe' A f i = dprecomp A f , dprecomp-is-equiv fe fe' A f i Π-change-of-variable-≃ : FunExt → {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (A : Y → 𝓦 ̇ ) (𝕗 : X ≃ Y) → (Π x ꞉ X , A (⌜ 𝕗 ⌝ x)) ≃ (Π y ꞉ Y , A y) Π-change-of-variable-≃ fe A (f , i) = ≃-sym (Π-change-of-variable (fe _ _) (fe _ _) A f i) Π-bicong : FunExt → {X : 𝓤 ̇ } (Y : X → 𝓥 ̇ ) {X' : 𝓤' ̇ } (Y' : X' → 𝓥' ̇ ) (𝕗 : X ≃ X') → ((x : X) → Y x ≃ Y' (⌜ 𝕗 ⌝ x)) → Π Y ≃ Π Y' Π-bicong {𝓤} {𝓥} {𝓤'} {𝓥'} fe {X} Y {X'} Y' 𝕗 φ = Π Y ≃⟨ Π-cong (fe 𝓤 𝓥) (fe 𝓤 𝓥') φ ⟩ (Π x ꞉ X , Y' (⌜ 𝕗 ⌝ x)) ≃⟨ Π-change-of-variable-≃ fe Y' 𝕗 ⟩ Π Y' ■ NatΠ-fiber-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → funext 𝓤 𝓦 → (g : Π B) → (Π x ꞉ X , fiber (ζ x) (g x)) ≃ fiber (NatΠ ζ) g NatΠ-fiber-equiv {𝓤} {𝓥} {𝓦} {X} A B ζ fe g = (Π x ꞉ X , fiber (ζ x) (g x)) ≃⟨ i ⟩ (Π x ꞉ X , Σ a ꞉ A x , ζ x a = g x) ≃⟨ ii ⟩ (Σ f ꞉ Π A , Π x ꞉ X , ζ x (f x) = g x) ≃⟨ iii ⟩ (Σ f ꞉ Π A , (λ x → ζ x (f x)) = g) ≃⟨ iv ⟩ fiber (NatΠ ζ) g ■ where i = ≃-refl _ ii = ΠΣ-distr-≃ iii = Σ-cong (λ f → ≃-sym (≃-funext fe (λ x → ζ x (f x)) g)) iv = ≃-refl _ NatΠ-vv-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → funext 𝓤 (𝓥 ⊔ 𝓦) → ((x : X) → is-vv-equiv (ζ x)) → is-vv-equiv (NatΠ ζ) NatΠ-vv-equiv {𝓤} {𝓥} {𝓦} A B ζ fe i g = equiv-to-singleton (≃-sym (NatΠ-fiber-equiv A B ζ (lower-funext 𝓤 𝓥 fe) g)) (Π-is-singleton fe (λ x → i x (g x))) NatΠ-equiv : {X : 𝓤 ̇ } (A : X → 𝓥 ̇ ) (B : X → 𝓦 ̇ ) (ζ : Nat A B) → funext 𝓤 (𝓥 ⊔ 𝓦) → ((x : X) → is-equiv (ζ x)) → is-equiv (NatΠ ζ) NatΠ-equiv A B ζ fe i = vv-equivs-are-equivs (NatΠ ζ) (NatΠ-vv-equiv A B ζ fe (λ x → equivs-are-vv-equivs (ζ x) (i x))) Π-cong' : {X : 𝓤 ̇ } → funext 𝓤 (𝓥 ⊔ 𝓦) → {A : X → 𝓥 ̇ } {B : X → 𝓦 ̇ } → ((x : X) → A x ≃ B x) → Π A ≃ Π B Π-cong' fe {A} {B} e = NatΠ (λ x → pr₁ (e x)) , NatΠ-equiv A B (λ x → pr₁ (e x)) fe (λ x → pr₂ (e x)) =-cong : {X : 𝓤 ̇ } (x y : X) {x' y' : X} → x = x' → y = y' → (x = y) ≃ (x' = y') =-cong x y refl refl = ≃-refl (x = y) =-cong-l : {X : 𝓤 ̇ } (x y : X) {x' : X} → x = x' → (x = y) ≃ (x' = y) =-cong-l x y refl = ≃-refl (x = y) =-cong-r : {X : 𝓤 ̇ } (x y : X) {y' : X} → y = y' → (x = y) ≃ (x = y') =-cong-r x y refl = ≃-refl (x = y) =-flip : {X : 𝓤 ̇ } {x y : X} → (x = y) ≃ (y = x) =-flip = _⁻¹ , (_⁻¹ , ⁻¹-involutive) , (_⁻¹ , ⁻¹-involutive) singleton-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → is-singleton X → is-singleton Y → X ≃ Y singleton-≃ i j = (λ _ → center j) , maps-of-singletons-are-equivs _ i j singleton-≃-𝟙 : {X : 𝓤 ̇ } → is-singleton X → X ≃ 𝟙 {𝓥} singleton-≃-𝟙 i = singleton-≃ i 𝟙-is-singleton singleton-≃-𝟙' : {X : 𝓤 ̇ } → is-singleton X → 𝟙 {𝓥} ≃ X singleton-≃-𝟙' = singleton-≃ 𝟙-is-singleton 𝟙-=-≃ : (P : 𝓤 ̇ ) → funext 𝓤 𝓤 → propext 𝓤 → is-prop P → (𝟙 = P) ≃ P 𝟙-=-≃ P fe pe i = qinveq (λ q → Idtofun q ⋆) (f , ε , η) where f : P → 𝟙 = P f p = pe 𝟙-is-prop i (λ _ → p) unique-to-𝟙 η : (p : P) → Idtofun (f p) ⋆ = p η p = i (Idtofun (f p) ⋆) p ε : (q : 𝟙 = P) → f (Idtofun q ⋆) = q ε q = identifications-with-props-are-props pe fe P i 𝟙 (f (Idtofun q ⋆)) q empty-≃-𝟘 : {X : 𝓤 ̇ } → (X → 𝟘 {𝓥}) → X ≃ 𝟘 {𝓦} empty-≃-𝟘 i = qinveq (𝟘-elim ∘ i) (𝟘-elim , (λ x → 𝟘-elim (i x)) , (λ x → 𝟘-elim x)) complement-is-equiv : is-equiv complement complement-is-equiv = qinvs-are-equivs complement (complement , complement-involutive , complement-involutive) complement-≃ : 𝟚 ≃ 𝟚 complement-≃ = (complement , complement-is-equiv) 𝟚-≃-𝟙+𝟙 : 𝟚 ≃ 𝟙{𝓤} + 𝟙{𝓤} 𝟚-≃-𝟙+𝟙 = f , qinvs-are-equivs f (g , gf , fg) where f : 𝟚 → 𝟙 + 𝟙 f = 𝟚-cases (inl ⋆) (inr ⋆) g : 𝟙 + 𝟙 → 𝟚 g = cases (λ x → ₀) (λ x → ₁) fg : (x : 𝟙 + 𝟙) → f (g x) = x fg (inl ⋆) = refl fg (inr ⋆) = refl gf : (x : 𝟚) → g (f x) = x gf ₀ = refl gf ₁ = refl alternative-× : funext 𝓤₀ 𝓤 → {A : 𝟚 → 𝓤 ̇ } → (Π n ꞉ 𝟚 , A n) ≃ (A ₀ × A ₁) alternative-× fe {A} = qinveq ϕ (ψ , η , ε) where ϕ : (Π n ꞉ 𝟚 , A n) → A ₀ × A ₁ ϕ f = (f ₀ , f ₁) ψ : A ₀ × A ₁ → Π n ꞉ 𝟚 , A n ψ (a₀ , a₁) ₀ = a₀ ψ (a₀ , a₁) ₁ = a₁ η : ψ ∘ ϕ ∼ id η f = dfunext fe (λ {₀ → refl ; ₁ → refl}) ε : ϕ ∘ ψ ∼ id ε (a₀ , a₁) = refl alternative-+ : {A : 𝟚 → 𝓤 ̇ } → (Σ n ꞉ 𝟚 , A n) ≃ (A ₀ + A ₁) alternative-+ {𝓤} {A} = qinveq ϕ (ψ , η , ε) where ϕ : (Σ n ꞉ 𝟚 , A n) → A ₀ + A ₁ ϕ (₀ , a) = inl a ϕ (₁ , a) = inr a ψ : A ₀ + A ₁ → Σ n ꞉ 𝟚 , A n ψ (inl a) = ₀ , a ψ (inr a) = ₁ , a η : ψ ∘ ϕ ∼ id η (₀ , a) = refl η (₁ , a) = refl ε : ϕ ∘ ψ ∼ id ε (inl a) = refl ε (inr a) = refl domain-is-total-fiber : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → X ≃ Σ (fiber f) domain-is-total-fiber {𝓤} {𝓥} {X} {Y} f = X ≃⟨ ≃-sym (𝟙-rneutral {𝓤} {𝓤}) ⟩ X × 𝟙 ≃⟨ Σ-cong (λ x → singleton-≃ 𝟙-is-singleton (singleton-types-are-singletons (f x))) ⟩ (Σ x ꞉ X , Σ y ꞉ Y , f x = y) ≃⟨ Σ-flip ⟩ (Σ y ꞉ Y , Σ x ꞉ X , f x = y) ■ total-fiber-is-domain : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X → Y) → (Σ y ꞉ Y , Σ x ꞉ X , f x = y) ≃ X total-fiber-is-domain {𝓤} {𝓥} {X} {Y} f = ≃-sym (domain-is-total-fiber f) left-Id-equiv : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (x : X) → (Σ x' ꞉ X , (x' = x) × Y x') ≃ Y x left-Id-equiv {𝓤} {𝓥} {X} {Y} x = (Σ x' ꞉ X , (x' = x) × Y x') ≃⟨ ≃-sym Σ-assoc ⟩ (Σ (x' , _) ꞉ singleton-type' x , Y x') ≃⟨ a ⟩ Y x ■ where a = prop-indexed-sum (singleton-types'-are-props x) (singleton'-center x) right-Id-equiv : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (x : X) → (Σ x' ꞉ X , Y x' × (x' = x)) ≃ Y x right-Id-equiv {𝓤} {𝓥} {X} {Y} x = (Σ x' ꞉ X , Y x' × (x' = x)) ≃⟨ Σ-cong (λ x' → ×-comm) ⟩ (Σ x' ꞉ X , (x' = x) × Y x') ≃⟨ left-Id-equiv x ⟩ Y x ■ pr₁-fiber-equiv : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } (x : X) → fiber (pr₁ {𝓤} {𝓥} {X} {Y}) x ≃ Y x pr₁-fiber-equiv {𝓤} {𝓥} {X} {Y} x = fiber pr₁ x ≃⟨ Σ-assoc ⟩ (Σ x' ꞉ X , Y x' × (x' = x)) ≃⟨ right-Id-equiv x ⟩ Y x ■ \end{code} Tom de Jong, September 2019 (two lemmas used in UF.Classifiers-Old) A nice application of Σ-change-of-variable is that the fiber of a map doesn't change (up to equivalence, at least) when precomposing with an equivalence. These two lemmas are used in UF.Classifiers-Old, but are sufficiently general to warrant their place here. \begin{code} precomposition-with-equiv-does-not-change-fibers : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (e : Z ≃ X) (f : X → Y) (y : Y) → fiber (f ∘ ⌜ e ⌝) y ≃ fiber f y precomposition-with-equiv-does-not-change-fibers (g , i) f y = Σ-change-of-variable (λ - → f - = y) g i retract-pointed-fibers : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {r : Y → X} → has-section r ≃ (Π x ꞉ X , fiber r x) retract-pointed-fibers {𝓤} {𝓥} {X} {Y} {r} = qinveq f (g , (p , q)) where f : (Σ s ꞉ (X → Y) , r ∘ s ∼ id) → Π (fiber r) f (s , rs) x = (s x) , (rs x) g : ((x : X) → fiber r x) → Σ s ꞉ (X → Y) , r ∘ s ∼ id g α = (λ (x : X) → pr₁ (α x)) , (λ (x : X) → pr₂ (α x)) p : (srs : Σ s ꞉ (X → Y) , r ∘ s ∼ id) → g (f srs) = srs p (s , rs) = refl q : (α : Π x ꞉ X , fiber r x) → f (g α) = α q α = refl \end{code} Added 10 February 2020 by Tom de Jong. \begin{code} fiber-of-composite : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X → Y) (g : Y → Z) → (z : Z) → fiber (g ∘ f) z ≃ (Σ (y , _) ꞉ fiber g z , fiber f y) fiber-of-composite {𝓤} {𝓥} {𝓦} {X} {Y} {Z} f g z = qinveq ϕ (ψ , (ψϕ , ϕψ)) where ϕ : fiber (g ∘ f) z → (Σ w ꞉ (fiber g z) , fiber f (fiber-point w)) ϕ (x , p) = ((f x) , p) , (x , refl) ψ : (Σ w ꞉ (fiber g z) , fiber f (fiber-point w)) → fiber (g ∘ f) z ψ ((y , q) , (x , p)) = x , ((ap g p) ∙ q) ψϕ : (w : fiber (g ∘ f) z) → ψ (ϕ w) = w ψϕ (x , refl) = refl ϕψ : (w : Σ w ꞉ (fiber g z) , fiber f (fiber-point w)) → ϕ (ψ w) = w ϕψ ((.(f x) , refl) , (x , refl)) = refl fiber-of-unique-to-𝟙 : {𝓥 : Universe} {X : 𝓤 ̇ } → (u : 𝟙) → fiber (unique-to-𝟙 {_} {𝓥} {X}) u ≃ X fiber-of-unique-to-𝟙 {𝓤} {𝓥} {X} ⋆ = (Σ x ꞉ X , unique-to-𝟙 x = ⋆) ≃⟨ Σ-cong ψ ⟩ X × 𝟙{𝓥} ≃⟨ 𝟙-rneutral ⟩ X ■ where ψ : (x : X) → (⋆ = ⋆) ≃ 𝟙 ψ x = singleton-≃-𝟙 (pointed-props-are-singletons refl (props-are-sets 𝟙-is-prop)) ∼-fiber-identifications-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {f : X → Y} {g : X → Y} → f ∼ g → (y : Y) (x : X) → (f x = y) ≃ (g x = y) ∼-fiber-identifications-≃ {𝓤} {𝓥} {X} {Y} {f} {g} H y x = qinveq α (β , (βα , αβ)) where α : f x = y → g x = y α p = (H x) ⁻¹ ∙ p β : g x = y → f x = y β q = (H x) ∙ q βα : (p : f x = y) → β (α p) = p βα p = β (α p) =⟨ refl ⟩ (H x) ∙ ((H x) ⁻¹ ∙ p) =⟨ (∙assoc (H x) ((H x) ⁻¹) p) ⁻¹ ⟩ (H x) ∙ (H x) ⁻¹ ∙ p =⟨ ap (λ - → - ∙ p) ((right-inverse (H x)) ⁻¹) ⟩ refl ∙ p =⟨ refl-left-neutral ⟩ p ∎ αβ : (q : g x = y) → α (β q) = q αβ q = α (β q) =⟨ refl ⟩ (H x) ⁻¹ ∙ ((H x) ∙ q) =⟨ (∙assoc ((H x) ⁻¹) (H x) q) ⁻¹ ⟩ (H x) ⁻¹ ∙ (H x) ∙ q =⟨ ap (λ - → - ∙ q) (left-inverse (H x)) ⟩ refl ∙ q =⟨ refl-left-neutral ⟩ q ∎ ∼-fiber-≃ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {f : X → Y} {g : X → Y} → f ∼ g → (y : Y) → fiber f y ≃ fiber g y ∼-fiber-≃ H y = Σ-cong (∼-fiber-identifications-≃ H y) \end{code} Added 9 July 2024 by Tom de Jong. \begin{code} fiber-of-ap-≃' : {A : 𝓤 ̇ } {B : 𝓥 ̇ } (f : A → B) {x y : A} (p : f x = f y) → fiber (ap f) p ≃ ((x , refl) =[ fiber' f (f x) ] (y , p)) fiber-of-ap-≃' f {x} {y} p = fiber (ap f) p ≃⟨ ≃-refl _ ⟩ (Σ e ꞉ x = y , transport (λ - → (f x = f -)) e refl = p) ≃⟨ ≃-sym Σ-=-≃ ⟩ ((x , refl) = (y , p)) ■ fiber-of-ap-≃ : {A : 𝓤 ̇ } {B : 𝓥 ̇ } (f : A → B) {x y : A} (p : f x = f y) → fiber (ap f) p ≃ ((x , p) =[ fiber f (f y) ] (y , refl)) fiber-of-ap-≃ f {x} {y} p = fiber (ap f) p ≃⟨ Σ-cong I ⟩ (Σ e ꞉ x = y , transport (λ - → f - = f y) e p = refl) ≃⟨ ≃-sym Σ-=-≃ ⟩ ((x , p) = (y , refl)) ■ where I : (e : x = y) → (ap f e = p) ≃ (transport (λ - → f - = f y) e p = refl) I refl = (refl = p) ≃⟨ =-flip ⟩ (p = refl) ≃⟨ ≃-refl _ ⟩ (transport (λ - → f - = f x) refl p = refl) ■ ∙-is-equiv-left : {X : 𝓤 ̇ } {x y z : X} (p : z = x) → is-equiv (λ (q : x = y) → p ∙ q) ∙-is-equiv-left {𝓤} {X} {x} {y} refl = equiv-closed-under-∼ id (refl ∙_) (id-is-equiv (x = y)) (λ _ → refl-left-neutral) ∙-is-equiv-right : {X : 𝓤 ̇ } {x y z : X} (q : x = y) → is-equiv (λ (p : z = x) → p ∙ q) ∙-is-equiv-right {𝓤} {X} {x} {y} {z} refl = id-is-equiv (z = y) \end{code} Added by Tom de Jong, November 2021. \begin{code} open import UF.PropTrunc module _ (pt : propositional-truncations-exist) where open PropositionalTruncation pt ∥∥-cong : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } → X ≃ Y → ∥ X ∥ ≃ ∥ Y ∥ ∥∥-cong f = logically-equivalent-props-are-equivalent ∥∥-is-prop ∥∥-is-prop (∥∥-functor ⌜ f ⌝) (∥∥-functor ⌜ f ⌝⁻¹) ∃-cong : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {Y' : X → 𝓦 ̇ } → ((x : X) → Y x ≃ Y' x) → ∃ Y ≃ ∃ Y' ∃-cong e = ∥∥-cong (Σ-cong e) outer-∃-inner-Σ : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ } {A : (x : X) → Y x → 𝓦 ̇ } → (∃ x ꞉ X , ∃ y ꞉ Y x , A x y) ≃ (∃ x ꞉ X , Σ y ꞉ Y x , A x y) outer-∃-inner-Σ {𝓤} {𝓥} {𝓦} {X} {Y} {A} = logically-equivalent-props-are-equivalent ∥∥-is-prop ∥∥-is-prop f g where g : (∃ x ꞉ X , Σ y ꞉ Y x , A x y) → (∃ x ꞉ X , ∃ y ꞉ Y x , A x y) g = ∥∥-functor (λ (x , y , a) → x , ∣ y , a ∣) f : (∃ x ꞉ X , ∃ y ꞉ Y x , A x y) → (∃ x ꞉ X , Σ y ꞉ Y x , A x y) f = ∥∥-rec ∥∥-is-prop ϕ where ϕ : (Σ x ꞉ X , ∃ y ꞉ Y x , A x y) → (∃ x ꞉ X , Σ y ꞉ Y x , A x y) ϕ (x , p) = ∥∥-functor (λ (y , a) → x , y , a) p \end{code}