    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bundles for types of functions
    ------------------------------------------------------------------------

    -- The contents of this file should usually be accessed from `Function`.

    -- Note that these bundles differ from those found elsewhere in other
    -- library hierarchies as they take Setoids as parameters. This is
    -- because a function is of no use without knowing what its domain and
    -- codomain is, as well which equalities are being considered over them.
    -- One consequence of this is that they are not built from the
    -- definitions found in `Function.Structures` as is usually the case in
    -- other library hierarchies, as this would duplicate the equality
    -- axioms.

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

    module Function.Dependent.Bundles where

    open import Level using (Level; _⊔_)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)

    private
      variable
        a b ℓ₁ ℓ₂ : Level

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

    module _
      (From : Setoid a ℓ₁)
      (To : IndexedSetoid (Setoid.Carrier From) b ℓ₂)
      where

      open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
      open IndexedSetoid To using () renaming (Carrier to B; _≈_ to _≈₂_)

    ------------------------------------------------------------------------
    -- Bundles with one element

      -- Called `Func` rather than `Function` in order to avoid clashing
      -- with the top-level module.
      record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          to   : (x : A) → B x
          cong : ∀ {x y} → x ≈₁ y → to x ≈₂ to y