Martin Escardo, 2012-

Expanded on demand whenever a general equivalence is needed.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

open import SpartanMLTT
open import Two-Properties
open import UF-Base
open import UF-Equiv
open import UF-FunExt
open import UF-Lower-FunExt
open import UF-Subsingletons
open import UF-Subsingletons-FunExt
open import UF-PropIndexedPiSigma

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

Ξ£-cong : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Y' : X β†’ 𝓦 Μ‡ }
       β†’ ((x : X) β†’ Y x ≃ Y' x) β†’ Ξ£ Y ≃ Ξ£ Y'
Ξ£-cong {𝓀} {π“₯} {𝓦} {X} {Y} {Y'} Ο† = (F , (G , FG) , (H , HF))
 where
  f : (x : X) β†’ Y x β†’ Y' x
  f x = pr₁ (Ο† x)

  g : (x : X) β†’ Y' x β†’ Y x
  g x = pr₁ (pr₁ (prβ‚‚ (Ο† x)))

  fg : (x : X) (y' : Y' x) β†’ f x (g x y') ≑ y'
  fg x = prβ‚‚ (pr₁ (prβ‚‚ (Ο† x)))

  h : (x : X) β†’ Y' x β†’ Y x
  h x = pr₁ (prβ‚‚ (prβ‚‚ (Ο† x)))

  hf : (x : X) (y : Y x) β†’ h x (f x y) ≑ y
  hf x = prβ‚‚ (prβ‚‚ (prβ‚‚ (Ο† x)))

  F : Ξ£ Y β†’ Ξ£ Y'
  F (x , y) = x , f x y

  G : Ξ£ Y' β†’ Ξ£ Y
  G (x , y') = x , g x y'

  H : Ξ£ Y' β†’ Ξ£ Y
  H (x , y') = x , h x y'

  FG : (w' : Ξ£ Y') β†’ F (G w') ≑ w'
  FG (x , y') = to-Ξ£-≑' (fg x y')

  HF : (w : Ξ£ Y) β†’ H (F w) ≑ w
  HF (x , y) = to-Ξ£-≑' (hf x 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-≃ {𝓀} {π“₯} {𝓦} {X} {A} {P} = qinveq Ξ Ξ£-distr (Ξ Ξ£-distr-back , Ξ΅ , Ξ·)
 where
  Ξ· :  Ξ Ξ£-distr {𝓀} {π“₯} {𝓦} {X} {A} {P} ∘ Ξ Ξ£-distr-back ∼ id
  Ξ· _ = refl

  Ρ : ΠΣ-distr-back ∘ ΠΣ-distr ∼ id
  Ξ΅ _ = refl

Ξ£+ : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
   β†’ (Ξ£ x κž‰ X , A x + B x)
   ≃ ((Ξ£ x κž‰ X , A x) + (Ξ£ x κž‰ X , B x))
Ξ£+ 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

\end{code}

The following name is badly chosen, and probably should have been used
for the above:

\begin{code}

Ξ£+distr : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡ ) (A : X + Y β†’ 𝓦 Μ‡ )
        β†’ (Ξ£ x κž‰ X , A (inl x)) + (Ξ£ y κž‰ Y , A (inr y))
        ≃ (Ξ£ z κž‰ X + Y , A z)
Ξ£+distr 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' Ο† = (F , (G , FG) , (H , HF))
 where
  f : (x : X) β†’ Y x β†’ Y' x
  f x = pr₁ (Ο† x)

  g : (x : X) β†’ Y' x β†’ Y x
  g x =  pr₁ (pr₁ (prβ‚‚ (Ο† x)))

  fg : (x : X) (y' : Y' x) β†’ f x (g x y') ≑ y'
  fg x = prβ‚‚ (pr₁ (prβ‚‚ (Ο† x)))

  h : (x : X) β†’ Y' x β†’ Y x
  h x = pr₁ (prβ‚‚ (prβ‚‚ (Ο† x)))

  hf : (x : X) (y : Y x) β†’ h x (f x y) ≑ y
  hf x = prβ‚‚ (prβ‚‚ (prβ‚‚ (Ο† x)))

  F : ((x : X) β†’ Y x) β†’ ((x : X) β†’ Y' x)
  F = Ξ» z x β†’ pr₁ (Ο† x) (z x)

  G : ((x : X) β†’ Y' x) β†’ (x : X) β†’ Y x
  G u x = g x (u x)

  H : ((x : X) β†’ Y' x) β†’ (x : X) β†’ Y x
  H u' x = h x (u' x)

  FG :  (w' : ((x : X) β†’ Y' x)) β†’ F (G w') ≑ w'
  FG w' = dfunext fe' FG'
   where
    FG' : (x : X) β†’ F (G w') x ≑ w' x
    FG' x = fg x (w' x)

  HF : (w : ((x : X) β†’ Y x)) β†’ H (F w) ≑ w
  HF w = dfunext fe GF'
   where
    GF' : (x : X) β†’ H (F w) x ≑ w x
    GF' x = hf x (w 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
                        (Ξ» x β†’ f x ≑ g x)
                        (Ξ» x β†’ f x ∼ g x)
                        (Ξ» 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

𝟘-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       β– 

one-πŸ™-only : (𝓀 π“₯ : Universe) β†’ πŸ™ {𝓀} ≃ πŸ™ {π“₯}
one-πŸ™-only _ _ = unique-to-πŸ™ , (unique-to-πŸ™ , (Ξ» {* β†’ refl})) , (unique-to-πŸ™ , (Ξ» {* β†’ refl}))

+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

+functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
         β†’ (X β†’ A) β†’ (Y β†’ B) β†’ X + Y β†’ A + B
+functor f g (inl x) = inl (f x)
+functor f g (inr y) = inr (g y)

+cong : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
      β†’ X ≃ A β†’ Y ≃ B β†’ X + Y ≃ A + B
+cong {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {A} {B} (f , (g , e) , (g' , d)) (Ο† , (Ξ³ , Ξ΅) , (Ξ³' , Ξ΄)) =
 +functor f Ο† , (+functor g Ξ³ , E) , (+functor g' Ξ³' , D)
 where
  E : (c : A + B) β†’ +functor f Ο† (+functor g Ξ³ c) ≑ c
  E (inl a) = ap inl (e a)
  E (inr b) = ap inr (Ξ΅ b)

  D : (z : X + Y) β†’ +functor g' Ξ³' (+functor f Ο† z) ≑ z
  D (inl x) = ap inl (d x)
  D (inr y) = ap inr (Ξ΄ y)

Γ—πŸ˜ : {X : 𝓀 Μ‡ } β†’ 𝟘 {π“₯} ≃ X Γ— 𝟘 {𝓦}
Γ—πŸ˜ {𝓀} {π“₯} {𝓦} {X} = qinveq f (g , Ξ· , Ξ΅)
 where
   f : 𝟘 β†’ X Γ— 𝟘
   f = unique-from-𝟘

   g : X Γ— 𝟘 β†’ 𝟘
   g (x , y) = 𝟘-elim y

   Ξ΅ : (t : X Γ— 𝟘) β†’ (f ∘ g) t ≑ t
   Ρ (x , y) = 𝟘-elim y

   Ξ· : (u : 𝟘) β†’ (g ∘ f) u ≑ u
   η = 𝟘-induction

πŸ™distr : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X Γ— Y + X ≃ X Γ— (Y + πŸ™ {𝓦})
πŸ™distr {𝓀} {π“₯} {𝓦} {X} {Y} = f , (g , Ξ΅) , (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

   Ξ΅ : (t : X Γ— (Y + πŸ™)) β†’ (f ∘ g) t ≑ t
   Ξ΅ (x , inl y) = refl
   Ξ΅ (x , inr *) = refl

   Ξ· : (u : X Γ— Y + X) β†’ (g ∘ f) u ≑ u
   Ξ· (inl (x , y)) = refl
   Ξ· (inr x)       = refl

Ap+ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (Z : 𝓦 Μ‡ ) β†’ X ≃ Y β†’ X + Z ≃ Y + Z
Ap+ {𝓀} {π“₯} {𝓦} {X} {Y} Z (f , (g , Ξ΅) , (h , Ξ·)) = f' , (g' , Ξ΅') , (h' , Ξ·')
 where
   f' : X + Z β†’ Y + Z
   f' (inl x) = inl (f x)
   f' (inr z) = inr z

   g' : Y + Z β†’ X + Z
   g' (inl y) = inl (g y)
   g' (inr z) = inr z

   h' : Y + Z β†’ X + Z
   h' (inl y) = inl (h y)
   h' (inr z) = inr z

   Ξ΅' : (t : Y + Z) β†’ (f' ∘ g') t ≑ t
   Ξ΅' (inl y) = ap inl (Ξ΅ y)
   Ξ΅' (inr z) = refl

   Ξ·' : (u : X + Z) β†’ (h' ∘ f') u ≑ u
   Ξ·' (inl x) = ap inl (Ξ· x)
   Ξ·' (inr z) = refl

Γ—comm : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X Γ— Y ≃ Y Γ— X
Γ—comm {𝓀} {π“₯} {X} {Y} = f , (g , Ξ΅) , (g , Ξ·)
 where
   f : X Γ— Y β†’ Y Γ— X
   f (x , y) = (y , x)

   g : Y Γ— X β†’ X Γ— Y
   g (y , x) = (x , y)

   Ξ΅ : (t : Y Γ— X) β†’ (f ∘ g) t ≑ t
   Ξ΅ (y , x) = refl

   Ξ· : (u : X Γ— Y) β†’ (g ∘ f) u ≑ u
   Ξ· (x , y) = refl

Γ—functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
         β†’ (X β†’ A) β†’ (Y β†’ B) β†’ X Γ— Y β†’ A Γ— B
Γ—functor f g (x , y) = f x , g y

Γ—-cong : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
      β†’ X ≃ A β†’ Y ≃ B β†’ X Γ— Y ≃ A Γ— B
Γ—-cong {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} {A} {B} (f , (g , e) , (g' , d)) (Ο† , (Ξ³ , Ξ΅) , (Ξ³' , Ξ΄)) =
 Γ—functor f Ο† , (Γ—functor g Ξ³ , E) , (Γ—functor g' Ξ³' , D)
 where
  E : (c : A Γ— B) β†’ Γ—functor f Ο† (Γ—functor g Ξ³ c) ≑ c
  E (a , b) = to-Γ—-≑ (e a) (Ξ΅ b)

  D : (z : X Γ— Y) β†’ Γ—functor g' Ξ³' (Γ—functor f Ο† z) ≑ z
  D (x , y) = to-Γ—-≑ (d x) (Ξ΄ y)

πŸ˜β†’ : {X : 𝓀 Μ‡ }
   β†’ funext 𝓦 𝓀
   β†’ πŸ™ {π“₯} ≃ (𝟘 {𝓦} β†’ X)
πŸ˜β†’ {𝓀} {π“₯} {𝓦} {X} fe = qinveq f (g , Ξ΅ , Ξ·)
 where
  f : πŸ™ β†’ 𝟘 β†’ X
  f * y = 𝟘-elim y

  g : (𝟘 β†’ X) β†’ πŸ™
  g h = *

  Ξ· : (h : 𝟘 β†’ X) β†’ f (g h) ≑ h
  Ξ· h = dfunext fe (Ξ» z β†’ 𝟘-elim z)

  Ξ΅ : (y : πŸ™) β†’ g (f y) ≑ y
  Ξ΅ * = 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 , i) (Ο† , j) =
 H (equivs-are-qinvs f i) (equivs-are-qinvs Ο† j)
 where
  H : qinv f β†’ qinv Ο† β†’ (X β†’ Y) ≃ (A β†’ B)
  H (g , e , d) (Ξ³ , Ξ΅ , Ξ΄) =  F , (G , E) , (G , D)
   where
    F : (X β†’ Y) β†’ (A β†’ B)
    F h = Ο† ∘ h ∘ g

    G : (A β†’ B) β†’ (X β†’ Y)
    G k = γ ∘ k ∘ f

    E : (k : A β†’ B) β†’ F (G k) ≑ k
    E k = dfunext fe (Ξ» a β†’ Ξ΄ (k (f (g a))) βˆ™ ap k (d a))

    D : (h : X β†’ Y) β†’ G (F h) ≑ h
    D h = dfunext fe' (Ξ» x β†’ Ξ΅ (h (g (f x))) βˆ™ ap h (e x))

β†’cong' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {B : 𝓣 Μ‡ }
       β†’ funext 𝓀 𝓣
       β†’ funext 𝓀 π“₯
       β†’ Y ≃ B β†’ (X β†’ Y) ≃ (X β†’ B)
β†’cong' {𝓀} {π“₯} {𝓣} {X} {Y} {B} fe fe' = β†’cong fe fe' (≃-refl X)

pr₁-equivalence : (X : 𝓀 Μ‡ ) (A : X β†’ π“₯ Μ‡ )
                β†’ ((x : X) β†’ is-singleton (A x))
                β†’ is-equiv (pr₁ {𝓀} {π“₯} {X} {A})
pr₁-equivalence {𝓀} {π“₯} X A iss = qinvs-are-equivs pr₁ (g , Ξ΅ , Ξ·)
 where
  g : X β†’ Ξ£ A
  g x = x , pr₁ (iss x)

  Ξ· : (x : X) β†’ pr₁ (g x) ≑ x
  Ξ· x = refl

  Ξ΅ : (Οƒ : Ξ£ A) β†’ g (pr₁ Οƒ) ≑ Οƒ
  Ξ΅ (x , a) = to-Ξ£-≑ (Ξ· x , singletons-are-props (iss x) _ _)

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 . (ΞΆ x a) (a , refl) = (x , a) , refl

  g : (b : B x) β†’ fiber (NatΞ£ ΞΆ) (x , b) β†’ fiber (ΞΆ x) b
  g . (ΞΆ x a) ((.x , a) , refl) = a , refl

  Ξ΅ : (b : B x) (w : fiber (ΞΆ x) b) β†’ g b (f b w) ≑ w
  Ξ΅ . (ΞΆ x a) (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Ξ£-equiv : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (ΞΆ : Nat A B)
           β†’ ((x : X) β†’ is-equiv (ΞΆ x))
           β†’ is-equiv (NatΞ£ ΞΆ)
NatΞ£-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 e = NatΞ£ (Ξ» x β†’ pr₁ (e x)) , NatΞ£-equiv A B (Ξ» x β†’ pr₁ (e x)) (Ξ» x β†’ prβ‚‚ (e x))

NatΞ£-equiv' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (ΞΆ : Nat A B)
            β†’ ((x : X) β†’ is-equiv (ΞΆ x))
            β†’ is-equiv (NatΞ£ ΞΆ)
NatΞ£-equiv' A B ΞΆ i = ((s , ΞΆs), (r , rΞΆ))
 where
  s : Ξ£ B β†’ Ξ£ A
  s (x , b) = x , pr₁ (pr₁ (i x)) b

  ΞΆs : (Ξ² : Ξ£ B) β†’ (NatΞ£ ΞΆ ∘ s) Ξ² ≑ Ξ²
  ΞΆs (x , b) = ap (Ξ» - β†’ (x , -)) (prβ‚‚ (pr₁ (i x)) b)

  r : Ξ£ B β†’ Ξ£ A
  r (x , b) = x , (pr₁ (prβ‚‚ (i x)) b)

  rΞΆ : (Ξ± : Ξ£ A) β†’ (r ∘ NatΞ£ ΞΆ) Ξ± ≑ Ξ±
  rΞΆ (x , a) = ap (Ξ» - β†’ (x , -)) (prβ‚‚ (prβ‚‚ (i x)) a)

Ξ£-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 , back-transport A (Ξ΅ x) a)

  Ξ³Ο† : (Οƒ : Ξ£ A) β†’ Ξ³ (Ο† Οƒ) ≑ Οƒ
  Ξ³Ο† (x , a) = to-Ξ£-≑ (Ξ΅ x , p)
   where
    p : transport A (Ξ΅ x) (back-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) (back-transport A (Ξ΅ (g y)) a) β‰‘βŸ¨ i ⟩
        transport A (ap g (Ξ· y)) (back-transport A (Ξ΅ (g y)) a)        β‰‘βŸ¨ ii ⟩
        transport A (Ξ΅ (g y)) (back-transport A (Ξ΅ (g y)) a)           β‰‘βŸ¨ iii ⟩
        a                                                              ∎
     where
      i   = transport-ap A g (Ξ· y)
      ii  = ap (Ξ» - β†’ transport A - (back-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)) ≃ Ξ£ A
Ξ£-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))

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 : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
        β†’ funext 𝓀 (π“₯ βŠ” 𝓦)
        β†’ ((x : X) β†’ A x ≃ B x)
        β†’ Ξ  A ≃ Ξ  B
Ξ -cong' A B fe 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-≃ {𝓀} {π“₯} (c , Ο†) (d , Ξ³) = (Ξ» _ β†’ d) , ((Ξ» _ β†’ c) , Ξ³) , ((Ξ» _ β†’ c) , Ο†)

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

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 (Ξ» x β†’ f x ≑ y) g i

retract-pointed-fibers : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {r : Y β†’ X}
                       β†’ (Ξ£ s κž‰ (X β†’ Y) , r ∘ s ∼ id) ≃ (Ξ  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)

βˆ™-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}