Constant maps

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

Created on 2022-02-08.
Last modified on 2023-06-10.

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

Definition

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

Recent changes