Propositional truncation in Idris2

PropTrunc.idr

import Data.DPair
import Decidable.Equality

interface IsProp a where
  prop : (0 x : a) -> (0 y : a) -> x = y

0 IsPropD : {a : Type} -> (p : a -> Type) -> Type
IsPropD {a} p = (0 m : a) -> IsProp (p m)

-- POSTULATES
Squash : Type -> Type
squash : (0 x : a) -> Squash a
squashProp : (0 x : Squash a) -> (0 y : Squash a) -> x = y
squashElim : (0 p : Squash a -> Type) -> IsPropD p => (pSquash : (0 x : a) -> p (squash x)) -> (b : Squash a) -> p b

IsProp (Squash a) where
  prop = squashProp
  
IsProp (a = a) where
  prop Refl Refl = Refl

dcong0 : {0 b : a -> Type} -> (f : (0 x : a) -> b x) -> x = y -> f x = f y
dcong0 f Refl = Refl

{0 p : a -> Type} -> DecEq a => DecEq (Subset a (\x => Squash (p x))) where
  decEq (Element x1 y1) (Element x2 y2) with (decEq x1 x2)
    decEq (Element x1 y1) (Element x1 y2) | Yes Refl = Yes (dcong0 (Element x1) (squashProp y1 y2))
    decEq (Element x1 y1) (Element x2 y2) | No c = No (\Refl => c Refl)