Properties of the disjoint sum _+_ of types.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module MLTT.Plus-Properties where

open import MLTT.Plus
open import MLTT.Negation
open import MLTT.Id
open import MLTT.Empty
open import MLTT.Unit
open import MLTT.Unit-Properties

+-commutative : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ A + B β†’ B + A
+-commutative = cases inr inl

+disjoint : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x : X} {y : Y} β†’ Β¬ (inl x ＝ inr y)
+disjoint {𝓀} {π“₯} {X} {Y} p = πŸ™-is-not-𝟘 q
 where
  f : X + Y β†’ 𝓀₀ Μ‡
  f (inl x) = πŸ™
  f (inr y) = 𝟘

  q : πŸ™ ＝ 𝟘
  q = ap f p

+disjoint' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x : X} {y : Y} β†’ Β¬ (inr y ＝ inl x)
+disjoint' p = +disjoint (p ⁻¹)

lni : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X β†’ X + Y β†’ X
lni xβ‚€ (inl x) = x
lni xβ‚€ (inr y) = xβ‚€

inl-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x x' : X}
       β†’ inl {𝓀} {π“₯} {X} {Y} x ＝ inl x' β†’ x ＝ x'
inl-lc {𝓀} {π“₯} {X} {Y} {x} = ap (lni x)

rni : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ Y β†’ X + Y β†’ Y
rni yβ‚€ (inl x) = yβ‚€
rni yβ‚€ (inr y) = y

inr-lc : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {y y' : Y}
       β†’ inr {𝓀} {π“₯} {X} {Y} y ＝ inr y' β†’ y ＝ y'
inr-lc {𝓀} {π“₯} {X} {Y} {y} = ap (rni y)

equality-cases : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } (z : X + Y)
               β†’ ((x : X) β†’ z ＝ inl x β†’ A) β†’ ((y : Y) β†’ z ＝ inr y β†’ A) β†’ A
equality-cases (inl x) f g = f x refl
equality-cases (inr y) f g = g y refl

Cases-equality-l : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } (f : X β†’ A) (g : Y β†’ A)
                 β†’ (z : X + Y) (x : X) β†’ z ＝ inl x β†’ Cases z f g ＝ f x
Cases-equality-l f g z x refl = refl

Cases-equality-r : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } (f : X β†’ A) (g : Y β†’ A)
                 β†’ (z : X + Y) (y : Y) β†’ z ＝ inr y β†’ Cases z f g ＝ g y
Cases-equality-r f g z y refl = refl

Left-fails-gives-right-holds : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } β†’ P + Q β†’ Β¬ P β†’ Q
Left-fails-gives-right-holds (inl p) u = 𝟘-elim (u p)
Left-fails-gives-right-holds (inr q) u = q

Right-fails-gives-left-holds : {P : 𝓀 Μ‡ } {Q : π“₯ Μ‡ } β†’ P + Q β†’ Β¬ Q β†’ P
Right-fails-gives-left-holds (inl p) u = p
Right-fails-gives-left-holds (inr q) u = 𝟘-elim (u q)

open import MLTT.Sigma
open import Notation.General

inl-preservation : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X + πŸ™ {𝓦}  β†’ Y + πŸ™ {𝓣})
                 β†’ f (inr ⋆) ＝ inr ⋆
                 β†’ left-cancellable f
                 β†’ (x : X) β†’ Ξ£ y κž‰ Y , f (inl x) ＝ inl y
inl-preservation {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} f p l x = Ξ³ x (f (inl x)) refl
 where
  Ξ³ : (x : X) (z : Y + πŸ™) β†’ f (inl x) ＝ z β†’ Ξ£ y κž‰ Y , z ＝ inl y
  Ξ³ x (inl y) q = y , refl
  Ξ³ x (inr ⋆) q = 𝟘-elim (+disjoint (l r))
   where
    r : f (inl x) ＝ f (inr ⋆)
    r = q βˆ™ p ⁻¹

+functor : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {A : 𝓦 Μ‡ } {B : 𝓣 Μ‡ }
         β†’ (X β†’ A) β†’ (Y β†’ B) β†’ X + Y β†’ A + B
