Constant maps

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-02-08.
Last modified on 2024-03-13.

module foundation-core.constant-maps where
Imports
open import foundation.universe-levels

Idea

The constant map from A to B at an element b : B is the function x ↦ b mapping every element x : A to the given element b : B. In common type theoretic notation, the constant map at b is the function

  λ x → b.

Definition

const : {l1 l2 : Level} (A : UU l1) (B : UU l2)  B  A  B
const A B b x = b

See also

Recent changes