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 βˆ₯β‚€

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)
  module βˆ₯-βˆ₯β‚€-idempotent 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})