open import 1Lab.HLevel.Retracts 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
The most interesting result is that, since the sets form a reflective subcategory of types, it generates 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)