------------------------------------------------------------------------
-- The Agda standard library
--
-- The binary relation defined by a constant
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Binary.Construct.Constant.Core where
 
open import Level using (Level)
open import Relation.Binary.Core using (REL)
 
private
  variable
    a b c : Level
    A : Set a
    B : Set b
 
------------------------------------------------------------------------
-- Definition
 
Const : Set c → REL A B c
Const I = λ _ _ → I