Constant maps

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

Created on 2022-02-08.
Last modified on 2025-07-15.

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 x = b

See also

Recent changes