    ------------------------------------------------------------------------
    -- 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