open import 1Lab.Path.IdentitySystem
open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Universe
open import 1Lab.HLevel.Closure
open import 1Lab.Type.Pointed
open import 1Lab.Truncation
open import 1Lab.Inductive
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Meta.Idiom
open import Meta.Bind
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
instance
  Inductive-βˆ₯βˆ₯β‚€
    : βˆ€ {β„“ β„“' β„“m} {A : Type β„“} {P : βˆ₯ A βˆ₯β‚€ β†’ Type β„“'} ⦃ i : Inductive (βˆ€ x β†’ P (inc x)) β„“m ⦄
    β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) 2 ⦄
    β†’ Inductive (βˆ€ x β†’ P x) β„“m
  Inductive-βˆ₯βˆ₯β‚€ ⦃ i ⦄ = record
    { methods = i .Inductive.methods
    ; from    = Ξ» f β†’ βˆ₯-βˆ₯β‚€-elim (Ξ» x β†’ hlevel 2) (i .Inductive.from 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

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})
instance
  H-Level-βˆ₯-βˆ₯β‚€ : βˆ€ {β„“} {A : Type β„“} {n : Nat} β†’ H-Level βˆ₯ A βˆ₯β‚€ (2 + n)
  H-Level-βˆ₯-βˆ₯β‚€ {n = n} = basic-instance 2 squash

  Map-βˆ₯βˆ₯β‚€ : Map (eff βˆ₯_βˆ₯β‚€)
  Map-βˆ₯βˆ₯β‚€ .Map.map = βˆ₯-βˆ₯β‚€-map

  Idiom-βˆ₯βˆ₯β‚€ : Idiom (eff βˆ₯_βˆ₯β‚€)
  Idiom-βˆ₯βˆ₯β‚€ .Idiom.pure = inc
  Idiom-βˆ₯βˆ₯β‚€ .Idiom._<*>_ {A = A} {B = B} = go where
    go : βˆ₯ (A β†’ B) βˆ₯β‚€ β†’ βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€
    go (inc f) (inc x) = inc (f x)
    go (inc f) (squash x y p q i j) = squash (go (inc f) x) (go (inc f) y) (Ξ» i β†’ go (inc f) (p i)) (Ξ» i β†’ go (inc f) (q i)) i j
    go (squash f g p q i j) y = squash (go f y) (go g y) (Ξ» i β†’ go (p i) y) (Ξ» i β†’ go (q i) y) i j

  Bind-βˆ₯βˆ₯β‚€ : Bind (eff βˆ₯_βˆ₯β‚€)
  Bind-βˆ₯βˆ₯β‚€ .Bind._>>=_ {A = A} {B = B} = go where
    go : βˆ₯ A βˆ₯β‚€ β†’ (A β†’ βˆ₯ B βˆ₯β‚€) β†’ βˆ₯ B βˆ₯β‚€
    go (inc x) f = f x
    go (squash x y p q i j) f = squash (go x f) (go y f) (Ξ» i β†’ go (p i) f) (Ξ» i β†’ go (q i) f) i j

is-contrβ†’βˆ₯-βˆ₯β‚€-is-contr : βˆ€ {β„“} {A : Type β„“} β†’ is-contr A β†’ is-contr βˆ₯ A βˆ₯β‚€
is-contrβ†’βˆ₯-βˆ₯β‚€-is-contr h = Equivβ†’is-hlevel 0 ((_ , βˆ₯-βˆ₯β‚€-idempotent (is-contrβ†’is-set h)) e⁻¹) h

is-propβ†’βˆ₯-βˆ₯β‚€-is-prop : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ is-prop βˆ₯ A βˆ₯β‚€
is-propβ†’βˆ₯-βˆ₯β‚€-is-prop h = Equivβ†’is-hlevel 1 ((_ , βˆ₯-βˆ₯β‚€-idempotent (is-propβ†’is-set h)) e⁻¹) h

βˆ₯-βˆ₯β‚€-ap : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} β†’ A ≃ B β†’ βˆ₯ A βˆ₯β‚€ ≃ βˆ₯ B βˆ₯β‚€
βˆ₯-βˆ₯β‚€-ap e .fst = βˆ₯-βˆ₯β‚€-map (e .fst)
βˆ₯-βˆ₯β‚€-ap e .snd = is-isoβ†’is-equiv Ξ» where
  .is-iso.from β†’ βˆ₯-βˆ₯β‚€-map (Equiv.from e)
  .is-iso.rinv β†’ elim! Ξ» x β†’ ap inc (Equiv.Ξ΅ e x)
  .is-iso.linv β†’ elim! Ξ» x β†’ ap inc (Equiv.Ξ· e x)

instance
  βˆ₯-βˆ₯β‚€-homogeneous : βˆ€ {β„“} {A : Type β„“} β†’ ⦃ _ : Homogeneous A ⦄ β†’ Homogeneous βˆ₯ A βˆ₯β‚€
  βˆ₯-βˆ₯β‚€-homogeneous {A = A} ⦃ h ⦄ {x} {y} =
    βˆ₯-βˆ₯β‚€-elim {B = Ξ» x β†’ βˆ€ y β†’ (βˆ₯ A βˆ₯β‚€ , x) ≑ (βˆ₯ A βˆ₯β‚€ , y)}
      (Ξ» _ β†’ Ξ -is-hlevel 2 Ξ» _ β†’ Typeβˆ™-path-is-hlevel 1)
      (Ξ» x β†’ βˆ₯-βˆ₯β‚€-elim
        (Ξ» _ β†’ Typeβˆ™-path-is-hlevel 1)
        (Ξ» y β†’ let e , pt = pathβ†’equivβˆ™ h
               in uaβˆ™ (βˆ₯-βˆ₯β‚€-ap e , ap βˆ₯_βˆ₯β‚€.inc pt)))
      x y