{- This file contains: - Definition of set truncations -} {-# OPTIONS --cubical --no-import-sorts --safe #-} module Cubical.HITs.SetTruncation.Base where open import Cubical.Core.Primitives -- set truncation as a higher inductive type: data ∥_∥₂ {ℓ} (A : Type ℓ) : Type ℓ where ∣_∣₂ : A → ∥ A ∥₂ squash₂ : ∀ (x y : ∥ A ∥₂) (p q : x ≡ y) → p ≡ q