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
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-04-28. Fredrik Bakke. Miscellaneous refactoring and small additions (#579).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).