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