Data/Setoid/Unit.agda


1
2
3
4
5
6
7
8
9
10
11

{-# OPTIONS --without-K --safe #-}

open import Level using (Level)

module Data.Setoid.Unit {c ℓ : Level} where

open import Categories.Category.Instance.SingletonSet using (SingletonSetoid)
open import Relation.Binary using (Setoid)

⊤ₛ : Setoid c ℓ
⊤ₛ = SingletonSetoid {c} {ℓ}