Codiagonal maps of types

Content created by Vojtěch Štěpančík.

Created on 2023-09-20.
Last modified on 2023-09-20.

module foundation.codiagonal-maps-of-types where
Imports 
open import foundation.universe-levels

open import foundation-core.coproduct-types

Idea

The codiagonal map ∇ : A + A → A of A is the map that projects A + A onto A.

Definitions

module _
  { l1 : Level} (A : UU l1)
  where

  codiagonal : A + A → A
  codiagonal (inl a) = a
  codiagonal (inr a) = a

Recent changes