------------------------------------------------------------------------
-- Truncation, defined using a kind of Church encoding
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

-- Partly following the HoTT book.

open import Equality

module H-level.Truncation.Church
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Prelude
open import Logical-equivalence using (_⇔_)

open import Bijection eq as Bijection using (_↔_)
open Derived-definitions-and-properties eq
open import Embedding eq hiding (_∘_)
open import Equality.Decidable-UIP eq
import Equality.Groupoid eq as EG
open import Equivalence eq as Eq using (_≃_; Is-equivalence)
import Equivalence.Half-adjoint eq as HA
open import Extensionality eq
open import Function-universe eq as F hiding (_∘_)
open import Groupoid eq
open import H-level eq as H-level
open import H-level.Closure eq
open import Nat eq
open import Preimage eq as Preimage using (_⁻¹_)
open import Surjection eq using (_↠_; Split-surjective)

-- Truncation.

∥_∥ : ∀ {a} → Type a → ℕ → (ℓ : Level) → Type (a ⊔ lsuc ℓ)
∥ A ∥ n ℓ = (P : Type ℓ) → H-level n P → (A → P) → P

-- If A is inhabited, then ∥ A ∥ n ℓ is also inhabited.

∣_∣ : ∀ {n ℓ a} {A : Type a} → A → ∥ A ∥ n ℓ
∣ x ∣ = λ _ _ f → f x

-- A special case of ∣_∣.

∣_∣₁ : ∀ {ℓ a} {A : Type a} → A → ∥ A ∥  ℓ
∣ x ∣₁ = ∣_∣ {n = } x

-- The truncation produces types of the right h-level (assuming
-- extensionality).

truncation-has-correct-h-level :
  ∀ n {ℓ a} {A : Type a} →
  Extensionality (a ⊔ lsuc ℓ) (a ⊔ ℓ) →
  H-level n (∥ A ∥ n ℓ)
truncation-has-correct-h-level n {ℓ} {a} ext =
  Π-closure (lower-extensionality a            lzero ext) n λ _ →
  Π-closure (lower-extensionality (a ⊔ lsuc ℓ) lzero ext) n λ h →
  Π-closure (lower-extensionality (lsuc ℓ)     a     ext) n λ _ →
  h

-- Primitive "recursion" for truncated types.

rec :
  ∀ n {a b} {A : Type a} {B : Type b} →
  H-level n B →
  (A → B) → ∥ A ∥ n b → B
rec _ h f x = x _ h f

private

  -- The function rec computes in the right way.

  rec-∣∣ :
    ∀ {n a b} {A : Type a} {B : Type b}
    (h : H-level n B) (f : A → B) (x : A) →
    rec _ h f ∣ x ∣ ≡ f x
  rec-∣∣ _ _ _ = refl _

-- Map function.

∥∥-map : ∀ n {a b ℓ} {A : Type a} {B : Type b} →
         (A → B) →
         ∥ A ∥ n ℓ → ∥ B ∥ n ℓ
∥∥-map _ f x = λ P h g → x P h (g ∘ f)

-- The truncation operator preserves logical equivalences.

∥∥-cong-⇔ : ∀ {n a b ℓ} {A : Type a} {B : Type b} →
            A ⇔ B → ∥ A ∥ n ℓ ⇔ ∥ B ∥ n ℓ
∥∥-cong-⇔ A⇔B = record
  { to   = ∥∥-map _ (_⇔_.to   A⇔B)
  ; from = ∥∥-map _ (_⇔_.from A⇔B)
  }

-- The truncation operator preserves bijections (assuming
-- extensionality).

∥∥-cong : ∀ {k n a b ℓ} {A : Type a} {B : Type b} →
          Extensionality (a ⊔ b ⊔ lsuc ℓ) (a ⊔ b ⊔ ℓ) →
          A ↔[ k ] B → ∥ A ∥ n ℓ ↔[ k ] ∥ B ∥ n ℓ
∥∥-cong {k} {n} {a} {b} {ℓ} ext A↝B = from-bijection (record
  { surjection = record
    { logical-equivalence = record
      { to   = ∥∥-map _ (_↔_.to   A↔B)
      ; from = ∥∥-map _ (_↔_.from A↔B)
      }
    ; right-inverse-of = lemma (lower-extensionality a a ext) A↔B
    }
  ; left-inverse-of = lemma (lower-extensionality b b ext) (inverse A↔B)
  })
  where
  A↔B = from-isomorphism A↝B

  lemma :
    ∀ {c d} {C : Type c} {D : Type d} →
    Extensionality (d ⊔ lsuc ℓ) (d ⊔ ℓ) →
    (C↔D : C ↔ D) (∥d∥ : ∥ D ∥ n ℓ) →
    ∥∥-map _ (_↔_.to C↔D) (∥∥-map _ (_↔_.from C↔D) ∥d∥) ≡ ∥d∥
  lemma {d} ext C↔D ∥d∥ =
    apply-ext (lower-extensionality d        lzero ext) λ P →
    apply-ext (lower-extensionality _        lzero ext) λ h →
    apply-ext (lower-extensionality (lsuc ℓ) d     ext) λ g →

      ∥d∥ P h (g ∘ _↔_.to C↔D ∘ _↔_.from C↔D)  ≡⟨ cong (λ f → ∥d∥ P h (g ∘ f)) $
                                                    apply-ext (lower-extensionality (lsuc ℓ) ℓ ext)
                                                      (_↔_.right-inverse-of C↔D) ⟩∎
      ∥d∥ P h g                                ∎