+functor f g (inl x) = inl (f x)
+functor f g (inr y) = inr (g y)

+functorβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } {X' : 𝓀' Μ‡ } {Y' : π“₯' Μ‡ } {Z' : 𝓦' Μ‡ }
          β†’ (X β†’ X') β†’ (Y β†’ Y') β†’ (Z β†’ Z') β†’ X + Y + Z β†’ X' + Y' + Z'
+functorβ‚‚ f g h = +functor f (+functor g h)

\end{code}

Added 29 Sep 2026 by Tom de Jong.

Previously, inl-lc-is-section and inr-lc-is-section were in UF.Sets and relied
on injectivity of inl (resp. inr) which Agda silently uses when we pattern match
on a term of type inl x ＝ inl x'.

\begin{code}

module encode-decode-inl
        {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
        {xβ‚€ : X}
       where

 private
  C : X + Y β†’ 𝓀 Μ‡
  C (inl x) = xβ‚€ ＝ x
  C (inr x) = 𝟘

  encode : (z : X + Y) β†’ (inl xβ‚€ ＝ z) β†’ C z
  encode (inl _) = inl-lc
  encode (inr _) = Ξ» p β†’ 𝟘-elim (+disjoint p)

  decode : (z : X + Y) β†’ C z β†’ (inl xβ‚€ ＝ z)
  decode (inl _) c = ap inl c
  decode (inr _) c = 𝟘-elim c

 encode-decode : (z : X + Y) (p : inl xβ‚€ ＝ z)
               β†’ decode z (encode z p) ＝ p
 encode-decode z refl = refl

 decode-encode : (z : X + Y) (c : C z) β†’ encode z (decode z c) ＝ c
 decode-encode (inl _) refl = refl
 decode-encode (inr _) c = 𝟘-elim c

inl-lc-is-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    {x x' : X}
                    (p : inl {𝓀} {π“₯} {X} {Y} x ＝ inl x')
                  β†’ ap inl (inl-lc p) ＝ p
inl-lc-is-section = encode-decode-inl.encode-decode (inl _)

inl-lc-is-retraction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                       {x x' : X}
                       (p : x ＝ x')
                     β†’ inl-lc {𝓀 } {π“₯} {X} {Y} (ap inl p) ＝ p
inl-lc-is-retraction = encode-decode-inl.decode-encode (inl _)

module encode-decode-inr
        {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
        {yβ‚€ : Y}
       where

 private
  C : X + Y β†’ π“₯ Μ‡
  C (inl _) = 𝟘
  C (inr y) = yβ‚€ ＝ y

  encode : (z : X + Y) β†’ (inr yβ‚€ ＝ z) β†’ C z
  encode (inl _) = Ξ» p β†’ 𝟘-elim (+disjoint (p ⁻¹))
  encode (inr _) = inr-lc

  decode : (z : X + Y) β†’ C z β†’ (inr yβ‚€ ＝ z)
  decode (inl _) c = 𝟘-elim c
  decode (inr _) c = ap inr c

 encode-decode : (z : X + Y) (p : inr yβ‚€ ＝ z)
               β†’ decode z (encode z p) ＝ p
 encode-decode z refl = refl

 decode-encode : (z : X + Y) (c : C z) β†’ encode z (decode z c) ＝ c
 decode-encode (inl _) c = 𝟘-elim c
 decode-encode (inr _) refl = refl

inr-lc-is-section : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    {y y' : Y}
                    (p : inr {𝓀} {π“₯} {X} {Y} y ＝ inr y')
                  β†’ ap inr (inr-lc p) ＝ p
inr-lc-is-section = encode-decode-inr.encode-decode (inr _)

inr-lc-is-retraction : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                       {y y' : Y}
                       (p : y ＝ y')
                     β†’ inr-lc {𝓀} {π“₯} {X} {Y} (ap inr p) ＝ p
inr-lc-is-retraction = encode-decode-inr.decode-encode (inr _)

\end{code}