Data/Setoid.agda


1
2
3
4
5
6
7
8

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

module Data.Setoid where

open import Relation.Binary using (Setoid)
open import Function.Construct.Setoid using () renaming (setoid to infixr 0 _⇒ₛ_) public

open Setoid renaming (Carrier to ∣_∣) public