-- The universe level can be decreased (unless it is zero).

with-lower-level :
  ∀ ℓ₁ {ℓ₂ a} n {A : Type a} →
  ∥ A ∥ n (ℓ₁ ⊔ ℓ₂) → ∥ A ∥ n ℓ₂
with-lower-level ℓ₁ _ x =
  λ P h f → lower (x (↑ ℓ₁ P) (↑-closure _ h) (lift ∘ f))

private

  -- The function with-lower-level computes in the right way.

  with-lower-level-∣∣ :
    ∀ {ℓ₁ ℓ₂ a n} {A : Type a} (x : A) →
    with-lower-level ℓ₁ {ℓ₂ = ℓ₂} n ∣ x ∣ ≡ ∣ x ∣
  with-lower-level-∣∣ _ = refl _

-- ∥_∥ is downwards closed in the h-level.

downwards-closed :
  ∀ {m n a ℓ} {A : Type a} →
  n ≤ m →
  ∥ A ∥ m ℓ → ∥ A ∥ n ℓ
downwards-closed n≤m x = λ P h f → x P (H-level.mono n≤m h) f

private

  -- The function downwards-closed computes in the right way.

  downwards-closed-∣∣ :
    ∀ {m n a ℓ} {A : Type a} (n≤m : n ≤ m) (x : A) →
    downwards-closed {ℓ = ℓ} n≤m ∣ x ∣ ≡ ∣ x ∣
  downwards-closed-∣∣ _ _ = refl _

-- The function rec can be used to define a kind of dependently typed
-- eliminator for the propositional truncation (assuming
-- extensionality).

prop-elim :
  ∀ {ℓ a p} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a ⊔ p) →
  (P : ∥ A ∥  ℓ → Type p) →
  (∀ x → Is-proposition (P x)) →
  ((x : A) → P ∣ x ∣₁) →
  ∥ A ∥  (lsuc ℓ ⊔ a ⊔ p) → (x : ∥ A ∥  ℓ) → P x
prop-elim {ℓ} {a} {p} ext P P-prop f =
  rec 
      (Π-closure (lower-extensionality lzero (ℓ ⊔ a) ext)  P-prop)
      (λ x _ → subst P
                     (truncation-has-correct-h-level 
                        (lower-extensionality lzero p ext) _ _)
                     (f x))

opaque

  -- The eliminator gives the right result, up to propositional
  -- equality, when applied to ∣ x ∣ and ∣ x ∣.

  prop-elim-∣∣ :
    ∀ {ℓ a p} {A : Type a}
    (ext : Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a ⊔ p))
    (P : ∥ A ∥  ℓ → Type p)
    (P-prop : ∀ x → Is-proposition (P x))
    (f : (x : A) → P ∣ x ∣₁) (x : A) →
    prop-elim ext P P-prop f ∣ x ∣₁ ∣ x ∣₁ ≡ f x
  prop-elim-∣∣ _ _ P-prop _ _ = P-prop _ _ _

-- Nested truncations can sometimes be flattened.

flatten↠ :
  ∀ {m n a ℓ} {A : Type a} →
  Extensionality (a ⊔ lsuc ℓ) (a ⊔ ℓ) →
  m ≤ n →
  ∥ ∥ A ∥ m ℓ ∥ n (a ⊔ lsuc ℓ) ↠ ∥ A ∥ m ℓ
flatten↠ ext m≤n = record
  { logical-equivalence = record
    { to   = rec _
                 (H-level.mono m≤n
                    (truncation-has-correct-h-level _ ext))
                 F.id
    ; from = ∣_∣
    }
  ; right-inverse-of = refl
  }

flatten↔ :
  ∀ {a ℓ} {A : Type a} →
  Extensionality (lsuc (a ⊔ lsuc ℓ)) (lsuc (a ⊔ lsuc ℓ)) →
  (∥ ∥ A ∥  ℓ ∥        (a ⊔ lsuc ℓ) →
   ∥ ∥ A ∥  ℓ ∥  (lsuc (a ⊔ lsuc ℓ))) →
  ∥ ∥ A ∥  ℓ ∥  (a ⊔ lsuc ℓ) ↔ ∥ A ∥  ℓ
flatten↔ ext resize = record
  { surjection      = flatten↠ {m = } ext′ ≤-refl
  ; left-inverse-of = λ x →
      prop-elim
        ext
        (λ x → ∣ rec 
                     (H-level.mono (≤-refl {n = })
                        (truncation-has-correct-h-level  ext′))
                     F.id x ∣₁ ≡ x)
        (λ _ → ⇒≡  $ truncation-has-correct-h-level
                         (lower-extensionality lzero _ ext))
        (λ _ → refl _)
        (resize x)
        x
  }
  where
  ext′ = lower-extensionality _ _ ext

-- Surjectivity.
--
-- I'm not quite sure what the universe level of the truncation should
-- be, so I've included it as a parameter.

Surjective : ∀ {a b} ℓ {A : Type a} {B : Type b} →
             (A → B) → Type (a ⊔ b ⊔ lsuc ℓ)
Surjective ℓ f = ∀ b → ∥ f ⁻¹ b ∥  ℓ

-- The property Surjective ℓ f is a proposition (assuming
-- extensionality).

