Relation.Binary.Morphism

Source code on Github
------------------------------------------------------------------------
-- 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