{-

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