Surjective-propositional :
  ∀ {ℓ a b} {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (a ⊔ b ⊔ lsuc ℓ) (a ⊔ b ⊔ lsuc ℓ) →
  Is-proposition (Surjective ℓ f)
Surjective-propositional {ℓ} {a} ext =
  Π-closure (lower-extensionality (a ⊔ lsuc ℓ) lzero ext)  λ _ →
  truncation-has-correct-h-level 
    (lower-extensionality lzero (lsuc ℓ) ext)

-- Split surjective functions are surjective.

Split-surjective→Surjective :
  ∀ {a b ℓ} {A : Type a} {B : Type b} {f : A → B} →
  Split-surjective f → Surjective ℓ f
Split-surjective→Surjective s = λ b → ∣ s b ∣₁

-- Being both surjective and an embedding is equivalent to being an
-- equivalence.
--
-- This is Corollary 4.6.4 from the first edition of the HoTT book
-- (the proof is perhaps not quite identical).

surjective×embedding≃equivalence :
  ∀ {a b} ℓ {A : Type a} {B : Type b} {f : A → B} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (lsuc (a ⊔ b ⊔ ℓ)) →
  (Surjective (a ⊔ b ⊔ ℓ) f × Is-embedding f) ≃ Is-equivalence f
surjective×embedding≃equivalence {a} {b} ℓ {f} ext =
  Eq.⇔→≃
    (×-closure  (Surjective-propositional ext)
                 (Is-embedding-propositional
                    (lower-extensionality _ _ ext)))
    (Is-equivalence-propositional (lower-extensionality _ _ ext))
    (λ (is-surj , is-emb) →
       _⇔_.from HA.Is-equivalence⇔Is-equivalence-CP $ λ y →
                                  $⟨ is-surj y ⟩
       ∥ f ⁻¹ y ∥  (a ⊔ b ⊔ ℓ)   ↝⟨ with-lower-level ℓ  ⟩
       ∥ f ⁻¹ y ∥  (a ⊔ b)       ↝⟨ rec 
                                         (Contractible-propositional
                                            (lower-extensionality _ _ ext))
           (f ⁻¹ y                       ↝⟨ propositional⇒inhabited⇒contractible
                                              (embedding→⁻¹-propositional is-emb y) ⟩□
            Contractible (f ⁻¹ y)        □) ⟩□

       Contractible (f ⁻¹ y)      □)
    (λ is-eq →
         (λ y →                       $⟨ HA.inverse is-eq y
                                       , HA.right-inverse-of is-eq y
                                       ⟩
            f ⁻¹ y                    ↝⟨ ∣_∣₁ ⟩□
            ∥ f ⁻¹ y ∥  (a ⊔ b ⊔ ℓ)  □)

       ,                  ($⟨ is-eq ⟩
         Is-equivalence f  ↝⟨ Embedding.is-embedding ∘ from-equivalence ∘ Eq.⟨ _ ,_⟩ ⟩□
         Is-embedding f    □))

-- If the underlying type has a certain h-level, then there is a split
-- surjection from corresponding truncations (if they are "big"
-- enough) to the type itself.

∥∥↠ : ∀ ℓ {a} {A : Type a} n →
      H-level n A → ∥ A ∥ n (a ⊔ ℓ) ↠ A
∥∥↠ ℓ _ h = record
  { logical-equivalence = record
    { to   = rec _ h F.id ∘ with-lower-level ℓ _
    ; from = ∣_∣
    }
  ; right-inverse-of = refl
  }

-- If the underlying type is a proposition, then propositional
-- truncations of the type are isomorphic to the type itself (if they
-- are "big" enough, and assuming extensionality).

∥∥↔ : ∀ ℓ {a} {A : Type a} →
      Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ ℓ) →
      Is-proposition A → ∥ A ∥  (a ⊔ ℓ) ↔ A
∥∥↔ ℓ ext A-prop = record
  { surjection      = ∥∥↠ ℓ  A-prop
  ; left-inverse-of = λ _ →
      truncation-has-correct-h-level  ext _ _
  }

-- A simple isomorphism involving propositional truncation.

∥∥×↔ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  ∥ A ∥  ℓ × A ↔ A
∥∥×↔ {ℓ} {A} ext =
  ∥ A ∥  ℓ × A  ↝⟨ ×-comm ⟩
  A × ∥ A ∥  ℓ  ↝⟨ (drop-⊤-right λ a →
                     _⇔_.to contractible⇔↔⊤ $
                       propositional⇒inhabited⇒contractible
                         (truncation-has-correct-h-level  ext)
                         ∣ a ∣₁) ⟩□
  A              □

-- A variant of ∥∥×↔, introduced to ensure that the right-inverse-of
-- proof is, by definition, simple (see right-inverse-of-∥∥×≃ below).

∥∥×≃ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  (∥ A ∥  ℓ × A) ≃ A
∥∥×≃ ext = Eq.↔→≃
  proj₂
  (λ x → ∣ x ∣₁ , x)
  refl
  (λ _ → cong (_, _) (truncation-has-correct-h-level  ext _ _))

private

  right-inverse-of-∥∥×≃ :
    ∀ {ℓ a} {A : Type a}
    (ext : Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a)) (x : A) →
    _≃_.right-inverse-of (∥∥×≃ {ℓ = ℓ} ext) x ≡ refl x
  right-inverse-of-∥∥×≃ _ x = refl (refl x)

-- ∥_∥ commutes with _×_ (assuming extensionality and a resizing
-- function for the propositional truncation).

