{-

This file contains:

- Definition of propositional truncation

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.PropositionalTruncation.Base where

open import Cubical.Core.Primitives

-- Propositional truncation as a higher inductive type:

data ∥_∥₁ {} (A : Type ) : Type  where
  ∣_∣₁ : A   A ∥₁
  squash₁ :  (x y :  A ∥₁)  x  y