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 โปยน)

inl-lc : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {x x' : X} โ†’ inl {๐“ค} {๐“ฅ} {X} {Y} x ๏ผ inl x' โ†’ x ๏ผ x'
inl-lc refl = refl

inr-lc : {X : ๐“ค ฬ‡ } {Y : ๐“ฅ ฬ‡ } {y y' : Y} โ†’ inr {๐“ค} {๐“ฅ} {X} {Y} y ๏ผ inr y' โ†’ y ๏ผ y'
inr-lc refl = refl

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 .(inl x) 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 .(inr y) 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)

\end{code}