This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Codiagonal maps of types

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