{-

This file contains:

- Properties of set truncations

-}
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.SetTruncation.Properties where

open import Cubical.Core.Glue

open import Cubical.HITs.SetTruncation.Base

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels

private
  variable
    ℓ : Level
    A : Set ℓ

elimSquash₀ : {B : A → Set ℓ} →
              (Bset : (x : A ) → isSet (B x)) →
              {x y : A } {p q : x ≡ y} (sq : p ≡ q) → ∀ bx by bp bq →
              PathP (λ i → PathP (λ j → B (sq i j)) bx by) bp bq
elimSquash₀ {A = A} {B = B} Bset {p = p} =
  J (λ q sq → ∀ bx by bp bq →
    PathP (λ i → PathP (λ j → B (sq i j)) bx by) bp bq) (BsetOver' p)
    where
    BsetOver' : {x y : A } → (p : x ≡ y) → ∀ bx by bp bp' → bp ≡ bp'
    BsetOver' {x = x} = J (λ y (p : x ≡ y) → ∀ bx by →
      (bp bp' : PathP (λ i → B (p i)) bx by) → bp ≡ bp') (Bset x)

-- lemma 6.9.1 in HoTT book
elimSetTrunc : {B : ∥ A ∥₀ → Set ℓ} →
               (Bset : (x : ∥ A ∥₀) → isSet (B x)) →
               (g : (a : A) → B (∣ a ∣₀)) →
               (x : ∥ A ∥₀) → B x
elimSetTrunc Bset g ∣ a ∣₀ = g a
elimSetTrunc {A = A} {B = B} Bset g (squash₀ x y p q i j) =
  elimSquash₀ Bset (squash₀ x y p q) (elimSetTrunc Bset g x) (elimSetTrunc Bset g y)
    (cong (elimSetTrunc Bset g) p) (cong (elimSetTrunc Bset g) q) i j

setTruncUniversal : {B : Set ℓ} → (isSet B) → (∥ A ∥₀ → B) ≃ (A → B)
setTruncUniversal Bset = isoToEquiv (iso intro elim leftInv rightInv)
  where
  intro = (λ h a → h ∣ a ∣₀)
  elim = elimSetTrunc (λ x → Bset)

  leftInv : ∀ g → intro (elim g) ≡ g
  leftInv g = refl

  rightInv : ∀ h → elim (intro h) ≡ h
  rightInv h i x = elimSetTrunc (λ x → isProp→isSet (Bset (elim (intro h) x) (h x)))
                                (λ a → refl) x i

elimSetTrunc2 : {B : ∥ A ∥₀ → ∥ A ∥₀ → Set ℓ}
                (Bset : ((x y : ∥ A ∥₀) → isSet (B x y)))
                (g : (a b : A) → B ∣ a ∣₀ ∣ b ∣₀)
                (x y : ∥ A ∥₀) → B x y
elimSetTrunc2 Bset g = elimSetTrunc (λ _ → hLevelPi  (λ _ → Bset _ _)) (λ a →
                       elimSetTrunc (λ _ → Bset _ _) (λ b → g a b))

elimSetTrunc3 : {B : (x y z : ∥ A ∥₀) → Set ℓ}
                (Bset : ((x y z : ∥ A ∥₀) → isSet (B x y z)))
                (g : (a b c : A) → B ∣ a ∣₀ ∣ b ∣₀ ∣ c ∣₀)
                (x y z : ∥ A ∥₀) → B x y z
elimSetTrunc3 Bset g = elimSetTrunc2 (λ _ _ → hLevelPi  λ _ → Bset _ _ _) (λ a b →
                       elimSetTrunc (λ _ → Bset _ _ _) (λ c → g a b c))