    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Order morphisms
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Core

    module Relation.Binary.Morphism where

    ------------------------------------------------------------------------
    -- Re-export contents of morphisms

    open import Relation.Binary.Morphism.Definitions public
    open import Relation.Binary.Morphism.Structures public
    open import Relation.Binary.Morphism.Bundles public