open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HIT.Truncation.Set 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.

data βˆ₯_βˆ₯β‚€ {β„“} (A : Type β„“) : Type β„“ where
  inc    : A β†’ βˆ₯ A βˆ₯β‚€
  squash : isSet βˆ₯ A βˆ₯β‚€
   
βˆ₯-βˆ₯β‚€-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 : βˆ₯ A βˆ₯β‚€ β†’ Type β„“'}
          β†’ (βˆ€ x β†’ isSet (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) =
  isSet→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

βˆ₯-βˆ₯β‚€-elimβ‚‚ : βˆ€ {β„“ β„“' β„“''} {A : Type β„“} {B : Type β„“'} {C : βˆ₯ A βˆ₯β‚€ β†’ βˆ₯ B βˆ₯β‚€ β†’ Type β„“''}
           β†’ (βˆ€ x y β†’ isSet (C x y))
           β†’ (βˆ€ x y β†’ C (inc x) (inc y))
           β†’ βˆ€ x y β†’ C x y
βˆ₯-βˆ₯β‚€-elimβ‚‚ Bset f = βˆ₯-βˆ₯β‚€-elim (Ξ» x β†’ isHLevelΞ  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 β†’ isSet (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 β†’ isHLevelΞ  2 (Bset x y)) 
  Ξ» x y β†’ βˆ₯-βˆ₯β‚€-elim (Bset (inc x) (inc y)) (f x y)
  
βˆ₯-βˆ₯β‚€-idempotent : βˆ€ {β„“} {A : Type β„“} β†’ isSet A
                β†’ isEquiv (inc {A = A})
βˆ₯-βˆ₯β‚€-idempotent {A = A} aset = isIsoβ†’isEquiv (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 (Ξ» _ β†’ isPropβ†’isSet (squash _ _)) Ξ» _ β†’ refl