open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.HIT.Truncation
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module Data.Set.Truncation where

Set truncationπŸ”—

Exactly analogously to the construction of propositional truncations, we can construct the set truncation of a type, reflecting it onto the subcategory of sets. Just like the propositional truncation is constructed by attaching enough lines to a type to hide away all information other than β€œis the type inhabited”, the set truncation is constructed by attaching enough square to kill off all homotopy groups.

data βˆ₯_βˆ₯β‚€ {β„“} (A : Type β„“) : Type β„“ where
  inc    : A β†’ βˆ₯ A βˆ₯β‚€
  squash : is-set βˆ₯ A βˆ₯β‚€

instance
  H-Level-βˆ₯-βˆ₯β‚€ : βˆ€ {n} {β„“} {A : Type β„“} β†’ H-Level βˆ₯ A βˆ₯β‚€ (suc (suc n))
  H-Level-βˆ₯-βˆ₯β‚€ = basic-instance 2 squash

We begin by defining the induction principle. The (family of) type(s) we map into must be a set, as required by the squash constructor.

βˆ₯-βˆ₯β‚€-elim : βˆ€ {β„“ β„“'} {A : Type β„“} {B : βˆ₯ A βˆ₯β‚€ β†’ Type β„“'}
          β†’ (βˆ€ x β†’ is-set (B x))
          β†’ (βˆ€ x β†’ B (inc x))
          β†’ βˆ€ x β†’ B x
βˆ₯-βˆ₯β‚€-elim Bset binc (inc x) = binc x
βˆ₯-βˆ₯β‚€-elim Bset binc (squash x y p q i j) =
  is-set→squarep (λ i j → Bset (squash x y p q i j))
    (Ξ» _ β†’ g x) (Ξ» i β†’ g (p i)) (Ξ» i β†’ g (q i)) (Ξ» i β†’ g y) i j
  where g = βˆ₯-βˆ₯β‚€-elim Bset binc

βˆ₯-βˆ₯β‚€-rec
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ is-set B
  β†’ (A β†’ B) β†’ βˆ₯ A βˆ₯β‚€ β†’ B
βˆ₯-βˆ₯β‚€-rec bset f (inc x) = f x
βˆ₯-βˆ₯β‚€-rec bset f (squash x y p q i j) =
  bset (go x) (go y) (Ξ» i β†’ go (p i)) (Ξ» i β†’ go (q i)) i j
  where go = βˆ₯-βˆ₯β‚€-rec bset f

The most interesting result is that, since the sets form a reflective subcategory of types, the set-truncation is an idempotent monad. Indeed, as required, the counit inc is an equivalence:

βˆ₯-βˆ₯β‚€-idempotent : βˆ€ {β„“} {A : Type β„“} β†’ is-set A
                β†’ is-equiv (inc {A = A})
βˆ₯-βˆ₯β‚€-idempotent {A = A} aset = is-isoβ†’is-equiv (iso proj inc∘proj Ξ» _ β†’ refl)
  where
    proj : βˆ₯ A βˆ₯β‚€ β†’ A
    proj (inc x) = x
    proj (squash x y p q i j) =
      aset (proj x) (proj y) (Ξ» i β†’ proj (p i)) (Ξ» i β†’ proj (q i)) i j

    inc∘proj : (x : βˆ₯ A βˆ₯β‚€) β†’ inc (proj x) ≑ x
    inc∘proj = βˆ₯-βˆ₯β‚€-elim (Ξ» _ β†’ is-propβ†’is-set (squash _ _)) Ξ» _ β†’ refl

The other definitions are entirely routine. We define functorial actions of βˆ₯_βˆ₯β‚€ directly, rather than using the eliminator, to avoid using is-setβ†’squarep.

βˆ₯-βˆ₯β‚€-map : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
        β†’ (A β†’ B) β†’ βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€
βˆ₯-βˆ₯β‚€-map f (inc x)        = inc (f x)
βˆ₯-βˆ₯β‚€-map f (squash x y p q i j) =
  squash (βˆ₯-βˆ₯β‚€-map f x) (βˆ₯-βˆ₯β‚€-map f y)
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-map f (p i))
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-map f (q i))
         i j

