Tom de Jong, 4 & 5 April 2022.

Assuming set quotients, we derive propositional truncations in the
presence of function extensionality.

\begin{code}

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

module Quotient.GivesPropTrunc where

open import MLTT.Spartan

open import Quotient.Type

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

module _ (sq : set-quotients-exist) where

 open general-set-quotients-exist sq

 private
  module _ {X : 𝓤 ̇ } where
   _≈_ : X → X → 𝓤₀ ̇
   x ≈ y = 𝟙
   ≋ : EqRel X
   ≋ = _≈_ , (λ x y → 𝟙-is-prop) , (λ x → ⋆) , (λ x y _ → ⋆) , (λ x y z _ _ → ⋆)

  ∥_∥ : 𝓤 ̇ → 𝓤 ̇
  ∥_∥ X = X / ≋

  ∣_∣ : {X : 𝓤 ̇ } → X → ∥ X ∥
  ∣_∣ = η/ ≋

  ∥∥-is-prop : {X : 𝓤 ̇ } → funext 𝓤 𝓤 → is-prop ∥ X ∥
  ∥∥-is-prop {𝓤} {X} fe = /-induction ≋ (λ x' → Π-is-prop fe (λ y' → /-is-set ≋))
                           (λ x → /-induction ≋ (λ y' → /-is-set ≋)
                                  (λ y → η/-identifies-related-points ≋ ⋆))

  ∥∥-rec : {X : 𝓤 ̇ } {P : 𝓥 ̇ } → is-prop P → (X → P) → ∥ X ∥ → P
  ∥∥-rec {𝓤} {𝓥} {X} {P} i f =
   ∃!-witness (/-universality ≋ (props-are-sets i) f
                              (λ {x} {x'}_ → i (f x) (f x')))

 abstract
  propositional-truncations-from-set-quotients :
   Fun-Ext → propositional-truncations-exist
  propositional-truncations-from-set-quotients fe = record
   { ∥_∥        = ∥_∥
   ; ∥∥-is-prop = ∥∥-is-prop fe
   ; ∣_∣        = ∣_∣
   ; ∥∥-rec     = ∥∥-rec
   }

\end{code}