∥∥×∥∥↔∥×∥ :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  (∀ {x} {X : Type x} →
     ∥ X ∥        (a ⊔ b ⊔ ℓ) →
     ∥ X ∥  (lsuc (a ⊔ b ⊔ ℓ))) →
  let ℓ′ = a ⊔ b ⊔ ℓ in
  (∥ A ∥  ℓ′ × ∥ B ∥  ℓ′) ↔ ∥ A × B ∥  ℓ′
∥∥×∥∥↔∥×∥ _ ext resize = record
  { surjection = record
    { logical-equivalence = record
      { from = λ p → ∥∥-map  proj₁ p , ∥∥-map  proj₂ p
      ; to   = λ { (x , y) →
                   rec 
                       (truncation-has-correct-h-level  ext)
                       (λ x → rec 
                                  (truncation-has-correct-h-level  ext)
                                  (λ y → ∣ x , y ∣₁)
                                  (resize y))
                       (resize x) }
      }
    ; right-inverse-of = λ _ → truncation-has-correct-h-level  ext _ _
    }
  ; left-inverse-of = λ _ →
      ×-closure 
        (truncation-has-correct-h-level  ext)
        (truncation-has-correct-h-level  ext)
        _ _
  }

-- If A is merely inhabited (at a certain level), then the
-- propositional truncation of A (at the same level) is isomorphic to
-- the unit type (assuming extensionality).

inhabited⇒∥∥↔⊤ :
  ∀ {ℓ a} {A : Type a} →
  Extensionality (lsuc ℓ ⊔ a) (ℓ ⊔ a) →
  ∥ A ∥  ℓ → ∥ A ∥  ℓ ↔ ⊤
inhabited⇒∥∥↔⊤ ext ∥a∥ =
  _⇔_.to contractible⇔↔⊤ $
    propositional⇒inhabited⇒contractible
      (truncation-has-correct-h-level  ext)
      ∥a∥

-- If A is not inhabited, then the propositional truncation of A is
-- isomorphic to the empty type.

not-inhabited⇒∥∥↔⊥ :
  ∀ {ℓ₁ ℓ₂ a} {A : Type a} →
  ¬ A → ∥ A ∥  ℓ₁ ↔ ⊥ {ℓ = ℓ₂}
not-inhabited⇒∥∥↔⊥ {A} =
  ¬ A            ↝⟨ (λ ¬a ∥a∥ → rec  ⊥-propositional ¬a (with-lower-level _  ∥a∥)) ⟩
  ¬ ∥ A ∥  _    ↝⟨ inverse ∘ Bijection.⊥↔uninhabited ⟩□
  ∥ A ∥  _ ↔ ⊥  □

-- The following two results come from "Generalizations of Hedberg's
-- Theorem" by Kraus, Escardó, Coquand and Altenkirch.

-- Types with constant endofunctions are "h-stable" (meaning that
-- "mere inhabitance" implies inhabitance).

constant-endofunction⇒h-stable :
  ∀ {a} {A : Type a} {f : A → A} →
  Constant f → ∥ A ∥  a → A
constant-endofunction⇒h-stable {a} {A} {f} c =
  ∥ A ∥  a                ↝⟨ rec  (fixpoint-lemma f c) (λ x → f x , c (f x) x) ⟩
  (∃ λ (x : A) → f x ≡ x)  ↝⟨ proj₁ ⟩□
  A                        □

-- Having a constant endofunction is logically equivalent to being
-- h-stable (assuming extensionality).

constant-endofunction⇔h-stable :
  ∀ {a} {A : Type a} →
  Extensionality (lsuc a) a →
  (∃ λ (f : A → A) → Constant f) ⇔ (∥ A ∥  a → A)
constant-endofunction⇔h-stable ext = record
  { to = λ { (_ , c) → constant-endofunction⇒h-stable c }
  ; from = λ f → f ∘ ∣_∣₁ , λ x y →

      f ∣ x ∣₁  ≡⟨ cong f $ truncation-has-correct-h-level  ext _ _ ⟩∎
      f ∣ y ∣₁  ∎
  }

-- The following three lemmas were communicated to me by Nicolai
-- Kraus. (In slightly different form.) They are closely related to
-- Lemma 2.1 in his paper "The General Universal Property of the
-- Propositional Truncation".

-- A variant of ∥∥×≃.

drop-∥∥ :
  ∀ ℓ {a b} {A : Type a} {B : A → Type b} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →

  (∥ A ∥  (a ⊔ ℓ) → ∀ x → B x)
    ↔
  (∀ x → B x)
drop-∥∥ ℓ {a} {b} {A} {B} ext =

  (∥ A ∥  _ → ∀ x → B x)              ↝⟨ inverse currying ⟩

  ((p : ∥ A ∥  _ × A) → B (proj₂ p))  ↝⟨ Π-cong (lower-extensionality lzero (a ⊔ ℓ) ext)
                                                 (∥∥×≃ (lower-extensionality lzero b ext))
                                                 (λ _ → F.id) ⟩□
  (∀ x → B x)                          □

-- Another variant of ∥∥×≃.

push-∥∥ :
  ∀ ℓ {a b c} {A : Type a} {B : A → Type b} {C : (∀ x → B x) → Type c} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ c ⊔ ℓ) →

  (∥ A ∥  (a ⊔ ℓ) → ∃ λ (f : ∀ x → B x) → C f)
    ↔
  (∃ λ (f : ∀ x → B x) → ∥ A ∥  (a ⊔ ℓ) → C f)

