DepthComonads.Discrete

{-# OPTIONS --safe #-}

module DepthComonads.Discrete where

open import DepthComonads.Level
open import DepthComonads.Dec
open import DepthComonads.Path

Discrete : Type a → Type a
Discrete A = (x y : A) → Dec (x ≡ y)

record IsDiscrete (A : Type a) : Type a where
  infix 4 _≟_
  field _≟_ : Discrete A
open IsDiscrete ⦃ ... ⦄ public

open import DepthComonads.Stable
open import DepthComonads.HLevels

Discrete→isSet : Discrete A → isSet A
Discrete→isSet d = Stable≡→isSet (λ x y → Dec→Stable (d x y))