open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Universe
open import 1Lab.HIT.Truncation
open import 1Lab.HLevel.Closure
open import 1Lab.Inductive
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 β₯β


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

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