    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The constant function
    ------------------------------------------------------------------------

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

    module Function.Construct.Constant where

    open import Function.Base using (const)
    open import Function.Bundles using (Func)
    import Function.Definitions as Definitions using (Congruent)
    import Function.Structures as Structures using (IsCongruent)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures as B hiding (IsEquivalence)

    private
      variable
        a b ℓ₁ ℓ₂ : Level
        A B : Set a

    ------------------------------------------------------------------------
    -- Properties

    module _ (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂) where

      open Definitions

      congruent : ∀ {b} → b ≈₂ b → Congruent _≈₁_ _≈₂_ (const b)
      congruent refl _ = refl

    ------------------------------------------------------------------------
    -- Structures

    module _
      {≈₁ : Rel A ℓ₁} {≈₂ : Rel B ℓ₂}
      (isEq₁ : B.IsEquivalence ≈₁)
      (isEq₂ : B.IsEquivalence ≈₂) where

      open Structures ≈₁ ≈₂
      open B.IsEquivalence

      isCongruent : ∀ b → IsCongruent (const b)
      isCongruent b = record
        { cong           = congruent ≈₁ ≈₂ (refl isEq₂)
        ; isEquivalence₁ = isEq₁
        ; isEquivalence₂ = isEq₂
        }

    ------------------------------------------------------------------------
    -- Setoid bundles

    module _ (S : Setoid a ℓ₂) (T : Setoid b ℓ₂) where

      open Setoid

      function : Carrier T → Func S T
      function b = record
        { to   = const b
        ; cong = congruent (_≈_ S) (_≈_ T) (refl T)
        }