push-∥∥ ℓ {a} {b} {c} {A} {B} {C} ext =

  (∥ A ∥  _ → ∃ λ (f : ∀ x → B x) → C f)                ↝⟨ ΠΣ-comm ⟩

  (∃ λ (f : ∥ A ∥  _ → ∀ x → B x) → ∀ ∥x∥ → C (f ∥x∥))  ↝⟨ Σ-cong (drop-∥∥ ℓ (lower-extensionality lzero c ext)) (λ f →
                                                            ∀-cong (lower-extensionality lzero (a ⊔ b ⊔ ℓ) ext) λ ∥x∥ →
                                                            ≡⇒↝ _ $ cong C $ apply-ext (lower-extensionality _ (a ⊔ c ⊔ ℓ) ext) λ x →
      f ∥x∥ x                                                 ≡⟨ cong (λ ∥x∥ → f ∥x∥ x) $
                                                                 truncation-has-correct-h-level 
                                                                   (lower-extensionality lzero (b ⊔ c) ext)
                                                                   _ _ ⟩
      f ∣ x ∣₁ x                                              ≡⟨ sym $ subst-refl _ _ ⟩∎

      subst B (refl x) (f ∣ x ∣₁ x)                           ∎) ⟩□

  (∃ λ (f : ∀ x → B x) → ∥ A ∥  _ → C (λ x → f x))      □

-- This is an instance of a variant of Lemma 2.1 from "The General
-- Universal Property of the Propositional Truncation" by Kraus.

drop-∥∥₃ :
  ∀ ℓ {a b c d}
    {A : Type a} {B : A → Type b} {C : A → (∀ x → B x) → Type c}
    {D : A → (f : ∀ x → B x) → (∀ x → C x f) → Type d} →
  Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ b ⊔ c ⊔ d ⊔ ℓ) →

  (∥ A ∥  (a ⊔ ℓ) →
   ∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)
    ↔
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)

drop-∥∥₃ ℓ {b} {c} {A} {B} {C} {D} ext =
  (∥ A ∥  _ →
   ∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)  ↝⟨ push-∥∥ ℓ ext ⟩

  (∃ λ (f : ∀ x → B x) →
   ∥ A ∥  _ → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)            ↝⟨ (∃-cong λ _ →
                                                                     push-∥∥ ℓ (lower-extensionality lzero b ext)) ⟩
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) →
   ∥ A ∥  _ → ∀ x → D x f g)                                    ↝⟨ (∃-cong λ _ → ∃-cong λ _ →
                                                                     drop-∥∥ ℓ (lower-extensionality lzero (b ⊔ c) ext)) ⟩□
  (∃ λ (f : ∀ x → B x) → ∃ λ (g : ∀ x → C x f) → ∀ x → D x f g)  □

-- Having a coherently constant function into a groupoid is equivalent
-- to having a function from a propositionally truncated type into the
-- groupoid (assuming extensionality). This result is Proposition 2.3
-- in "The General Universal Property of the Propositional Truncation"
-- by Kraus.

Coherently-constant :
  ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Coherently-constant f =
  ∃ λ (c : Constant f) →
  ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃

coherently-constant-function≃∥inhabited∥⇒inhabited :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  H-level  B →
  (∃ λ (f : A → B) → Coherently-constant f) ≃ (∥ A ∥  (a ⊔ b ⊔ ℓ) → B)
