This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Constant maps
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