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