coherently-constant-function≃∥inhabited∥⇒inhabited {a} {b} ℓ {A} {B}
                                                   ext B-groupoid =
  (∃ λ (f : A → B) → Coherently-constant f)               ↔⟨ inverse $ drop-∥∥₃ (b ⊔ ℓ) ext ⟩
  (∥ A ∥  ℓ′ → ∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ ∀-cong (lower-extensionality lzero ℓ ext) (inverse ∘ equivalence₂) ⟩□
  (∥ A ∥  ℓ′ → B)                                        □
  where
  ℓ′ = a ⊔ b ⊔ ℓ

  rearrangement-lemma = λ a₀ →
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ ∃-comm ⟩

    (∃ λ (f : A → B) →
     ∃ λ (f₁ : B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) →
     ∃ λ (f₁ : B) →
     ∃ λ (c : Constant f) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (f₁ : B) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-comm) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                     ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                           ∃-cong λ _ → ∃-comm) ⟩□
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                     □

  equivalence₁ : A → (B ≃ ∃ λ (f : A → B) → Coherently-constant f)
  equivalence₁ a₀ = Eq.↔⇒≃ (
    B                                                                    ↝⟨ (inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     (a : A) → ∃ λ (b : B) → b ≡ f₁)                                     ↝⟨ (∃-cong λ _ → ΠΣ-comm) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → (a : A) → f a ≡ f₁)                               ↝⟨ (∃-cong λ _ → ∃-cong λ _ → inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ a₂ → ∃ λ (c : f a₁ ≡ f a₂) → c ≡ trans (c₁ a₁) (sym (c₁ a₂)))  ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ ℓ       ext) λ _ →
                                                                             ∀-cong (lower-extensionality _ (a ⊔ ℓ) ext) λ _ →
                                                                             ∃-cong λ _ → ≡⇒↝ _ $ sym $ [trans≡]≡[≡trans-symʳ] _ _ _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ a₂ → ∃ λ (c : f a₁ ≡ f a₂) → trans c (c₁ a₂) ≡ c₁ a₁)          ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ ℓ ext) λ _ →
                                                                             ΠΣ-comm) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∀ a₁ → ∃ λ (c : ∀ a₂ → f a₁ ≡ f a₂) →
            ∀ a₂ → trans (c a₂) (c₁ a₂) ≡ c₁ a₁)                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ΠΣ-comm) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) → ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁)   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               other-singleton-contractible _) ⟩
    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ c₁ → ∃-cong λ c → ∃-cong λ d₁ →
                                                                             ∃-cong λ _ → inverse $ drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                 (Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                                                  Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                                                  Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                                  B-groupoid)
                                                                                 (λ a₁ a₂ a₃ →
         trans (c a₁ a₂) (c a₂ a₃)                                                  ≡⟨ cong₂ trans (≡⇒↝ implication
                                                                                                        ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _))
                                                                                                   (≡⇒↝ implication
                                                                                                        ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _)) ⟩
         trans (trans (c₁ a₁) (sym (c₁ a₂)))
               (trans (c₁ a₂) (sym (c₁ a₃)))                                        ≡⟨ sym $ trans-assoc _ _ _ ⟩

         trans (trans (trans (c₁ a₁) (sym (c₁ a₂))) (c₁ a₂))
               (sym (c₁ a₃))                                                        ≡⟨ cong (flip trans _) $ trans-[trans-sym]- _ _ ⟩

         trans (c₁ a₁) (sym (c₁ a₃))                                                ≡⟨ sym $ ≡⇒↝ implication
                                                                                                 ([trans≡]≡[≡trans-symʳ] _ _ _) (d₁ _ _) ⟩∎
         c a₁ a₃                                                                    ∎)) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃)                   ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ c₁ → ∃-cong λ c → ∃-cong λ d₁ →
                                                                             ∃-cong λ c₂ → ∃-cong λ d₃ → inverse $ drop-⊤-right λ d →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                 (Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                                  B-groupoid)
                                                                                 (λ a →
         trans (c a₀ a) (c₁ a)                                                      ≡⟨ cong (λ x → trans x _) $ sym $ d _ _ _ ⟩
         trans (trans (c a₀ a₀) (c a₀ a)) (c₁ a)                                    ≡⟨ trans-assoc _ _ _ ⟩
         trans (c a₀ a₀) (trans (c a₀ a) (c₁ a))                                    ≡⟨ cong (trans _) $ d₁ _ _ ⟩
         trans (c a₀ a₀) (c₁ a₀)                                                    ≡⟨ d₃ ⟩∎
         c₂                                                                         ∎)) ⟩

    (∃ λ (f₁ : B) →
     ∃ λ (f : A → B) → ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (c : Constant f) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     ∃ λ (c₂ : f a₀ ≡ f₁) → ∃ λ (d₃ : trans (c a₀ a₀) (c₁ a₀) ≡ c₂) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                               ↝⟨ rearrangement-lemma a₀ ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∃ λ (d₁ : ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁) →
     trans (c a₀ a₀) (c₁ a₀) ≡ c₂)                                       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∃-cong λ _ → ∃-cong λ d₂ → drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                 (B-groupoid)
                                                                                 (d₂ _)) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     ∃ λ (d₂ : (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂) →
     ∀ a₁ a₂ → trans (c a₁ a₂) (c₁ a₂) ≡ c₁ a₁)                          ↝⟨ (∃-cong λ _ → ∃-cong λ c → ∃-cong λ d → ∃-cong λ _ → ∃-cong λ c₂ →
                                                                             ∃-cong λ c₁ → drop-⊤-right λ d₂ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               propositional⇒inhabited⇒contractible
                                                                                 (Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                                                  Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                                  B-groupoid)
                                                                                 (λ a₁ a₂ →
         trans (c a₁ a₂) (c₁ a₂)                                                    ≡⟨ cong₂ trans (sym $ d _ _ _)
                                                                                                   (≡⇒↝ implication
                                                                                                        ([trans≡]≡[≡trans-symˡ] _ _ _) (d₂ _)) ⟩
         trans (trans (c a₁ a₀) (c a₀ a₂)) (trans (sym (c a₀ a₂)) c₂)               ≡⟨ sym $ trans-assoc _ _ _ ⟩
         trans (trans (trans (c a₁ a₀) (c a₀ a₂)) (sym (c a₀ a₂))) c₂               ≡⟨ cong (flip trans _) $ trans-[trans]-sym _ _ ⟩
         trans (c a₁ a₀) c₂                                                         ≡⟨ cong (trans _) $ sym $ d₂ _ ⟩
         trans (c a₁ a₀) (trans (c a₀ a₁) (c₁ a₁))                                  ≡⟨ sym $ trans-assoc _ _ _ ⟩
         trans (trans (c a₁ a₀) (c a₀ a₁)) (c₁ a₁)                                  ≡⟨ cong (flip trans _) $ d _ _ _ ⟩
         trans (c a₁ a₁) (c₁ a₁)                                                    ≡⟨ cong (flip trans _) $
                                                                                         Groupoid.idempotent⇒≡id (EG.groupoid _) (d _ _ _) ⟩
         trans (refl _) (c₁ a₁)                                                     ≡⟨ trans-reflˡ _ ⟩∎
         c₁ a₁                                                                      ∎)) ⟩

    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     ∃ λ (c₁ : (a : A) → f a ≡ f₁) →
     (a : A) → trans (c a₀ a) (c₁ a) ≡ c₂)                               ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             inverse ΠΣ-comm) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     (a : A) → ∃ λ (c₁ : f a ≡ f₁) → trans (c a₀ a) c₁ ≡ c₂)             ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             ∀-cong (lower-extensionality _ (a ⊔ ℓ) ext) λ _ → ∃-cong λ _ →
                                                                             ≡⇒↝ _ $ [trans≡]≡[≡trans-symˡ] _ _ _) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → ∃ λ (c₂ : f a₀ ≡ f₁) →
     (a : A) → ∃ λ (c₁ : f a ≡ f₁) → c₁ ≡ trans (sym (c a₀ a)) c₂)       ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ → ∃-cong λ _ →
                                                                             drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                                               singleton-contractible _) ⟩
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∃ λ (d : ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃) →
     ∃ λ (f₁ : B) → f a₀ ≡ f₁)                                           ↝⟨ (∃-cong λ _ → ∃-cong λ _ → drop-⊤-right λ _ →
                                                                             _⇔_.to contractible⇔↔⊤ $
                                                                               other-singleton-contractible _) ⟩□
    (∃ λ (f : A → B) → ∃ λ (c : Constant f) →
     ∀ a₁ a₂ a₃ → trans (c a₁ a₂) (c a₂ a₃) ≡ c a₁ a₃)                   □)

  -- An alternative implementation of the forward component of the
  -- equivalence above (with shorter proofs).

  to : B → ∃ λ (f : A → B) → Coherently-constant f
  to b =
      (λ _ → b)
    , (λ _ _ → refl b)
    , (λ _ _ _ → trans-refl-refl)

  to-is-an-equivalence : A → Is-equivalence to
  to-is-an-equivalence a₀ =
    Eq.respects-extensional-equality
      {f = _≃_.to (equivalence₁ a₀)}
      (λ b →
         Σ-≡,≡→≡ (refl _) $
         Σ-≡,≡→≡
           (proj₁ (subst Coherently-constant
                         (refl _)
                         (proj₂ (_≃_.to (equivalence₁ a₀) b)))  ≡⟨ cong proj₁ $ subst-refl Coherently-constant _ ⟩

            (λ _ _ → trans (refl b) (sym (refl b)))             ≡⟨ (apply-ext (lower-extensionality _ ℓ       ext) λ _ →
                                                                    apply-ext (lower-extensionality _ (a ⊔ ℓ) ext) λ _ →
                                                                    trans-symʳ _) ⟩∎
            (λ _ _ → refl b)                                    ∎)
           ((Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
             Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
             Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
             B-groupoid) _ _))
      (_≃_.is-equivalence (equivalence₁ a₀))

  -- The forward component of the equivalence above does not depend on
  -- the value a₀ of type A, so it suffices to assume that A is merely
  -- inhabited.

  equivalence₂ :
    ∥ A ∥  ℓ′ → (B ≃ ∃ λ (f : A → B) → Coherently-constant f)
  equivalence₂ ∥a∥ =
    Eq.⟨ to
       , rec 
             (Is-equivalence-propositional
                (lower-extensionality _ ℓ ext))
             to-is-an-equivalence
             (with-lower-level ℓ  ∥a∥)
       ⟩

