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, 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)
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})