βˆ₯-βˆ₯β‚€-mapβ‚‚ : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“'} {C : Type β„“''}
          β†’ (A β†’ B β†’ C) β†’ βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€ β†’ βˆ₯ C βˆ₯β‚€
βˆ₯-βˆ₯β‚€-mapβ‚‚ f (inc x) (inc y)        = inc (f x y)
βˆ₯-βˆ₯β‚€-mapβ‚‚ f (squash x y p q i j) b =
  squash (βˆ₯-βˆ₯β‚€-mapβ‚‚ f x b) (βˆ₯-βˆ₯β‚€-mapβ‚‚ f y b)
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-mapβ‚‚ f (p i) b)
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-mapβ‚‚ f (q i) b)
         i j
βˆ₯-βˆ₯β‚€-mapβ‚‚ f a (squash x y p q i j) =
  squash (βˆ₯-βˆ₯β‚€-mapβ‚‚ f a x) (βˆ₯-βˆ₯β‚€-mapβ‚‚ f a y)
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-mapβ‚‚ f a (p i))
         (Ξ» i β†’ βˆ₯-βˆ₯β‚€-mapβ‚‚ f a (q i))
         i j

βˆ₯-βˆ₯β‚€-elimβ‚‚ : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“'} {C : βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€ β†’ Type β„“''}
           β†’ (βˆ€ x y β†’ is-set (C x y))
           β†’ (βˆ€ x y β†’ C (inc x) (inc y))
           β†’ βˆ€ x y β†’ C x y
βˆ₯-βˆ₯β‚€-elimβ‚‚ Bset f = βˆ₯-βˆ₯β‚€-elim (Ξ» x β†’ Ξ -is-hlevel 2 (Bset x))
  Ξ» x β†’ βˆ₯-βˆ₯β‚€-elim (Bset (inc x)) (f x)

βˆ₯-βˆ₯β‚€-elim₃ : βˆ€ {β„“ β„“' β„“'' β„“'''} {A : Type β„“} {B : Type β„“'} {C : Type β„“''}
               {D : βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€ β†’ βˆ₯ C βˆ₯β‚€ β†’ Type β„“'''}
           β†’ (βˆ€ x y z β†’ is-set (D x y z))
           β†’ (βˆ€ x y z β†’ D (inc x) (inc y) (inc z))
           β†’ βˆ€ x y z β†’ D x y z
βˆ₯-βˆ₯β‚€-elim₃ Bset f = βˆ₯-βˆ₯β‚€-elimβ‚‚ (Ξ» x y β†’ Ξ -is-hlevel 2 (Bset x y))
  Ξ» x y β†’ βˆ₯-βˆ₯β‚€-elim (Bset (inc x) (inc y)) (f x y)

Paths in the set truncationπŸ”—

βˆ₯-βˆ₯β‚€-path-equiv
  : βˆ€ {β„“} {A : Type β„“} {x y : A}
  β†’ (βˆ₯_βˆ₯β‚€.inc x ≑ βˆ₯_βˆ₯β‚€.inc y) ≃ βˆ₯ x ≑ y βˆ₯
βˆ₯-βˆ₯β‚€-path-equiv {A = A} =
  prop-ext (squash _ _) squash (encode _ _) (decode _ (inc _))
  where
    code : βˆ€ x (y : βˆ₯ A βˆ₯β‚€) β†’ Prop _
    code x = βˆ₯-βˆ₯β‚€-elim (Ξ» y β†’ hlevel 2) Ξ» y β†’ el βˆ₯ x ≑ y βˆ₯ squash

    encode : βˆ€ x y β†’ inc x ≑ y β†’ ∣ code x y ∣
    encode x y p = J (Ξ» y p β†’ ∣ code x y ∣) (inc refl) p

    decode : βˆ€ x y β†’ ∣ code x y ∣ β†’ inc x ≑ y
    decode x = βˆ₯-βˆ₯β‚€-elim
      (λ _ → fun-is-hlevel 2 (is-prop→is-set (squash _ _)))
      Ξ» _ β†’ βˆ₯-βˆ₯-rec (squash _ _) (ap inc)

module βˆ₯-βˆ₯β‚€-path {β„“} {A : Type β„“} {x} {y}
  = Equiv (βˆ₯-βˆ₯β‚€-path-equiv {A = A} {x} {y})