-- Having a constant function into a set is equivalent to having a
-- function from a propositionally truncated type into the set
-- (assuming extensionality). The statement of this result is that of
-- Proposition 2.2 in "The General Universal Property of the
-- Propositional Truncation" by Kraus, but it uses a different proof:
-- as observed by Kraus this result follows from Proposition 2.3.

constant-function≃∥inhabited∥⇒inhabited :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  Is-set B →
  (∃ λ (f : A → B) → Constant f) ≃ (∥ A ∥  (a ⊔ b ⊔ ℓ) → B)
constant-function≃∥inhabited∥⇒inhabited {a} {b} ℓ {A} {B} ext B-set =
  (∃ λ (f : A → B) → Constant f)             ↔⟨ (∃-cong λ f → inverse $ drop-⊤-right λ c →
                                                 _⇔_.to contractible⇔↔⊤ $
                                                   Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                   Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                                   Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                                   +⇒≡ B-set) ⟩
  (∃ λ (f : A → B) → Coherently-constant f)  ↝⟨ coherently-constant-function≃∥inhabited∥⇒inhabited ℓ ext (mono₁  B-set) ⟩□
  (∥ A ∥  (a ⊔ b ⊔ ℓ) → B)                  □

private

  -- One direction of the proposition above computes in the right way.

  to-constant-function≃∥inhabited∥⇒inhabited :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-set : Is-set B)
    (f : ∃ λ (f : A → B) → Constant f) (x : A) →
    _≃_.to (constant-function≃∥inhabited∥⇒inhabited ℓ ext B-set)
      f ∣ x ∣₁ ≡ proj₁ f x
  to-constant-function≃∥inhabited∥⇒inhabited _ _ _ _ _ = refl _

-- The propositional truncation's universal property (defined using
-- extensionality).
--
-- As observed by Kraus this result follows from Proposition 2.2 in
-- his "The General Universal Property of the Propositional
-- Truncation".

universal-property :
  ∀ {a b} ℓ {A : Type a} {B : Type b} →
  Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ) →
  Is-proposition B →
  (∥ A ∥  (a ⊔ b ⊔ ℓ) → B) ≃ (A → B)
