Skip to content

UF.EquivalenceExamples

Martin Escardo, 2012-

Expanded on demand whenever a general equivalence is needed.


{-# 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

Ξ -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 , H , G)
 where
  f : ((x : X) (y : Y) β†’ A x y) β†’ ((y : Y) (x : X) β†’ A x y)
  f h y x = h x y
  g : ((y : Y) (x : X) β†’ A x y) β†’ ((x : X) (y : Y) β†’ A x y)
  g h x y = h y x
  H : (h : ((x : X) (y : Y) β†’ A x y)) β†’ g (f h) ＝ h
  H h = refl
  G : (h : ((y : Y) (x : X) β†’ A x y)) β†’ f (g h) ＝ h
  G h = refl

Ξ -flip' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : X β†’ Y β†’ 𝓦 Μ‡ }
        β†’ ((y : Y) (x : X) β†’ A x y) ≃ ((x : X) (y : Y) β†’ A x y)
Ξ -flip' = ≃-sym Ξ -flip

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


An application of Ξ -cong is the following:


≃-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 Γ— πŸ™                         β‰ƒβŸ¨ I ⟩
 (Ξ£ x κž‰ X , Ξ£ y κž‰ Y , f x ＝ y) β‰ƒβŸ¨ Ξ£-flip ⟩
 (Ξ£ y κž‰ Y , Ξ£ x κž‰ X , f x ＝ y) β– 
  where
   I =  Ξ£-cong
         (Ξ» x β†’ singleton-≃ πŸ™-is-singleton
                 (singleton-types-are-singletons (f x)))

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'-center x) (singleton-types'-are-props 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                           β– 


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.


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


Added 10 February 2020 by Tom de Jong.


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)


Added 9 July 2024 by Tom de Jong.


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                                              β‰ƒβŸ¨by-definition⟩
 (Ξ£ 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)                                   β‰ƒβŸ¨by-definition⟩
            (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)


Added by Tom de Jong, November 2021.


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


Added by Anna Williams 26 February

We show that for subtypes, equality on subtypes is equivalent
to equality on the base type.


subtype-＝-≃-pr₁-＝ : {X : 𝓀 Μ‡ }
                     (P : X β†’ π“₯ Μ‡ )
                   β†’ ((x : X) β†’ is-prop (P x))
                   β†’ (x y : Ξ£ P)
                   β†’ (x ＝ y) ≃ (pr₁ x ＝ pr₁ y)
subtype-＝-≃-pr₁-＝ {_} {_} {X} P p (x , Px) (y , Py)
 = qinveq f (f⁻¹ , (f-is-section , f-has-section))
 where
  f : (x , Px) ＝ (y , Py) β†’ x ＝ y
  f refl = refl

  f⁻¹ : x ＝ y β†’ (x , Px) ＝ (y , Py)
  f⁻¹ refl = to-Σ-＝' (p x Px Py)

  f-has-section : f ∘ f⁻¹ ∼ id
  f-has-section refl = t (p x Px Py)
   where
    t : Px ＝ Py β†’ (f ∘ f⁻¹) refl ＝ refl
    t refl = ap (f ∘ to-Σ-＝') (props-are-sets (p x) (p x Px Px) refl)

  f-is-section : f⁻¹ ∘ f ∼ id
  f-is-section refl = ap to-Σ-＝' (props-are-sets (p x) (p x Px Px) refl)