universal-property {a} {b} ℓ {A} {B} ext B-prop =
  Eq.with-other-function
    ((∥ A ∥  (a ⊔ b ⊔ ℓ) → B)       ↝⟨ inverse $ constant-function≃∥inhabited∥⇒inhabited ℓ ext (mono₁  B-prop) ⟩
     (∃ λ (f : A → B) → Constant f)  ↔⟨ (drop-⊤-right λ _ →
                                         _⇔_.to contractible⇔↔⊤ $
                                         Π-closure (lower-extensionality _ ℓ       ext)  λ _ →
                                         Π-closure (lower-extensionality _ (a ⊔ ℓ) ext)  λ _ →
                                         +⇒≡ B-prop) ⟩□
     (A → B)                         □)

    (_∘ ∣_∣₁)

    (λ f → apply-ext (lower-extensionality _ (a ⊔ ℓ) ext) λ x →
       subst (const B) (refl x) (f ∣ x ∣₁)  ≡⟨ subst-refl _ _ ⟩∎
       f ∣ x ∣₁                             ∎)

private

  -- The universal property computes in the right way.

  to-universal-property :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-prop : Is-proposition B)
    (f : ∥ A ∥  (a ⊔ b ⊔ ℓ) → B) →
    _≃_.to (universal-property ℓ ext B-prop) f ≡ f ∘ ∣_∣₁
  to-universal-property _ _ _ _ = refl _

  from-universal-property :
    ∀ {a b} ℓ {A : Type a} {B : Type b}
    (ext : Extensionality (lsuc (a ⊔ b ⊔ ℓ)) (a ⊔ b ⊔ ℓ))
    (B-prop : Is-proposition B)
    (f : A → B) (x : A) →
    _≃_.from (universal-property ℓ ext B-prop) f ∣ x ∣₁ ≡ f x
  from-universal-property _ _ _ _ _ = refl _

-- Some properties of an imagined "real" /propositional/ truncation.

module Real-propositional-truncation
  (∥_∥ʳ : ∀ {a} → Type a → Type a)
  (∣_∣ʳ : ∀ {a} {A : Type a} → A → ∥ A ∥ʳ)
  (truncation-is-proposition :
     ∀ {a} {A : Type a} → Is-proposition ∥ A ∥ʳ)
  (recʳ :
    ∀ {a b} {A : Type a} {B : Type b} →
    Is-proposition B →
    (A → B) → ∥ A ∥ʳ → B)
  where

  -- The function recʳ can be used to define a dependently typed
  -- eliminator (assuming extensionality).

  elimʳ :
    ∀ {a p} {A : Type a} →
    Extensionality a p →
    (P : ∥ A ∥ʳ → Type p) →
    (∀ x → Is-proposition (P x)) →
    ((x : A) → P ∣ x ∣ʳ) →
    (x : ∥ A ∥ʳ) → P x
  elimʳ {A} ext P P-prop f x =
    recʳ {A = A}
         {B = ∀ x → P x}
         (Π-closure ext  P-prop)
         (λ x _ → subst P
                        (truncation-is-proposition _ _)
                        (f x))
         x
         x

  -- The eliminator gives the right result, up to propositional
  -- equality, when applied to ∣ x ∣ʳ.

  elimʳ-∣∣ʳ :
    ∀ {a p} {A : Type a}
    (ext : Extensionality a p)
    (P : ∥ A ∥ʳ → Type p)
    (P-prop : ∀ x → Is-proposition (P x))
    (f : (x : A) → P ∣ x ∣ʳ)
    (x : A) →
    elimʳ ext P P-prop f ∣ x ∣ʳ ≡ f x
  elimʳ-∣∣ʳ ext P P-prop f x =
    P-prop _ _ _

  -- The "real" propositional truncation is isomorphic to the one
  -- defined above (assuming extensionality).

  isomorphic :
    ∀ {ℓ a} {A : Type a} →
    Extensionality (lsuc (a ⊔ ℓ)) (a ⊔ ℓ) →
    ∥ A ∥ʳ ↔ ∥ A ∥  (a ⊔ ℓ)
  isomorphic {ℓ} ext = record
    { surjection = record
      { logical-equivalence = record
        { to   = recʳ (truncation-has-correct-h-level  ext) ∣_∣₁
        ; from = lower {ℓ = ℓ} ∘
                 rec 
                     (↑-closure  truncation-is-proposition)
                     (lift ∘ ∣_∣ʳ)
        }
      ; right-inverse-of = λ _ →
          truncation-has-correct-h-level  ext _ _
      }
    ; left-inverse-of = λ _ → truncation-is-proposition _ _
    }

-- The axiom of choice, in one of the alternative forms given in the
-- HoTT book (§3.8).
--
-- The HoTT book uses a "real" propositional truncation, rather than
-- the defined one used here. Note that I don't know if the universe
-- levels used below (b ⊔ ℓ and a ⊔ b ⊔ ℓ) make sense. However, in the
-- presence of a "real" propositional truncation (and extensionality)
-- they can be dropped (see Real-propositional-truncation.isomorphic).

Axiom-of-choice : (a b ℓ : Level) → Type (lsuc (a ⊔ b ⊔ ℓ))
Axiom-of-choice a b ℓ =
  {A : Type a} {B : A → Type b} →
  Is-set A → (∀ x → ∥ B x ∥  (b ⊔ ℓ)) → ∥ (∀ x → B x) ∥  (a ⊔ b ⊔ ℓ)